2
$\begingroup$

I have been watching Terry Tao's lecture on machine-assisted proofs https://www.youtube.com/watch?v=AayZuuDDKP0&t=1460s. However in terms of the formalization of proofs via systems like Lean or Coq that Tao talks about I still do not really get the point of why this is important or what this is good for. I feel like Tao actually never specifies in an intuitive way why these very very advanced proofs need to be formalized.

This is because they are so difficult and dependent on so many assumptions, theorems, mathematical structures etc. right? They are too large basically to keep an overview? Is it this? Or there any other benefits that go beyond verification of systems too large to comprehend for a single individual?

Because I wonder, it would not be of benefit to formalize the proof for the fact that $\sqrt{2}$ is not a rational number, right? Just because it is so small and clear to most beginners even? Or would there also be any benefit in that case?

Mathematicians anyway check each other's proofs, and anyway we/they use a formal language for that, that is mathematics, so using the computer is basically just like having another mathematician on board for the proof who is better informed of all the necessary steps. Is that interpretation correct? Or am I missing something fundamental?

$\endgroup$
4
  • $\begingroup$ I don’t think there is something like ‘the’ reason or a number of reasons that are the ‘right’ reasons. But sure, there are reasons we do this. And a big one is the one you mention: sometimes proofs do get so complicated or long and tedious that a computer can really help $\endgroup$
    – Bram28
    Feb 11 at 12:10
  • 1
    $\begingroup$ Humans are easily fooled, or may overlook (incorrect) details. Therefore, one uses computers to formally verify that a proof is actually correct. If the computer (proof checker) is programmed correctly (which you only have to check once and not for every new proof that you check), this gives you are very high level of confidence. This gets more important the more important the result and the more involved the proof is. $\endgroup$
    – PhoemueX
    Feb 11 at 12:14
  • $\begingroup$ You may want to also watch Kevin Buzzard’s ICM talk. I think he gave more motivation? $\endgroup$
    – Aphelli
    Feb 11 at 12:19
  • 3
    $\begingroup$ My impression is that it’s useful simply to be sure that our proofs really are correct. Also we’re approaching a point where authors can formally verify a proof faster than reviewers can review it. So that could be a game changer for the publishing process. Another thought is that all these lean proofs become training data for language models which in the future could help us convert natural language proofs into lean proofs much more easily. $\endgroup$
    – littleO
    Feb 11 at 12:20

1 Answer 1

5
$\begingroup$

I don’t think there is something like ‘the’ reason or a number of reasons that are the ‘right’ reasons. But sure, there are reasons we do this.

A big one is the one you mention: sometimes proofs do get so complicated or long and tedious that a computer can really help to make sure the proof is correct.

For example, in the 1800's a number of 'proofs' of the four color theorem were offered that turned out to be incorrect .. but sometimes it took more than 10 years before we found the mistake. Presumably if we had tried to formalize it in the first place, we might have found those mistakes earlier.

Indeed, it can be easy for us humans to make mistakes. Think of the infamous 'proof' that all horses are the same color. It can initially be hard to spot the mistake in the proof. And when proofs get more complicated, it gets harder to spot any mistakes yet.

Indeed, you can imagine that after picking the 'low hanging fruit', mathematical proofs get more and more complicated, and I like to think that one impetus for the development of modern formal logic in the 1800's was because of the mistakes that started to occur more and more often.

I also want to note that even though providing a formal proof (whether computer-assisted or not) often feels like an after-the-fact formalization of a proof that we already firmly grasp 'in our head', we oftentimes do rely on symbolic systems to help us think about problems. Notational systems don't just express our already completed thoughts, but help us guide and organize our thinking. Without it, mathematics wouldn't be what it is today.

In this vein, I often wonder to what extent the very formalization of set theory led to Russell's Paradox, and thus to the realization that we can't just make a set out of 'anything you want'.

Other than helping with really complicated proofs, computers can also help us with just very long and tedious proofs. Again we can point to the four color theorem. In 1976 a very long proof was created that relied on checking a very large number of cases: too many for a human to feasibly do. So, they relied on a computer to systematically go through all those cases.

Interestingly, this proof was still looked at with some suspicion, since it wasn't grounded in a purely formal logic system like Coq or Lean. So in 2005 they managed to do the whole thing in such a logic-based proof system.

More recently a good example is the proof of the Sphere Packing Conjecture. In 1998 the mathematician Thomas Hales submitted a gigantic proof of this conjecture (involving lots of computer code) to a journal, but the referees (who did spend a good bit of time trying to work through it) came back and said that they were '99% sure' the proof was correct ... which of course is not acceptable to a mathematician! So then Hales and a team of other people spent a good number of years formalizing the proof in Isabella and HOL light, two other logic-based computer-assisted proof systems, and they completed this in 2014. A few years later, the journal then accepted this proof as well.

With these last 2 examples you might think: Why spend so much time on formalizing one specific proof? Well, especially when a logic-based approach is used, the eventual proofs that were generated are likely to be built up from various lemma's and sub-theorems that they also had to formalize. And those can now be used for other proofs as well.

And finally, some will find it just a fun challenge to try and formalize a proof, even if that it is as simple as the proof that the square root of 2 is an irrational number, or that there are infinitely many prime numbers ... and doing so again can sometimes provide some deeper insight as to how the proof works, what axioms it relies on , etc.

$\endgroup$
1
  • $\begingroup$ Another recent example is Clausen-Scholze’s “liquid tensor experiment”, which is not as voluminous as the sphere-packing or 4-color examples but still extremely technical. $\endgroup$
    – Aphelli
    Feb 11 at 12:25

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .