ICM 2022. Kevin Buzzard: The Rise of Formalism in Mathematics

In this post I would like to report on Kevin Buzzard’s spectacular lecture on moving mathematics toward formal mathematical proofs.  (Here are the slides.) The picture above is based on images from the other spectacular Saturday morning lecture by Laure Saint-Raymond. The issues raised in Laure’s talk regarding fluctuations, atypical behavior, and chaos are rather close to my heart and recent interests.

Let me mention that in ICM2022 discord was used for question and answers (in addition, some of the lectures in front of live audience had a lovely Q/A part), and Kevin’s lecture led to many live questions and questions on discord.

Can we widely formalize and use computer to check mathematical proofs?

Kevin’s lecture gives strong evidence that the answer is yes! Here is an analogy, until a few decades ago typing a paper usually involved handwriting it, giving it to a typist, and then making a few tedious rounds of corrections. This has changed and now most mathematicians type their own papers. It seems quite possible that in a couple of decades mathematicians will write their proofs in a way which allows automatic verification.   

Kevin Buzzard !

A demonstration of how it works

Kevin demonstrated a verification of a proof to a theorem in topology asserting that the composition of two continuous functions is continuous. The demonstration was a little quick for me (I don’t know “Lean”) but it looked very convincing. You can see in real time how Lean replaces the term “continuous” with its definition and how the steps of the proofs enter Lean’s “brain”. Following this demonstration Kevin also showed a couple of short-cuts, using so-called “tactics” based on tricks or facts that the program already know. (The second short-cut was based on the theorem already there in the library.) At the end of each proof the program asserts “goals accomplished”  with an emoji of a flower. 

Proving theorems, Kevin said, turns into a nice computer game. Kevin also described the prehistory; indeed the example above could been achieved by systems from the 90s.

What was achieved so far?

This was the main part of Kevin’s lecture and the progress is mind-boggling.

Part 1: Before 2018

2004: A formal proof of the prime number theorem (Avigad et al using “Isabelle/HOL”, not having complex analysis it verified an elementary proof.) In 2009 Harrison verified the complex analysis proof.

2004: Gonthier formally verified the four-color theorem (using “Coq”)

2005: Hales verified the Jordan curve theorem (“Isabelle/HOL”)

2013: Gonthier et al formally verified Feit and Thompson’s odd order theorem

###

2015: Hales and a team found a formalized proof for the Kepler conjecture  (that he and Furgeson had proved in 1998).  Hales’ 2017 lecture on this proof changed Kevin’s life and led him to his work on formal proofs. Hales proposed to create a system capable of “understanding” all statements of theorems published in serious mathematical journals. (Understanding statements is easier than understanding proofs.)

First, Kevin said, one needs to formalize all the statements of undergraduate mathematics. 

###

In 2017 Kevin started a Lean club for undergraduates! They did very well. The lean community (I suppose Lean is used for other things) embraced this project. 

Introduced by Grothendieck in 1960, schemes made understandable to computers by Lean in 2018. (Schemes and especially schemes of line-bundles are needed for understanding Kazhdan’s lecture from the previous post. I personally have a vague understanding of what they are. BTW, the lecture mentions Scott Morrison as a Lean star and I wondered if this is the MathOverflow star by the same name.) 

###

Next, Kevin mentioned the progress related to Scholze’s perfectoid spaces. Earlier, very complicated proofs to simple-to-state theorems were formalized and this was a formalization of very simple theorems on very complex objects. It was also a nice way to learn the definition! 

&&&

Part II after 2018

Lean and even its mathematical library “mathlib” are by now gigantic project and Kevin made it clear that it’s not “his” project but rather that he is one of many, many participants.

2020: The Scholze challenge (we talked about it in this post, and in any case it is way over my head). This is an example of formalizing a very complex proof of a very complex theorem. It eventually led to a somewhat different proof and better understanding of the necessary underlying objects.

2018: A new proof by Gouezel and Shchur for a 2013 theorem by Shchur whose formalization led to finding an error and then correcting it.

2019 the proof of the 2016 cap set conjectures (see this post) was formalized.

2021 Bloom proved that every dense set of integers contains a finite subset where the sum of reciprocals equals 1. The proof  was formalized by Bloom and Bhavik Mehta (including all earlier results the paper relies on and including the circle method).

