What is the endgoal of formalising mathematics?

Question

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?

Answer 1

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.

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?

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.

Will mathematicians themselves be expected to formalise their results as they are proved?

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.

Answer 2

Since you mentioned 100 years out, let me suggest that the end goal is to put ourselves out of business.

We just need to formalize enough mathematics so that AI programs will get the idea of what we're trying to do. Then they'll take over the job of doing mathematics research. We won't need to formalize any old math at that point because the AIs will rediscover everything worth rediscovering anyway.

[EDIT: For an example of some first baby steps in this direction, see Generative language modeling for automated theorem proving by Stanislas Polu and Ilya Sutskever.]

I am half joking here, but only half. I don't think that the only, or even the main, goal of formalizing is to increase the certainty of a proof from 99.9% to 99.9999999%. The main goal is to enable new approaches to doing research that don't currently exist.

For that goal, complete formalization isn't necessary, but for what it's worth, I also don't believe that "chasing our tail" will be a problem. Setting aside my pie-in-the-sky vision of putting mathematicians out of business, I think that once the tools get good enough, and the mathematical populace is sufficiently trained, new proofs will be formalized as a matter of course, just as papers are now written in $\LaTeX$ as a matter of course. As for the older papers, formalizing them will be assigned as exercises for students who are just learning the system.

Answer 3

Other answers address several aspects of your question, but to add a point not mentioned yet — you write:

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?

Certainly, at the moment, formalising maths is very laborious and time-consuming. But I think most people who work the formalisation hope that it won’t stay so bad! It’s been getting steadily better as proof assistants and their libraries have progressed — “better” both in terms of how quickly experienced users can cover ground, and in terms of the learning curve for new users. This improvement hasn’t perhaps been as fast as we’d like, or might have hoped — but it’s been steady, and continuing.

If usability continues to improve, then it’s reasonable to imagine a future proof assistant with a role comparable to LaTeX today. Typesetting our work in LaTeX takes a bit of work, and has a bit of a learning curve — but most mathematicians accept the time and effort as worthwhile for the payoff of good typesetting. A very few mathematicians outsource this to professional typesetters; a larger minority leave it to their co-authors when possible. But it’s part of the expectations of the field, and there’s no problem of “tail-chasing” — no question of “can we typeset mathematics as fast as we can produce it?”, or of requiring major grant support to get work typeset. This is one possible future that I and some others in formalisation envisage, and that it seems reasonable to hope for in a timescale of a few decades.

One likely difference from LaTeX is that this could well arrive in some subfields of maths sooner than others, since (so far) some topics seem much more amenable to formalisation.

Answer 4

I've thought more about what would be required for a complete formalisation of mathematics. I believe this could only happen if mathematicians formalise their results as they go, i.e. all of them are actively using proof assistants as part of the research process. To this end, here are some properties that I think would be desirable in a proof system:

1. Syntax that is "proof-y" rather than "program-y". I played around with Lean last night, on Kevin Buzzard's great natural number game, but it still felt like I was programming, rather than writing a proof. Yes, I know they're equivalent by the Curry-Howard isomorphism, but mathematicians don't want to learn a new programming language, they want to write proofs. Why couldn't we have syntax that looks like an actual, natural-language proof, e.g.

   Theorem:
   Let U, V be vector spaces.
   Let f: U -> V be a linear map.
   Then dim(U) = rank(f) + nullity(f).
   
   Proof:
   Fix v in V.
   ....
   

   Here, Let could be a command indicating that one is defining a new object, be / be a / be an indicates the type of said object, Then indicates you are done defining things, . indicates the end of a command, etc.

2. A typing system that reflects mathematical intuition. I know very little type theory, but it seems like dependent types are necessary to the way mathematics is currently practiced. Other properties such as univalence, polymorphism, inheritance, abstract data types also seem necessary to reflect "real" mathematical practice. I know this might add complexity to a proof assistant; however, the proof assistant should be designed to meet mathematicians, rather than us having to meet the proof system.

3. I work in logic, and there are many subfields (set theory, reverse mathematics, constructive math) where axioms can vary. So to formalise these areas, we would need a way to change the axioms as necessary. E.g. $\mathsf{ZFC}$ would be taken as the default set of axioms, but you could declare

   Axioms = ZF+AD.
   

   at the start to change the axioms for your proofs. Further, you would want to be able to treat axioms as objects in their own right.

4. Many steps of reasoning will often be skipped in a mathematician's proof (as it is painstaking to write it all out in full). Therefore, I would want an "autofill" system, where one puts in the main steps of the proof (i.e. those that you would write in the natural language proof):

   (n + 1)^3
   ...
   n^3 + 3n^2 + 3n + 1
   

   and the proof assistant would search to find correct reasoning to fill the space between.

5. One of the current issues is that not enough prerequisite material has been formalised for most research mathematicians to start using proof assistants for their work. I wonder if it's possible to have a "modular" approach, where mathematicians can take the theorems they want to use as "axioms", and proceed with formalising their work. Then, someone else can come along later and prove these "axioms" from more foundational principles. This would mean that mathematicians could start using the proof system right now, rather than in 20 years when all the necessary background has been formalised (and their research has moved on). (I suppose the relevant definitions still need to be formalised beforehand).

I don't know much about the different proof assistants, and whether there are any that have the above properties.