Recently, I've become interested in proof assistants such as Lean, Coq, Isabelle, and the drive from many mathematicians (Kevin Buzzard, Tom Hales, Metamath, etc) to formalise all of mathematics in such a system. I am very sympathetic to some of the aims of this project, such as finding mistakes in published proofs, and definitively verifying complex and controversial proofs [Kepler conjecture (Hales), four-colour theorem (Appel/Haken), Fermat's last theorem (Wiles), …].
However, I'd like to understand more about the ultimate goals of this project, and the vision for achieving a computer formalisation of all of mathematics. I understand a good portion of core (undergraduate) mathematics has been formalised. Yet, the bulk of research-level mathematics remains unformalised, and it seems to me that we are currently creating new mathematics at a far greater rate than we are formalising mathematics. Are we always going to be "chasing our tails" here? What needs to change so that we can catch up and achieve a complete formalisation of mathematics?
Another issue is, of course, new mathematics is being created all the time. If we achieve complete formalisation, how do we sustain this? Will there be "professional formalisers" whose job it is to formalise the recent results of mathematicians? Will mathematicians themselves be expected to formalise their results as they are proved? What role will proof assistants play in 20 (or 50, or 100) years?
Best Answer
This answer is based only on my having watched this lecture by Kevin Buzzard, followed by my applying some skepticism and critical thinking.
Buzzard has had some experiences that make him not trust some of the results that people are claiming in mathematics papers. He tells the story of refereeing a paper and fighting (and winning) a long, drawn-out battle because he didn't believe the authors had proved what they said they had. He also says there are papers coming out in which a result is said to be proved, but there are 100 pages of details that have been left out and will be supplied in a forthcoming publication.
With, in my opinion, less justice, he complains that professional mathematicians "do math like Gauss and Euler," "don't know foundations," "don't know set theory," and decide what is correct mathematics based on a consensus of beliefs among the elders in the community. This seems absurd to me. I would consider a theorem by Gauss or Euler to be less reliable if it depended on ZFC. If someone told me that a theorem in analysis depended on choice, I would decide that that theorem was not really true but only true conditioned on AC. If ZFC is proved tomorrow to be inconsistent, I will still have great faith that the theorems of Gauss and Euler are correct within some more conservative foundational system.
However, if you believe at least some of his complaints about real uncertainty and doubt in published mathematical results, then it does make some sense to see if you can "formalize" these results in the sense of getting a computer to verify them all the way down to some foundation.
What seems to have been going on for a long time with computer theorem checkers is that because using them was so labor-intensive, people would try to code up the tiniest possible fragment of mathematics in order to achieve their goal. The trouble with this strategy seems to be the following. If you believe that a lot of math really is in doubt, then the doubtful parts are in areas where there is a big pyramid of math. At the apex you have Fermat's last theorem or something about perfectoid spaces (which I know nothing about, but he cites them as modern pieces of mathematical machinery with a lot of moving parts). The apex is supported by a whole bunch of more basic stuff, going all the way down through freshman calculus, etc. Therefore you can't do a tiny fragment of mathematics, because these aren't self-contained fragments.
So I think that Buzzard's argument is: (1) there are important, significant doubts about whether results deemed true by the elders really are true; (2) theorem provers are a good way of solving this problem; and (3) in order to carry out this solution, one needs to build up a comprehensive database of the beliefs of the elders (his characterization of Hale).
My own opinion is that 1 is probably true but not a threat to the enterprise of mathematics, 2 is speculative, and 3 is infeasible. Of course my opinion is worthless because I'm not even an amateur in this area. But note that even if I'm right, it doesn't mean that proof assistants and automated theorem checkers shouldn't be worked on at all -- it just means that Buzzard's grandiose dream isn't going to happen.
Looking into my crystal ball, I predict that it will not be achieved, because it costs too much, and the necessary vast funding will not be allocated. It won't be allocated because not many mathematicians agree that it would be a worthwhile use of the resources. Systematic ongoing formalization will also not happen, for the same reasons.
No. By all accounts this work is tedious and extremely time-consuming. Mathematicians want to work with new ideas, not spend their time writing code to explain their work to a computer that is orders of magnitude dumber than the dumbest undergrad they've ever taught.