Plan used by Anthropic’s Claude to formalize Fermat’s Last Theorem; source: Anthropic
Introduction
In 1637, French mathematician Pierre de Fermat, while perusing a copy of Arithmetica, an ancient mathematical text by the Greek mathematician Diophantus, wrote in the margin (English translation): “It is impossible to separate a cube into two cubes, or a fourth power into two fourth powers, or in general, any power higher than the second, into two like powers. I have discovered a truly marvelous proof of this, which this margin is too narrow to contain.” In modern mathematical parlance, “No positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for any n > 2,” an assertion now known as Fermat’s Last Theorem (FLT).
The consensus of modern mathematicians is that Fermat almost certainly did not have a complete, valid proof, since after his claim became known it resisted 358 years of determined efforts by mathematicians worldwide. For many years its proof was widely regarded as the premier unsolved problem of mathematics.
The first complete and valid proof Fermat’s Last Theorem was published by Oxford mathematician Sir Andrew Wiles in 1995. It was some 129 pages long, relied on many previously published results, and required months of painstaking work to verify. The first version of his proof, submitted in 1993, was subsequently found to be in error, requiring a collaboration with his former student Richard Taylor before a complete and fully valid proof was finished. Numerous mathematical and historical details are available in this Wikipedia article and in Simon Singh’s book.
Formal verification of the Kepler conjecture
In recent years, researchers have pursued the formal verification of much of the traditional corpus of mathematical knowledge. Researchers enter every step of a mathematical proof, using software such as Lean, which then verifies the proof in exhaustive detail down to the most basic axioms of mathematics. Just one of many examples that could be cited is the verification of the Kepler conjecture, namely the assertion that the simple scheme of stacking oranges in a supermarket has the highest possible average density.
In the early 1990s, Thomas Hales determined that the maximum density of all possible arrangements could be obtained by minimizing a certain function with 150 variables, and set out to construct a proof. In 1998, Hales and his graduate student Samuel Ferguson, son of famed mathematician-sculptor Helaman Ferguson, announced that their project was complete, documented by 250 pages of notes and three Gbyte of computer code, data and results.
Hales’ computer-assisted proof generated some controversy — the journal Annals of Mathematics originally demurred, although ultimately accepted his paper. In the wake of this controversy, Hales decided to embark on a collaborative effort to certify the proof via automated techniques. This project, named Flyspeck, employed the proof-checking software HOL Light and Isabelle. The effort commenced in 2003, but was not completed until 2014.
In the years since the proof and verification of Kepler’s conjecture, proof-checking software has advanced considerably. Today the most widely used platform is Lean. As of this date, a large corpus of mathematical knowledge has been encoded in Lean, certainly including all of the theorems typically studied in undergraduate mathematics courses, and many advanced topics as well. However, using Lean is a laborious process, even in the hands of highly trained researchers. Thus some mathematicians have explored using agent-based AI software to accelerate the process. This has raised the question: How far can these technologies go?
Formal verification of Fermat’s Last Theorem
In a development that has shocked the mathematical community, a team of researchers at the AI firm Anthropic announced that Claude, Anthropic’s agent-based AI software, has completed a full computer-checked formal verification of Fermat’s Last Theorem, in an effort that required only 11 days. Their formalization consists of 13 million lines of Lean, organized into 29,500 intermediate theorems. It is easily the largest Lean-based proof ever written.
This success has startled researchers in the field, who had not expected a computer-verified proof of FLT to be completed in the foreseeable future. Just a few weeks ago, a team led by Kevin Buzzard of Imperial College London had initiated a project to formalize FLT, with the task expected to take at least five years.
Buzzard acknowledged that the new proof appears to be both valid and complete, leaving “no assumptions other than the axioms of mathematics.” As he elaborated,
Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered. … If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature. Such autoformalization techniques will lead to new tools, rooting out errors in the current mathematical corpus and lightening the load of referees. The techniques will also enable us to rigorously check LLM [large language model]-generated mathematics, which is currently typically an extremely costly human-led process.
Some additional details on Anthropic’s achievement are available here. See also the graphic above.
Terence Tao on proof checkers, AI and the future of mathematical research
UCLA Fields Medalist mathematician Terence Tao recently discussed (prior to Anthropic’s announcement) the current status of computer tools in mathematical research, including proof-checking software such as Lean and AI-based tools such as Claude. Here are some excerpts from this interview (see also here):
Drosser: With the advent of automated proof checkers, how is [the trust between mathematicians] changing?
Tao: Now you can really collaborate with hundreds of people that you’ve never met before. And you don’t need to trust them, because they upload code and the Lean compiler verifies it. You can do much larger-scale mathematics than we do normally. When I formalized our most recent results with what is called the Polynomial Freiman-Ruzsa (PFR) conjecture, [I was working with] more than 20 people. We had broken up the proof in lots of little steps, and each person contributed a proof to one of these little steps. And I didn’t need to check line by line that the contributions were correct. I just needed to sort of manage the whole thing and make sure everything was going in the right direction. It was a different way of doing mathematics, a more modern way.
Drosser: German mathematician and Fields Medalist Peter Scholze collaborated in a Lean project — even though he told me he doesn’t know much about computers.
Tao: With these formalization projects, not everyone needs to be a programmer. Some people can just focus on the mathematical direction; you’re just splitting up a big mathematical task into lots of smaller pieces. And then there are people who specialize in turning those smaller pieces into formal proofs. We don’t need everybody to be a programmer; we just need some people to be programmers. It’s a division of labor.
[Continuing after some skip:]
Drosser: I heard about machine-assisted proofs 20 years ago, when it was a very theoretical field. Everybody thought you have to start from square one — formalize the axioms and then do basic geometry or algebra — and to get to higher mathematics was beyond people’s imagination. What has changed that made formal mathematics practical?
Tao: One thing that changed is the development of standard math libraries. Lean, in particular, has this massive project called mathlib. All the basic theorems of undergraduate mathematics, such as calculus and topology, and so forth, have one by one been put in this library. So people have already put in the work to get from the axioms to a reasonably high level. And the dream is to actually get [the libraries] to a graduate level of education. Then it will be much easier to formalize new fields [of mathematics]. There are also better ways to search because if you want to prove something, you have to be able to find the things that it already has confirmed to be true. So also the development of really smart search engines has been a major new development.
Drosser: So it’s not a question of computing power?
Tao: No, once we had formalized the whole PFR project, it only took like half an hour to compile it to verify. That’s not the bottleneck — it’s getting the humans to use it, the usability, the user friendliness. There’s now a large community of thousands of people, and there’s a very active online forum to discuss how to make the language better.
Drosser: Is Lean the state of the art, or are there competing systems?
Tao: Lean is probably the most active community. For single-author projects, maybe there are some other languages that are slightly better, but Lean is easier to pick up in general. And it has a very nice library and a nice community. It may eventually be replaced by an alternative, but right now it is the dominant formal language.
[Continuing after some skip:]
Drosser: So far, the idea for the proof still has to come from the human mathematician, doesn’t it?
Tao: Yes, the fastest way to formalize is to first find the human proof. Humans come up with the ideas, the first draft of the proof. Then you convert it to a formal proof. In the future, maybe things will proceed differently. There could be collaborative projects where we don’t know how to prove the whole thing. But people have ideas on how to prove little pieces, and they formalize that and try to put them together. In the future, I could imagine a big theorem being proven by a combination of 20 people and a bunch of AIs each proving little things. And over time, they will get connected, and you can create some wonderful thing. That will be great. It’ll be many years before that’s even possible. The technology is not there yet, partly because formalization is so painful right now.
Drosser: I have talked to people that try to use large language models or similar machine-learning technologies to create new proofs. Tony Wu and Christian Szegedy, who recently co-founded the company xAI, with Elon Musk and others, told me that in two to three years mathematics will be “solved” in the same sense that chess is solved — that machines will be better than any human at finding proofs.
Tao: I think in three years AI will become useful for mathematicians. It will be a great co-pilot. You’re trying to prove a theorem, and there’s one step that you think is true, but you can’t quite see how it’s true. And you can say, “AI, can you do this stuff for me?” And it may say, “I think I can prove this.” I don’t think mathematics will become solved. If there was another major breakthrough in AI, it’s possible, but I would say that in three years you will see notable progress, and it will become more and more manageable to actually use AI. And even if AI can do the type of mathematics we do now, it means that we will just move to a higher type of mathematics. So right now, for example, we prove things one at a time. It’s like individual craftsmen making a wooden doll or something. You take one doll and you very carefully paint everything, and so forth, and then you take another one. The way we do mathematics hasn’t changed that much. But in every other type of discipline, we have mass production. And so with AI, we can start proving hundreds of theorems or thousands of theorems at a time. And human mathematicians will direct the AIs to do various things. So I think the way we do mathematics will change, but their time frame is maybe a little bit aggressive.
Drosser: I interviewed Peter Scholze when he won the Fields Medal in 2018. I asked him, How many people understand what you’re doing? And he said there were about 10 people.
Tao: With formalization projects, what we’ve noticed is that you can collaborate with people who don’t understand the entire mathematics of the entire project, but they understand one tiny little piece. It’s like any modern device. No single person can build a computer on their own, mine all the metals and refine them, and then create the hardware and the software. We have all these specialists, and we have a big logistics supply chain, and eventually we can create a smartphone or whatever. Right now, in a mathematical collaboration, everyone has to know pretty much all the mathematics, and that is a stumbling block, as [Scholze] mentioned. But with these formalizations, it is possible to compartmentalize and contribute to a project only knowing a piece of it. I think also we should start formalizing textbooks. If a textbook is formalized, you can create these very interactive textbooks, where you could describe the proof of a result in a very high-level sense, assuming lots of knowledge. But if there are steps that you don’t understand, you can expand them and go into details — all the way down the axioms if you want to. No one does this right now for textbooks because it’s too much work. But if you’re already formalizing it, the computer can create these interactive textbooks for you. It will make it easier for a mathematician in one field to start contributing to another because you can precisely specify subtasks of a big task that don’t require understanding everything.
[Continuing after some skip:]
Drosser: By breaking down a problem and exploring it, you learn a lot of new things on the way, too. Fermat’s Last Theorem, for example, was a simple conjecture about natural numbers, but the math that was developed to prove it isn’t necessarily about natural numbers anymore. So tackling a proof is much more than just proving this one instance.
Tao: Let’s say an AI supplies an incomprehensible, ugly proof. Then you can work with it, and you can analyze it. Suppose this proof uses 10 hypotheses to get one conclusion — if I delete one hypothesis, does the proof still work? That’s a science that doesn’t really exist yet because we don’t have so many AI-generated proofs, but I think there will be a new type of mathematician that will take AI-generated mathematics and make it more comprehensible. Like, we have theoretical and experimental science. There are lots of things that we discover empirically, but then we do more experiments, and we discover laws of nature. We don’t do that right now in mathematics. But I think there’ll be an industry of people trying to extract insight from AI proofs that initially don’t have any insight.
Drosser: So instead of this being the end of mathematics, would it be a bright future for mathematics?
Tao: I think there’ll be different ways of doing mathematics that just don’t exist right now. I can see project manager mathematicians who can organize very complicated projects — they don’t understand all the mathematics, but they can break things up into smaller pieces and delegate them to other people, and they have good people skills. Then there are specialists who work in subfields. There are people who are good at trying to train AI on specific types of mathematics, and then there are people who can convert the AI proofs into something human-readable. It will become much more like the way almost any other modern industry works. Like, in journalism, not everyone has the same set of skills. You have editors, you have journalists, and you have businesspeople, and so forth — we’ll have similar things in mathematics eventually.
The full text of the interview is available here.