Of possible interest: Peter Scholze and Fomalization of mathematics

[Siddhartha Gadgil]

Dear All,

          Peter Scholze reports as a guest post on the blog of Kevin Buzzard what may be considered a landmark in "Formalization of mathematics", i.e., computer verification of a mathematical proof: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/

Half a year of the Liquid Tensor Experiment: Amazing developments | Xena [This is a guest post by Peter Scholze.] Exactly half a year ago I wrote the Liquid Tensor Experiment blog post, challenging the formalization of a difficult foundational theorem from my Analytic Geometry lecture notes on joint work with Dustin Clausen. While this challenge has not been completed yet, I am excited to announce that the Experiment has verified the entire part of the argument ... xenaproject.wordpress.com



       Based on what I understand, here is a brief summary. Clausen and Scholze are developing "Condensed mathematics", with "condensed sets" replacing topological spaces (replacing in algebraic applications but equvialent to usual topology in geometric situations). A foundational theorem of theirs had a delicate proof and Scholze was worried it could be wrong. Since it wan meant to be used as a blackbox, an error would mean a lot of mathematics built on it will be in doubt.

        Six months ago, Scholze issued a challenge to the formalization community to formalize and computer verify a set of results, including the foundational one. Scholze announces that the result he was waorried about is now formally verified in the lean theorem prover, with some tweaks to the proof outline along the way (and the original challenge is halfway done). This suggests that "formalization" is approaching the stage where this is (even in practice) the best way to be sure mathematics is correct. 

regards,

Siddhartha