2019 Apery’s proof of the irrationality of zeta (3) was formalized.

Let me stop here, there were 20-30  more startling successes for which I refer you to the talk itself. Fermat’s last theorem, Poincare’s conjectures in dimensions 4 and 3 and the classification of finite simple groups are still waiting for their turn and of course so are many more less famous proofs. Kevin refers to it as a new era of digitizing mathematics.

Other issues regarding formal mathematical proofs

Did the movement to formal proofs gain enough attention/recognition in the mathematical community?

Kevin complained about this matter (every appearance of ### above) but I tend to disagree with this complaint. Formal proofs did gain a lot of attention and, in any case, the appropriate response if you do not get attention is “to work harder” which incidentally is also (on the nose) the appropriate response if you do get attention. Also, Robert Aumann often says that in science, like in other areas, salesmanship accounts for more than 50% of success, and indeed Kevin mentioned that salesmanship was among the motivations of one of their projects (&&& above).

Are there many cases that in the process of formalization the proof turned out to be wrong?

The lecture mentioned a single case for which the proof was corrected. It will be surprising (perhaps even suspicious) if upon formalization, 99% of proofs turn out to be correct. (And there are interesting issues on what to do with theorems and proofs that we cannot verify formally.)

Are the formal proofs absolutely reliable?

This is something I asked about in discord and it led to interesting comments. (It is related to the previous question.) Kevin mentioned, for example, that initially the proof of the irrationality of zeta (3) proved a different statement.

Are formal proofs useful for teaching mathematics?

Probably, yes! This is an interesting issue worthy of further discussion.

What about combinatorics?

This is also something I asked about over discord. I was referred to the following link:  Combinatorics in lean.

Can we use the formal methods to make the computer understand incomplete mathematical approaches, and vague mathematical ideas? 

I suppose that the answer is positive. This would be a nice project.

Can human proofs be automatically transferred into formal proofs?

This does not seem out of the question, but having such a “compiler” will require also different AI abilities that go well beyond current efforts.

Can computers replace humans in doing mathematics and especially in proving theorems?

Kevin started his lecture by answering “NO” and referring to such a possibility as “science fiction”. The way I see it is that there are various avenues towards computerizing (what we regard now as) the creative process of mathematics including coming up with conjectures, proving theorems, and building theories, and formalizing mathematical theorems and proofs besides its own value can also be regarded as an avenue (among several) in automatizing mathematics.

Kevin asserted that he is not impressed by current successes, but people could equally be unimpressed with formalizing mathematics in 2010, and he mentioned some reasoning coming from AI for why it is difficult (which I could not understand). On the other hand, since he regarded the state of the project as “the beginning of the beginning” it may be the case that Kevin does think about tasks which go beyond “just” formalizing mathematics.

There are various other skeptical voices regarding the possibility of replacing humans with computers in mathematical research, including the famous mathematician Michael Harris who often writes about it, but I am not familiar with the skeptical arguments themselves.

There are many people who are enthusiastic about replacing humans with computers in doing mathematics and few of them even put their careers where their mouth is. Doron Zeilberger (aka, Doron Z. and Dr. Z) is a very famous example. Now, with the next 2026 ICM in Philadelphia, we can say that:

If Doron Z. does not come to the ICM, the ICM comes (pretty close) to Doron Z,

and it will be nice to see various aspects regarding the interface between mathematics and computers represented in ICM 2026.

Regarding the use of computers in major mathematical achievements see these two Math Overflow questions (one, two).

 

Another link from the discussion: Solving (Some) Formal Math Olympiad Problems

A description of a Lean project in progress. The green ellipses represent completed parts. I am a little worried by the ellipse where it is written “clearly” and also by the one with the title “it is easy to see” 🙂 .

Updates:

1) Doron Zeilberger, a pioneer in using computers for mathematics, wrote a skeptical opinion regarding the formal proof direction https://sites.math.rutgers.edu/~zeilberg/Opinion184.html . Twelve years ago he wrote a similar opinion .   

2) Georges Gonthier, an early hero on formal proofs gave another ICM 2022 lecture: Computer proofs: teaching computers mathematics, and conversely.