Fermat's Last Theorem proved by AI | Lex Fridman

Video authored by the channel shown, not by IANIA; all rights belong to the creator. Transcript and summary generated automatically; the original-language content is preserved.

Original language: English

Original video: Fermat’s Last Theorem proved by AI | Lex Fridman · Channel: Lex Clips · 07:55 · Watch on YouTube

Topics: AI evaluation and benchmarks, AI models, Open source and software ecosystems

Summary

A mathematician describes being stunned when AI systems produced a sorry-free Lean formalization of Fermat’s Last Theorem, far sooner than he expected. The proof consisted of about 13 million lines and, while valid, was not yet a clean, Mathlib-quality proof. He contrasts this result with the difficulty of organizing formal mathematics into a reusable, elegant library and says the AI’s achievement exceeded his expectations by an enormous margin. He concludes that producing formal proofs of human-written mathematical statements may be essentially solved, even though developing beautiful libraries and supporting human understanding remain substantial challenges.

Key points

The Fermat’s Last Theorem formalization in Lean comprised about 13 million lines of code.
Mathlib aims for proofs built from canonical, reusable results, while current AI systems are not yet good at canonizing and refactoring code.
Before this result, the speaker expected formalizing work far beyond Mathlib’s existing coverage to take years.
The speaker says Kevin Buzzard had a grant to work toward reducing the formalization to mathematics known by the 1980s.
Anthropic’s AI systems produced a sorry-free proof, but it was described as a jerry-rigged result rather than a clean Mathlib-quality proof.
The speaker recalls that two or three humans were involved and believes most of their input was simply encouraging the system to continue.
His prior experience suggested AI could help with Lean library search but could not scale its abilities by an order of magnitude; this result was far beyond his expectations.
He considers autoformalization of human-written mathematical statements essentially solved, while emphasizing that building a high-quality mathematics library remains difficult and ongoing.

Chapters

Start	Chapter	Summary
00:02	Why the result was so unexpected	The speaker introduces his surprise at the rapid Lean formalization and explains Mathlib’s goals and the limits he had observed in AI-assisted formalization.
02:07	The expected timeline and the 13-million-line proof	He describes the work expected to be needed for Fermat’s Last Theorem and recounts how a sorry-free formal proof appeared just days after his colloquium.
03:13	How the formal proof was produced	The speakers discuss Anthropic’s result, its sprawling and non-canonical character, and how rapidly changing AI capabilities can make expert predictions wrong.
04:16	Prior experience with AI and human involvement	The mathematician recalls AI’s gradual improvement at Lean library search and discusses the reported human role in producing the proof.
05:50	What autoformalization means for mathematics	The conversation considers possible undisclosed groundwork, the speaker’s reaction to the result, and his view that formalizing paper-written statements is now essentially solved.

Quotes

And everything I said in that colloquium was wrong. — 02:40

they had a sorry-free formal Lean proof of Fermat’s Last Theorem. — 03:44

It was just completely outside of the distribution in my mind of what systems were capable of. — 05:18

I think that problem is done. — 07:24

Concepts and entities

Fermat’s Last Theorem, Lean, Mathlib, Anthropic, Kevin Buzzard, Andrew Wiles, Richard Taylor, autoformalização, Navier–Stokes equations

Full transcript (original language)

00:02 And this is– It’s been a month of things happening way outside of my model of what was possible. The Fermat’s Last Theorem formalization, I was sure we were three years away, at least, from being able to do something like that. - So, maybe you can elaborate on that. It was in Lean, it was formalized as… How big was the Fermat’s Last Theorem in Lean? - Like, 13 million lines. - 13 million lines. Okay. - So I just– Two days before, I gave a colloquium in the Princeton Math Department where I explained in painstaking detail what Lean is, what Mathlib is, but also

00:33 that AI systems today, you know, there’s this Mathlib library where everything is kind of perfectly done, exactly the right levels of generality, enough– There’s no– There’s not supposed to be any code that’s reusing code that’s reproving theorems somewhere else. Everything is the most general, the most abstract, and what AI systems are capable of doing is building, like, one or two layers on top of that. But they’re, what they’re doing is jerry-rigging. They have not been trained yet, I’m not saying they can’t do it, but they’re not good at it right now, at what I call canonization, which is

01:05 taking kind of sloppy code, refactoring it, figuring out exactly where in the library it belongs, what’s the canonical version of this statement, of this lemma, and then everything, every proof should just be a combination of you apply this lemma from over here, you apply that lemma from over there, put all these things together, there’s your theorem. And then it’s really clean, it’s really beautiful, very elegant. That’s what Mathlib is going for. And what I said in my colloquium is, where we are today is that you can get entire textbooks formalized as long as they’re in the Mathlib halo.

01:36 As long as they’re, like, one, maybe two steps removed from things that have already been done in Mathlib. But when you start, and this had been my practice, my experience had been, when you start asking it to do things that are, you know, three or four steps removed from, the library, the way that it came up with a definition of this object and the way that it came up with some other definition of the same object, ’cause it was doing it for two different purposes, then they clash. You can’t stitch these things back together. Like, you really need the library, Mathlib, to grow- … in order to get to a place where you can

