28
$\begingroup$

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?

$\endgroup$
24
  • 13
    $\begingroup$ "What role will proof assistants play in 20 (or 50, or 100) years?" Well, in order to answer this, I guess one should possess some kind of pre-cog ability :-) $\endgroup$ Dec 9 '20 at 7:31
  • 6
    $\begingroup$ One near-term goal motivation of formalization can be seen in Scholze's recent formalization challenge. He (and Dustin Clausen) have a result that is "logically involved" (of the form $\forall\exists\forall\exists\forall\exists$), and that could be the basis of a new approach to real functional analysis by applying the theorem in a "black box" way. The "black box" application means the details of the proof may get examined less than other foundational results. One should read the linked post for more details. $\endgroup$
    – Mark
    Dec 9 '20 at 18:22
  • 6
    $\begingroup$ Who is talking about formalizing all of mathematics, and where? That assumption of the question seems dubious, and I don't see any references for that claim. $\endgroup$
    – Matt F.
    Dec 9 '20 at 19:30
  • 5
    $\begingroup$ I would suggest, as with several questions that have surfaced concerning what Kevin has said and written in a certain rhetorical vein, that we are best off waiting for him to turn up in person, when he can either row back or double down as he sees fit :) $\endgroup$
    – Yemon Choi
    Dec 9 '20 at 20:02
  • 17
    $\begingroup$ What's the point of digitising music? Vinyl works fine. But digitising music was a game changer -- now we have Spotify. What's the point in digitising books? What's the point in LaTeX? Typewriters worked fine. What's the point of digitising mathematics? We have no idea what will happen as a consequence. People will use it to do crazy things we can't even imagine right now. Ask the machine learning people what the point of digitising mathematics is. Ask the educators. Ask Scholze. People will figure out uses. We should do it because we can. Because nobody tried to do it yet. $\endgroup$ Dec 10 '20 at 9:52
20
$\begingroup$

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.

$\endgroup$
17
  • 1
    $\begingroup$ This brings up an interesting point. As mentioned, if the goal of formalization is to feel more secure about the cutting-edge of math by formalizing everything, that would require a huge change in mathematical practice and culture. On the other hand, if the goal is to root out bogus arguments, perhaps a different system could be designed: one which could be fed in the logical "shape" of an argument and try to detect places where the logic might fail. Notice that in the first picture, the onus is on the prover, and in the second it is on the doubter. $\endgroup$ Dec 9 '20 at 19:03
  • 2
    $\begingroup$ So, true is the theory you get from the reverse mathematics of Gauss + Euler + whatever fragments you have that don't require things like "the real numbers are not a countable union of countable sets" and other choicey consequences. $\endgroup$
    – Asaf Karagila
    Dec 9 '20 at 19:28
  • 3
    $\begingroup$ @AsafKaragila: Sure, or maybe we should call it classical-analysis-true. Seems to me that there is a whole separate Q&A implied here, which you would be more qualified than I am both to ask and to answer :-) $\endgroup$ Dec 9 '20 at 19:32
  • 11
    $\begingroup$ @BenCrowell : I don't think that Buzzard's point about "elders" has anything to do with ZFC specifically. If ZFC bothers you, replace it with something much weaker, such as RCA$_0$. As I see it, Buzzard is contrasting a situation in which all the details of a proof are truly available for public inspection, with a situation where many crucial details are locked up inaccessibly in the brains of a few experts. $\endgroup$ Dec 9 '20 at 23:06
  • 2
    $\begingroup$ 'professional mathematicians "do math like Gauss and Euler,'"' - Wouldn't it be great if that were true? $\endgroup$ Dec 10 '20 at 5:50
17
$\begingroup$

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.

$\endgroup$
10
  • 3
    $\begingroup$ Music has been thoroughly digitized, but that has not put all musicians out of business. $\endgroup$
    – Matt F.
    Dec 9 '20 at 22:06
  • $\begingroup$ @MattF. : But in 100 years, perhaps we'll all have folded hands, that don't even play music. $\endgroup$ Dec 9 '20 at 22:56
  • 4
    $\begingroup$ It's not going to take 100 years... $\endgroup$ Dec 10 '20 at 9:01
  • 1
    $\begingroup$ ... and then years later people may want to apply what is stated in print rather than "what was in the heads of the experts" $\endgroup$
    – Yemon Choi
    Dec 10 '20 at 21:12
  • 1
    $\begingroup$ @TimothyChow My understanding is that Kevin's Lean Math group has had to rewrite its category theory library several times because of this kind of thing. $\endgroup$ Jan 17 at 17:44
16
$\begingroup$

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.

$\endgroup$
1
8
$\begingroup$

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.

$\endgroup$
7
  • 3
    $\begingroup$ As an absolute non-expert, let me make some comments. 1. Natural language is ambiguous. Any attempt to make it unambiguous is bound to make the language more "mechanical". Sure some basic things like "let" can be simplified, but quickly it will be less feasible. 4. You are asking for (what in Lean at least is called) tactics. Many such exist, for instance there is one which will automatically prove any identity in the language of commutative rings. 5. This is already (to an extent) happening. However, the entry barrier is high, so almost everyone is first working out the basics.. $\endgroup$
    – Wojowu
    Dec 9 '20 at 22:51
  • 4
    $\begingroup$ Overall though, I do agree with the sentiment that there is some work left to be done to make proof assitants more mathematician-friendly. Kevin Buzzard is very vocal in expressing his frustration when first learning Lean and how the documentation was written "by computer scientists for computer scientists". One has to remember though that someone has to build those programs, and someone with nearly enough programming proficiency to more than likely to come from CS background than math one. $\endgroup$
    – Wojowu
    Dec 9 '20 at 22:55
  • 2
    $\begingroup$ In terms of proofs that look more like natural language, the proof assistants based on set theory tend to be more readable; see the Mizar examples in Freek Wiedijk's Notices article. Also, set-theoretic proof assistants arguably are closer to mathematicians' intuition. I discuss some of the objections to set-theoretic proof assistants in another MO answer. $\endgroup$ Dec 9 '20 at 23:35
  • 3
    $\begingroup$ Historical minutiae: When the BASIC programming language first appeared in 1964, defining a new object (variable) did in fact require the keyword "LET", for precisely the math-idiom reasons seen here. But over time that was considered burdensome, and the use of LET was made optional and then dropped (instead, the first time a new variable is seen it's assumed to be declared). dartmouth.edu/basicfifty/commands.html $\endgroup$ Dec 10 '20 at 3:33
  • 2
    $\begingroup$ I don't think being based on set theory has anything to do with what input syntax provers offer. Isabelle also has declarative proof syntax, which is probably still quite a bit away from what you are looking for, but certainly closer than most systems. (see the examples here). $\endgroup$ Dec 10 '20 at 7:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.