6 ms·
I very much like this. I wonder whether this will eventually lead to collaborative proofs , and ‘ bug fixes’ , essentially turning maths into a process similar
by Agingcoder 2y ago
I very much like this.
I wonder whether this will eventually lead to collaborative proofs , and ‘ bug fixes’ , essentially turning maths into a process similar to code on GitHub.
- trenchgun 2y agoAlready is. Check Lean blueprints. https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
- practal 2y agoYes, this idea of collaborative proofs has been around for a while now, at least for 10 years: https://arxiv.org/abs/1404.6186 https://arxiv.org/abs/1404.6186