02:07 do research manuscripts, you know that are, that are really using, synthesizing tons of different areas of mathematics. - Which is why you would expect Fermat’s last theorem to take– because it’s so far outside of the halo of Mathlib, it would take quite a bit of time. - Exactly right. So Kevin Buzzard had a million dollar grant to spend the next five years, or I th- maybe he’s already a year or two into that grant, to reduce the formalization of Fermat’s last theorem to things that were known in the 1980s. So he wanted to do that last step, the, those seven years of Wiles’ work,

02:40 and Wiles Taylor, to finally finish you know, Fermat’s last theorem, but built on top of things that we knew would be extraordinarily difficult. He wasn’t gonna do Langlands’ Tunnell, he wasn’t gonna do Mazur. There were, there were all kinds of things that were expected to be even much more difficult than what these five years would take. And everything I said in that colloquium was wrong. And I think my colloquium was on a Wednesday. On Friday, there was a drop of thirteen million lines of code from the axioms, Fermat’s last theorem is proved. The statement of Fermat’s Last Theorem is completely elementary. There’s no semantic alignment to

03:13 check. You just glance at it. Yes, that’s the statement. It’s– Lean says it’s sorry-free. - Can you explain how it was done? - How it was done. So it was Anthropic, and how it was done was AI systems just got really, really good at– It’s still not a nice proof. It’s not the clean proof. It’s not– There’s still a ton of work that needs to be done to make that proof a Mathlib quality proof, and I think that’s important work and work that we want to do. But in terms of just getting that sorry-free theorem, they just blasted through all of these. They jerry-rigged this, they jerry-rigged that,

03:44 and, you know, thirteen million lines later, they had a sorry-free formal Lean proof of Fermat’s Last Theorem. It’s just absolutely shocking. - By the way, it’s beautiful to always, um– Because of how rapid everything is, there’s going to be a lot of statements that everybody makes, the world experts make, that are wrong. That’s the whole point of it. And that’s the fun thing about human discussion, is we have disagreements and I would venture to say somewhere between forty to eighty percent of everything said today will be wrong in five years because everything’s changing s-

04:16 so fast. But that’s the whole point of human discussion and deliberation and discourse and the, even the scientific process is saying shit and seeing what sticks, Over time. Over ten years, over a hundred years, and so on. - I was describing my experience. I had a lot of experience with Lean and, and with using AI. I started doing Lean before AI existed in the, in the sense that we understand it now, and it was very painstaking. And the second, uh, AI systems came on, you know, the first LLMs were coming online, they were, they were crap at

04:47 Lean, but then they got a little bit better, a little bit better, and I was like, “Oh my God, I can do library search.” I don’t have to sit there looking, I know there’s a lemma that does this, but I don’t know what it’s called, and I don’t know which exactly. Is it in the manifolds library? Is it in the algebraic geometry library? Like, give me this, give me this lemmas. It was great at that, and I was like, “Oh, this is amazing. I’m gonna keep using these systems.” And every bit of my experience told me that they can do, like, X, but not ten X, and this was a million X. It was just completely outside of the distribution in my mind of what systems

05:18 were capable of. - Do you have a ballpark estimate of how many humans were involved in that, and, like, what is the level of human involvement in generating those thirteen million lines of code? - Uh, I believe it was two or three humans. - Okay. - And I believe most of their involvement was, “Keep going,” all caps. - Okay. All right, so you think it’s really just, like gentle guidance, not like, you know, pathway creating and- - As far as I understand, there was no domain expertise- - Okay - … on the parts of the people who were doing this.

05:50 - As the meme goes with OpenAI or Anthropic you know, the prompt is solve math- … or something. And then- - Do a breakthrough. - Yeah, yeah. Yeah, do a breakthrough. - Do a breakthrough. That’s the prompt. And it goes and does it. - Of course, you never know from a company perspective, there’s a lot of incentive to sort of sell it as that, even though there might have been a lot of intermediate steps that led whe- at any stages of the training or maybe some things left unsaid, even though the final prompt is do a breakthrough, there could be a lot

06:23 of groundwork before that, that led to, we don’t know. - So I remember that was a Friday because I just was completely, like my mind was completely exploded, and it was Labor Day, and we just took the kids to the beach, and I needed a few days of, you know, I’m not checking my phone, I’m not on Twitter. I’m just throwing, you know, throwing my kids into the ocean and, and- - Did you have that moment where you’re just sitting and looking at the ocean and contemplating? - Yeah. Like, what does it all mean?

06:53 So I had already gone through that a month before. And I was like, I– So now what that says is that autoformalization is basically solved. It’s not solved in the way that I would want it to be solved. I want– And people are still gonna work very, very hard on this. There’s all kinds of other things that happen, just like there’s all kinds of other things that happen when you prove theorems that are byproducts of that process for human understanding. There’s all kinds of other things when you work on making a beautiful library of mathematics, and that process will continue. That process will be

07:24 very difficult. It’s gonna be the, you know, thousands of man-hours of people around the world contributing in this open source way. But in terms of can you get a sorry-free proof of something that human beings have written down on paper, I think that problem is done. - And so you were standing there with a whiskey, having gone through this a month before, and now again. - Right. This was round three. - This is round three. - ’Cause when I got back from Labor Day, it was Navier-Stokes. - Navier-Stokes. - But this one- - So I was like, “I was just mourning FLT. You’re gonna do this to me? Come on.”

07:55 - But now, I mean, this really hit home, right? With, with the quasi-RH.