5 ms·

> I don't think this is easily resolved. It is technically resolvable. Just insist on Lean (or some other formal verifier) proofs for everything. It looks to

> I don't think this is easily resolved. It is technically resolvable. Just insist on Lean (or some other formal verifier) proofs for everything. It looks to me like math is heading that way, but a lot of mathematicians will have to die before its the accepted practice. Mathematicians who are already doing formal proofs are discovering it have the same properties as shared computer code. Those properties have have lead to most of the code executed on the planet being open source source, despite the fact you can't make money directly from it. Code is easy to share, easy to collaborate on, and in the case of formal proofs easy to trust. It is tedious to write, but collaboration is so easy that publishing your 1/2 done work will often prompt others to do some of the tedious stuff. Code isn't self documenting unless it's very well written, but even horrible code is far better at documenting what it does than what you are describing.

zozbot234 2y ago
> Just insist on Lean (or some other formal verifier) proofs for everything. This is not an easy change at all. Some subfields of math rely on a huge amount of prereqs, that all have to be formalized before current research in that field can insist on formal proofs for everything as a matter of course. This is the problem that the Lean mathlib folks are trying to address, and it's a whole lot of work. The OP discusses a fraction of that work - namely, formalizing every prereq for modern proofs of FLT - that is expected to take several years on its own.
eab- 2y ago
> Just insist on Lean (or some other formal verifier) proofs for everything Lean is too inflexible for this, in my opinion. Maybe I'm not dreaming big enough, but I think there'll have to be one more big idea to make this possible; I think the typeclass inference systems we use these days are a severe bottleneck, for one, and I think it's very, very tedious to state some things in Lean (my go-to example is the finite-dimensionality of modular forms of level 1 - the contour integral is a bitch and has a lot of technicalities)
- ykonstant 2y ago
  I agree, although I don't see a better solution: typeclass inference is trying to "quasi-solve" higher unification, which is unsolvable. The core tactics writers are already doing wizard-level stuff and there is more to come, but the challenge is immense. By the way, if you are a meta-programming wizard and/or a Prolog wizard, please consider learning Lean 4 or another tactics based proof assistant. I think they will all welcome expert assistance in the development of better tactics and the improvement and debugging of current ones.
panda-giddiness 2y ago
You might as well have written that mathematicians should stop doing mathematics. If every mathematician were to work full time on formalizing theorems in proof assistants, then no living mathematician would ever do original research again -- there is simply too much that would need to be translated to software. And to what end? It's not as if people suspect that the foundations of mathematics are on the verge of toppling. > Code is easy to share, easy to collaborate on [...] collaboration is so easy that publishing your 1/2 done work will often prompt others to do some of the tedious stuff Here's an experiment anyone can try at home: pick a random article from the mathematics arxiv [1]. Now rewrite the main theorem from that paper in Lean [2]. Did you find this task "easy"? Would you go out of your way to finish the "tedious" stuff? > even horrible code is far better at documenting what it does than what you are describing The "documentation" is provided by talking to other researchers in the field. If you don't understand some portion of a proof, you talk to someone about it. That is a far more efficient use of time than writing code for things that are (relatively) obviously true. (No shade on anyone who wants to write proofs in Lean, though.) --- [1] https://arxiv.org/list/math/new https://arxiv.org/list/math/new [2] https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html https://lean-lang.org/theorem_proving_in_lean4/dependent_typ...

zozbot234 2y ago

> Just insist on Lean (or some other formal verifier) proofs for everything. This is not an easy change at all. Some subfields of math rely on a huge amount of prereqs, that all have to be formalized before current research in that field can insist on formal proofs for everything as a matter of course. This is the problem that the Lean mathlib folks are trying to address, and it's a whole lot of work. The OP discusses a fraction of that work - namely, formalizing every prereq for modern proofs of FLT - that is expected to take several years on its own.

eab- 2y ago

> Just insist on Lean (or some other formal verifier) proofs for everything Lean is too inflexible for this, in my opinion. Maybe I'm not dreaming big enough, but I think there'll have to be one more big idea to make this possible; I think the typeclass inference systems we use these days are a severe bottleneck, for one, and I think it's very, very tedious to state some things in Lean (my go-to example is the finite-dimensionality of modular forms of level 1 - the contour integral is a bitch and has a lot of technicalities)

ykonstant 2y ago
I agree, although I don't see a better solution: typeclass inference is trying to "quasi-solve" higher unification, which is unsolvable. The core tactics writers are already doing wizard-level stuff and there is more to come, but the challenge is immense. By the way, if you are a meta-programming wizard and/or a Prolog wizard, please consider learning Lean 4 or another tactics based proof assistant. I think they will all welcome expert assistance in the development of better tactics and the improvement and debugging of current ones.

panda-giddiness 2y ago

You might as well have written that mathematicians should stop doing mathematics. If every mathematician were to work full time on formalizing theorems in proof assistants, then no living mathematician would ever do original research again -- there is simply too much that would need to be translated to software. And to what end? It's not as if people suspect that the foundations of mathematics are on the verge of toppling. > Code is easy to share, easy to collaborate on [...] collaboration is so easy that publishing your 1/2 done work will often prompt others to do some of the tedious stuff Here's an experiment anyone can try at home: pick a random article from the mathematics arxiv [1]. Now rewrite the main theorem from that paper in Lean [2]. Did you find this task "easy"? Would you go out of your way to finish the "tedious" stuff? > even horrible code is far better at documenting what it does than what you are describing The "documentation" is provided by talking to other researchers in the field. If you don't understand some portion of a proof, you talk to someone about it. That is a far more efficient use of time than writing code for things that are (relatively) obviously true. (No shade on anyone who wants to write proofs in Lean, though.) --- [1] https://arxiv.org/list/math/new https://arxiv.org/list/math/new [2] https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html https://lean-lang.org/theorem_proving_in_lean4/dependent_typ...