Editor's note: Formalism, as one of the three major schools of thought in the history of mathematics, has experienced many ups and downs. But now, with the rise of artificial intelligence, machine learning, and the joint efforts of the open source community, computers are used to solve Mathematical Olympiad problems, check whether there are errors in the mathematical proof process, and even automatically discover and formally prove mathematical theorems. What sparks will collide in theory and practice, and how will they be constrained by Gödel's incomplete theorem. Professor Kevin Buzzard provided some information and insights for your reference in his one-hour report speech at the 2022 International Congress of Mathematicians (also see Quantum Magazine’s interview podcast with Kevin Buzzard previously compiled by zzllrr Xiaole, and Lean’s introduction)
Time: 2022-7-9 Saturday Special Plenary Lecture Special Conference Report
Speaker: Professor Kevin Buzzard, Imperial College London
Preface to the speech:
Teaching formalization of proofs to ordinary mathematicians. Summary: Formalism is the art of writing down what you really mean. Mathematics has a rich history of formalization: Euclid, Russell-Whitehead, and Bourbaki all attempted it. This century, Avigad, Hales and Gonthier show us another way. Now, a new generation of young people is formalizing algebra, analysis, category theory, combinatorics, geometry, number theory, topology, etc., this time using computers. Lean's math library mathlib contains nearly one million lines of free open source code, corresponding to more than 80,000 proofs of theorems, such as the fundamental theorem of Galois's theory, and it is growing rapidly. An AI trained on a math library has solved International Mathematical Olympiad IMO problems on its own. What's happening? This is not about making sure the paper is correct. This is not about making a computer program that prints out a billion-line proof of the BSD conjecture (Birch and Swinnerton-Dyer) using only mathematical axioms. This is not about extracting beauty from the proof, leaving only a directed acyclic graph. It's about developing computer tools that have the potential to help researchers and PhD students in new ways. There is still much work to be done. I will provide an overview of this area.
Speech PPT text:
The rise of mathematical formalism.
Kevin Buzzard, Imperial College London
July 9, 2022, International Congress of Mathematicians
before we start
Thank you to the organizer for the invitation and everyone for coming!
Mathematics and Computers
For 60 years, computers have been superior to humans in computing.
They've been better than us at chess for 25 years.
For a few years, they performed better than we did.
When will they become better at proving theorems than us?
Screenshots of two reports from nature magazine
Mathematicians welcome computer-aided proof of 'grand unified' theory
·DeepMind’s AI helps unravel the knots of mathematics
The beginning of the end?
Will computers soon be better than humans at proving research-level mathematical theorems?
Are our jobs as mathematics researchers at risk?
No. (in my opinion).
The beginning of the beginning.
But will computers soon help humans prove theorems?
Not just by example, but by reasoning?
Looking for proofs or counterexamples in databases, constructing simple proofs yourself, pursuing graphical representations?
Will computers make it easier for humans to learn math?
Will they allow humans to explore evidence in new ways?
My guess: yes.
Summary of conversation
-
Live demonstration of computer theorem prover
-
Some history of the field
-
state of the art technology
-
How to participate
What is a computer certification assistant?
We're about to see Lean in action.
Many other such systems exist (Coq, Isabelle/HOL, HOL Light, Agda, cubical Agda, Metamath, Mizar...).
You can use such systems to formalize mathematical proofs.
There are also automatic theorem provers such as Prover9, Otter, E, Waldmeister, Vampire...
https://gitpod.io/#https://github.com/leanprover-community/mathlib
What did we just see?
We all know that computers can be used to calculate.
We just saw that they can now be used for reasoning.
Proof Assistant: Turn math problems into computer puzzle game levels.
We just saw them doing undergraduate level topology.
Are these just toys?
History (before 2000)
1970s: The first computer-verified construction of real numbers as a complete ordered field (Jutting's paper).
1990s: Simple theorem proofs where the system can check human input (undergraduate level).
History (21st century)
Some milestones of the 2000s:
-
2004: Avigad et al. formally verified the prime number theorem in Isabelle/HOL (also Harrison 2009 in HOL Light).
-
2004: Gonthier formally verified the four-color theorem.
-
2005: Hales formally verified the Jordan Curve Theorem in Isabelle/HOL.
-
2013: Gonthier et al. formally verified the odd-order theorem in Coq.
Reaction from the mathematical community was minimal.
I hope the results I'm going to talk about today will have a greater resonance.
Kepler's conjecture
In 1998, Hales and Ferguson proved Kepler's conjecture (the optimal density for the packing of 3-dimensional spheres).
Part of the proof involved checking 23,000 nonlinear inequalities on a computer. (Note that Viazovska's work in 8 and 24 dimensions is more conceptual).
Five years later, Annals of Mathematics told Hales that reviewers could not fully prove the proof.
Hales's remarkable reaction: He assembled a team of more than 20 people and spent the next 12 years formalizing the results in an interactive theorem prover.
They succeeded in 2015.
Hales' conclusion
Hales, now an expert in the field, told the Newton Institute about the July 2017 story.
https://www.newton.ac.uk/seminar/21474/
https://api.newton.ac.uk/website/v0/seminars/21474/presentation-files/250
He concluded that the following projects are now feasible:
Create a system that understands the statements of all theorems currently published in serious pure mathematics journals.
Easier to state than to prove!
Presentation is a necessary first step.
If computers can't even understand the question, how can they help us find the answer?
harder than it looks
To formalize the statement of research-level mathematics for 2022, we would be better off first formalizing the full undergraduate degree content.
If you don't have definitions for smooth manifolds, vector bundles, classes, and various basic homology and cohomology theories (singular cohomology, de Rham cohomology...) in your prover, what chance do you have?
Because our community has been largely uninterested in this work, no system in 2017 has these definitions. It's our fault.
more recent history
In 2017, I founded a Lean club called the Xena Project at Imperial College London.
The goals are (a) to teach undergraduate students how to use the software, and (b) to formalize parts of our undergraduate coursework.
Students soon wanted to take on projects in finite group theory, and then more ambitious projects.
The Lean community welcomes us in and teaches us how to use the software.
They invited us to help build a Lean math library called mathlib.
Undergraduate mathematicians define linear maps, matrices, subgroups, ... and add them to Lean's math library.
Concept
In the 1960s, Grothendieck revolutionized algebraic geometry by introducing the concept of schemes.
In 2018, some undergraduate students from the club (Kenny Lau, Chris Hughes, Amelia Livingston, Ramon Fernández Mir) and I defined profiles in Lean.
We then started doing exercises in Hartshorne's algebraic geometry textbook.
It's harder than you think, but not too hard.
The Lean community encouraged us to publish (we did, and Scott Morrison redefined everything using the language of "categories").
But we still need more to impress mathematicians.
perfect space
In 2018, Peter Scholze won the Fields Medal.
This was partly due to his work on Perfectoid spaces.
In 2019, Johan Commelin, Patrick Massot, and myself formalized the definition of perfect spaces in Lean.
Why do we formalize perfect space?
-
A new way of using software (simple theorems about complex objects, rather than complex theorems about simple objects).
-
Check whether modern computer proof systems can handle such complex definitions.
-
A fun way to learn definitions correctly.
-
Publicity stunt.
But it worked: It brought the field to the attention of more mathematicians.
Lean is not me
Lean is not my "Kevin Buzzard project," and neither is its math library.
Lean's math library mathlib is a huge collaborative project.
This is a massive undergraduate mathematics database built by hundreds of volunteers and led by the Lean prover community, of which I am only a small part.
recent projects
Now I'm going to take a quick look at a list of some math that people in the theorem prover community have been doing lately, mostly at the graduate level.
Liquid tensor experiment
In December 2020, Peter Scholze challenged the theorem prover community to verify liquid
Fundamental theorem of volume vector spaces (proven by Clausen and Scholze):
For i≥1, there is
This is a technical result concerning higher-dimensional generalizations in the category of condensed Abelian groups.
Six months later, a team led by Johan Commelin formalized in Lean a proof of the key technical lemma that Scholze believed was at the heart of the problem.
The community (Commelin, Topaz, and many others) is about to get the job done.
What did we learn from this work?
First, Commelin greatly simplified one part of Clausen-Scholze's proof (the "Commelin complex").
Second, Scholze claims that the experience taught him “what exactly makes a proof effective.”
". . . it made me realize that the key thing that was actually happening was that the non-convex problem on the real numbers was reduced to a convex problem on the integers."
Third, we see that the system can now handle complex proofs of complex objects.
2013:Vladimir Shchur proved a quantitative version of Morse's lemma for Gromov hyperbolic spaces.
The proof is published in the Journal of Functional Analysis.
Sébastien Gouëzel attempted to formalize the results in Isabelle/HOL but discovered a fundamental error.
Gouëzel and Shchur discovered a new (more complex) proof.
2018:(Their) joint paper with better estimates, and a fully formalized proof.
2016:Ellenberg and Gijswijt solved the Cap Set conjecture (in affine geometry, the largest subset of n-dimensional affine space on the ternary field, no 3 elements are on the same line).
https://en.wikipedia.org/wiki/Cap_set
The work was published in Annals of Mathematics.
2019,Dahmen, Hölzl, and Lewis formalized the proof in Lean.
December 2021:Thomas Bloom proved that a set with positive upper density contains a finite subset S such that the sum of the reciprocals of all elements in the subset is 1
This conclusion answers a question posed by two famous late mathematicians, Erdös and Graham.
He then learned how to use Lean through Bhavik Mehta, a doctoral student of Sir Gowers Gowers of Cambridge University, winner of the 1998 Fields Medal and author of The Princeton Companion to Mathematics.
6 months later,Bloom and Mehta fully formalized this proof in Lean.
This work contains the formalization of an instance of the Hardy-Littlewood circle method.
Bloom's paper is still under review.
2021:Baanen, Dahmen, Narayanan, and Nuccio formalized Dedekind fields and corresponding taxa in Lean.
They also formalized the proof that the overall domain of taxa is finite.
2022:de Frutos Fernández formalized adeles and ideles over the domain of wholes in Lean.
She proved the relationship between ideal groups and ideal ideal groups.
Sebastian Monnet formally defines the Krull topology on the Galois group and proves that it is finite.
de Frutos Fernández then states the main conjectures of global class field theory in a non-cohomological form.
over the past few months, Livingston defined group cohomology and Galois cohomology.
She is currently working on cohomology forms expressing local and global theorems.
De Frutos Fernandez outlined a method for formalizing the proofs of the main theorems of local class domain theory, which was a natural next project.
Narayanan is currently studyingIwasawa Theory。
She has defined p-radical L-functions and is currently proving that their special values are related to generalized Bernoulli numbers.
Gouëzel, Kudryashov, Macbeth, Degenne, and Ying have formalized analysis and probability in Lean.
Notable recent results include the law of large numbers, changes in variables in multivariable calculus, Lebesgue's differential theorem, Cauchy's integral theorem, andMartingale(martingales) definition and basic properties.
2020,Commelin and Lewis formalized the Witt vector ring W(R) of the commutative ring R.
Using their work, de Frutos Fernández is working on the definition of Fontaine rings such as B_{dR}
The natural next step: exponentiated ideals and B_{cris}.
Also in p-adic Hodge theory: Dupuis, Lewis and Macbeth classified one-dimensional isocrystals on algebraically closed fields with positive characteristics.
1999:Warwick Tucker proved that the Lorenz attractor is chaotic.
Tucker's proof involved extensive calculations written in C++.
2017,Immler completed the formal verification of the calculations using Isabelle/HOL.
Scott Morrison has built a huge library of category theory (basic, monoid categories, etc.).
Commelin, Himmel, Morrison, Topaz, and Yang used it to establish Abelian categories, derivative functors, and homology algebra.
(This is essential for liquid tensor experiments).
Nash formalized Lie algebras in Lean and in the process proposed what appears to be a new, more conceptual proof of Engel's theorem.
2022:Jujian Zhang formalized projective schemes in Lean and is currently defining sheaf cohomology. Étale cohomology is definitely on the horizon (the underlying commutative algebra is also in a favorable stage).
I defined elliptic curves in Lean, and Birkbeck defined modular forms and stated the modular conjecture.
Karatarakis and I are slowly beginning our journey to find proof. This will take many, many man-years. Whether it takes many years depends largely on the number of people involved.
At the same time, Brasca was leading a project to formalize an old proof of Fermat's last theorem for regular primes.
You can monitor progress by viewing the dependency graph.
https://leanprover-community.github.io/flt-regular/dep_graph_document.html
1978:Apéry proved that ζ(3) is irrational.
2019,Mahboubi and Sibut-Pinote (after their earlier work with Chyzak and Tassi) formalized the proof in Coq.
2019:Manuel Eberl at Isabelle/HOL formalized most of the contents of Apostol's analytic number theory book.
Examples of what he did: the statement of the Riemann hypothesis, and the proof of Dirichlet's theorem regarding prime numbers in arithmetic series.
2021:Bordg, Paulson, and Li formalized the definition of schemes in Isabelle/HOL.
(Funny for basic reasons)
Mehta and Dillies formalized Szemerédi's regularity lemma and Roth's arithmetic series theorem in Lean, while Edmonds, Koutsoukou-Argyraki, and Paulson formalized the same results in Isabelle/HOL.
Many previous projects had a flavor of number theory or algebra.
This simply reflects the interest of mathematicians within the theorem prover community.
Massot, van Doorn and Nash's sphere eversion project was a non-trivial project in a completely different field.
Sphere eversion project
Theorem(Smale, 1950s): The sphere can evert.
There are videos online showing the construction visually. https://youtu.be/OI-To1eUtuU?t=95
Is it really possible to formalize such a result in a computer theorem prover?
Massot observed that what should be formalized was Gromov's h-principle, by convex integrals.
You can see their current progress here.
https://leanprover-community.github.io/sphere-eversion/blueprint/index.html
Join
An interesting starting point is a natural number game written for undergraduates at my university. https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
Many modern theorem provers have online communities on Discord or Zulip. For example:
• Coq: coq.zulipchat.com
• Lean: leanprover.zulipchat.com
• Isabelle: isabelle.zulipchat.com
• Agda: agda.zulipchat.com
future
They digitized music (CDs, MP3s), but no one at the time foresaw the consequences (Napster, Spotify).
We are digitizing mathematics, and I believe this will inevitably change mathematics.
Welcome to join us.
Thank you very much for your attention.
-
Click on the lower left corner "Read the original article”, view original article source.
-
Click "zzllrr Xiaole"Official account homepage, upper right corner"Set as star", Mathematics popularization will not get lost.
Machine-translated from the Chinese original 小乐数学科普：2022国际数学家大会一小时报告《数学形式主义的兴起》Kevin Buzzard 演讲全文 (published 2024-03-28). WeChat original ↗