Johan Commelin, The Liquid Tensor Experiment

Homotopy Type Theory Electronic Seminar Talks, 2023-01-26

In December 2020, Peter Scholze posed a challenge to formally verify the main theorem on liquid R-vector spaces, which is part of his joint work with Dustin Clausen on condensed mathematics. I took up this challenge with a team of mathematicians to verify the theorem in the Lean proof assistant. Half a year later, we reached a major milestone, and in the summer of 2022 we have completed the full challenge.

In this talk I will give a brief motivation for condensed/liquid mathematics, report on our experiences formalizing state-of-the-art research in mathematics, and discuss some new insights in the proof of the main theorem.

[fbkintanar]

This is was a weird talk to listen to. It discussed a part of math that is completely impenetrable to me, with my limited math background. But it also offered some tantalizing glimpses on how high-end mathematicians and logicians/computer science researchers can talk metamathetically about parts of math as formal objects. It is interesting where he discusses Lesson (2) 55:35 from the experience. He was surprised that the interactive theorem prover acted more helpful like a genuine proof assistant than he expected, it really helped in a way that you have no right to expect from a dumb piece of silicon. 56:15 "Lean showed to be a powerful tool for managing complex proofs." Somehow this give me optimism that formally encoded proofs can eventually be helpful in math education, even at the graduate researcher level. His description about translating from Latin 57:00 suggests to me that students may be able to slog through a difficult piece of math a few lines at a time, and somehow come out with understanding where they might have been stuck forever without a software tool. Scholz's cited comment that the proof seems too large to fit in human RAM makes me wonder about modern math research and the limits of human cognition. It looks like professional mathematicians will be needed to explain how high-end proofs can be conceptualized for a broader audience, they aren't going to be put out of work by interactive theorem provers. It will just save reviewers the boring manual work of verifying very technical proofs, and make it possible to hand off some of the work to teams of less-skilled coders in the language of the chosen proof assistant. The time of the reviewers of advanced math will hopefully be freed up to write more expository articles and books! Math as a whole could become more accessible to mere mortals.