A mathematical formalisation challenge by Peter Scholze
xenaproject.wordpress.com
xenaproject.wordpress.com
“ I have occasionally been able to be very persuasive even with wrong arguments. (Fun fact: In the selection exams for the international math olympiad, twice I got full points for a wrong solution. Later, I once had a full proof of the weight-monodromy conjecture that passed the judgment of some top mathematicians, but then it turned out to contain a fatal mistake.)”
Scholze's first application of the theory of perfectoid spaces was to prove weight-monodromy in many new cases (but not in all cases) -- this was his first breakthrough result really. Fun fact: in the first version of the post which he sent me, this weight-monodromy confession was not there. He then slept on it and sent a second version a day later, and it was only when I was converting the LaTeX into Wordpress format that I noticed that he had added this extra line. I quite agree that it is very rare for people, especially of his stature, to publically admit to errors, especially ones which never made it into print. Of course we will be working on this challenge in Lean, and we are currently optimistic, but who knows. It is certainly true that in the study group we had on the work at Imperial earlier this year, we did not work through the technical proof which Scholze is now challenging the formalization community to check. This is really Scholze's point I guess: once you have a Fields Medal it's very easy for other people to say "well this is a bit technical but let's face it, it's probably fine" (this is exactly what we did, for example). Voevodsky made similar comments around a decade ago -- and he managed to get false arguments published, perhaps partly because of his own Fields Medal. Scholze is flagging an explicit argument in his work which he believes needs to be carefully analysed, and I have seen with my own eyes that the academic system we have right now might not actually do it carefully enough. What is not at all clear, right now at least, is whether computer proof verification systems are up to the task. I think it will be interesting to see how this develops.
Yes, Voedovsky’s abd Scholze’s candidness is encouraging and liberating. And a great call to responsibility for us reviewers.
And thanks for your work on formalization. Truly important in my view.
[It's not just about math, see https://hapgood.us/2015/10/17/the-garden-and-the-stream-a-te... for a great explanation of the type of labor that is mathlib is sorely lacking in just about every sector. I'm really hoping that mathematics can lead the way here.]
It's certainly possible in principle, but whether it's possible in practice is part of the challenge. You need enough people that understand the details of the proof, and know how to turn that into a formally verified proof. Such proofs can also become slow, so to keep things practical, you also need to take speed into account.
Also, and perhaps easier to wrap one's head around, is issues of tooling. Already, there is a very heavy use of "tactics" (metaprograms, and ones with decent computational complexity (think "search" not just "expansion")). Mathematicians write lemmas so we can try to run the tactics on "mini problems" that do not grow even as the total body of work grows, but there's always a risk the that there's some sticking point one cannot break down enough.
(Three years later, my doctoral supervisor pointed out the mistake to me, and we published another paper -- in the same journal -- filling the gap.)
I am certainly not one of those people. Nevertheless, I find this enormously exciting. Formalisation of mathematics has long been the preserve of a handful of logicians and type theorists. What we’re seeing here is one of the world’s leading mathematicians, whose work is situated squarely at the centre of what is today considered mainstream mathematics, advocating the importance of formalisation.
If, like me, you believe that formalisation will be an essential part of the mathematics of the future, this is a very encouraging development.
The TLDR is that Peter Scholze, one of modern mathematics' most accomplished theory builders, has a concept called a 'condensed set' that he thinks can act as a drop-in replacement for topological spaces in most of mathematics. Topological spaces are perhaps one of the least restrictive models of 'space' is in mathematics. Peter thinks his definition will allow mathematicians to bring algebraic techniques to bear on problems that were previously not amenable to such methods.
The problem is that everything rests on one theorem, whose proof is difficult. Because the proof is so foundational, he'd like to get it checked by computer instead of relying on the opinion of a handful of mathematicians, who may be sloppy in their checking.
1. https://leanprover-community.github.io/
2. http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game...
Theorem proving can be a fun open-world videogame, and I do hope these aspects can be refined overtime to make real mathematics a lot more accessible.
can this type of push towards formalizing mathematical proofs be seen as a sort of continuation of Hilbert's program? If no, what's the difference? If yes, how are the fatal issues in that program avoided?
Actually Hilbert’s Programme was shattered when his great hope (the proof of the consistency and completeness of Mathematics FINITISTICALLY) was proved impossible (actually inconsistent).
But from the point of view of mechanizing Maths, it is more or less equivalent.