3 ms·

Maybe half (?) of the basic undergraduate math curriculum has been formally verified, after decades of effort by large numbers of researchers. The proof under d

Maybe half (?) of the basic undergraduate math curriculum has been formally verified, after decades of effort by large numbers of researchers. The proof under discussion here is significantly more complicated than anything that has ever been formally verified, as far as I understand. Disclaimer: I don’t know much about formal verification of mathematics, only what I have read from time to time on the internet.

3PS 5y ago
It's not out of the question for research-level math to be formalized in proof assistants. Most notably, a landmark paper by Peter Scholze (a Fields medalist) was, at his request, formalized in Lean. Or at least, the important part was formalized in about 6 months. See [1] for the post where Scholze asks for help in formalizing the proof and explains why he thinks it's important - in this case it was a very gnarly proof of a theorem that could hopefully be used as a black box by other mathematicians. See [2] for Scholze's thoughts after the project succeeded, 6 months later. [1] https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/ https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e... [2] https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...
- jacobolus 5y ago
  This is great work. But to be clear: a community effort by 20+ people, after 6 months of work, managed to make progress toward proving a theorem, including proving some of the trickiest technical parts. As I said before, this is like 2 orders of magnitude more effort than the original plain-language (slightly sloppy/underspecified) proof. Scholze: > I cannot read the proofs at all — they are analogous to referring to theorems only via their LaTeX labels, together with a specification of the variables to which it gets applied; plus the names of some random proof finding routines.

3PS 5y ago

It's not out of the question for research-level math to be formalized in proof assistants. Most notably, a landmark paper by Peter Scholze (a Fields medalist) was, at his request, formalized in Lean. Or at least, the important part was formalized in about 6 months. See [1] for the post where Scholze asks for help in formalizing the proof and explains why he thinks it's important - in this case it was a very gnarly proof of a theorem that could hopefully be used as a black box by other mathematicians. See [2] for Scholze's thoughts after the project succeeded, 6 months later. [1] https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/ https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e... [2] https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...

jacobolus 5y ago
This is great work. But to be clear: a community effort by 20+ people, after 6 months of work, managed to make progress toward proving a theorem, including proving some of the trickiest technical parts. As I said before, this is like 2 orders of magnitude more effort than the original plain-language (slightly sloppy/underspecified) proof. Scholze: > I cannot read the proofs at all — they are analogous to referring to theorems only via their LaTeX labels, together with a specification of the variables to which it gets applied; plus the names of some random proof finding routines.