According to legend, in or around 1637, French mathematician Pierre de Fermat scribbled a problem and a note in a copy of Arithmetica, a book by third-century Greek mathematician Diophantus. The problem involves this equation: an + bn = cn. If n = 2, then we know there are infinitely many solutions. That’s because in that case, the equation becomes the Pythagorean theorem and a, b and c correspond to the side lengths of right triangles.

Fermat stated that there are no whole numbers for a, b and c that can solve this equation if n is greater than 2. Next to the problem, Fermat wrote in Latin: “I have a truly marvelous demonstration of this proposition that this margin is too narrow to contain.”

Fermat’s son discovered the book and the note, but not until after his father’s death. The theorem was easy to state and hard to prove, and Fermat’s missing proof vexed mathematicians for centuries. No one ever found his “truly marvelous” argument, and no mathematician ever conjured a proof that might remotely fit that description. Some question whether it ever existed, or conjecture that whatever proof Fermat had in mind was fatally flawed. It’s tempting to view Fermat’s statement as a practical joke with extraordinarily long legs.

British mathematician Andrew Wiles finally cracked it in the late 20th century and later collaborated with mathematician Richard Taylor to finalize it. Their proof used arcane, far-reaching mathematical concepts that weren’t around in the 17th century, ideas that bridge mathematical fields that once seemed unconnected.

Over centuries, by probing Fermat’s simple problem mathematicians have made enormous breakthroughs in many fields beyond number theory, the field most closely associated with the original problem. In one of the most significant, German mathematician Ernst Kummer proved in 1847 that the theorem held for the regular primes — a subset of prime numbers. He did so by developing ideas that laid the groundwork for a new field called algebraic number theory.

A graphical depiction of Fermat’s Last Theorem. The text reads: “According to mathematician Pierre de Fermat, there are no whole numbers for a, b and c that can solve this equation if n is greater than 2.” C. CHANG In 2023, with support from the U.K.’s Engineering and Physical Sciences Research Council, Buzzard launched his formalization project with Fermat’s last theorem partly because of the proof’s size and importance, and partly because many of his colleagues at Imperial College London are exploring ideas used in the proof. He knew it would be a Herculean, messy task to encode every definition and lemma — akin to a mini-theorem embedded in a larger proof — that plays some role in the overall scheme. And it’s been a rocky road. “I’m sort of all over the place, and I’ve had some failed starts,” he says.

He’s not toiling alone. At first, Buzzard says, about 30 people were contributing to his formalization effort by writing code for Lean, all of them familiar names and faces. Many more have reached out with ideas or otherwise tried to join the effort, he says, and just over 60 have had their coded contributions verified and accepted. Still, the project has grown into an interdisciplinary collaboration on a scale that Buzzard couldn’t have imagined. Anonymous number theorists are reaching out with ideas, he says. Last August, he says, he went camping at a music festival for a week and returned to find 7,000 unread messages about various aspects of the proof.

In January, the effort reached one of its first major milestones. “We proved that a certain thing was finite,” paving the way for the next step, Buzzard says. The effort required for that milestone, however, has led him to doubt whether they’ll finish in his targeted timeline of five years.

One of the largest challenges, Buzzard says, is figuring out how to quickly build Lean’s library of mathematical knowledge. This is a bottleneck for AI applications in math, too. “In this whole area of AI for math is that there’s a terrible lack of interesting datasets,” he says.

In a separate project funded by Renaissance Philanthropy, Buzzard and Rutgers mathematician Alex Kontorovich are further contributing to Lean’s library — and expanding its applicability — by formalizing problems from a list of recent, particularly thorny theorems representing the cutting edge of mathematics in the 21st century.

The implications reach far beyond Buzzard’s projects. An expanding volume of mathematical knowledge could enable working mathematicians — if they were so inclined — to find fault lines in new proofs, or determine whether certain conjectures could hold up. Referees and editors who review papers for journals would be free to focus on the big ideas behind submitted papers rather than the excruciatingly fine details of the logic behind the proof.

“That’s game changing,” Riehl says. “Proofs are hard, and the papers are already very long.” Errors can slip through.

A theorem prover with access to a robust library of mathematical knowledge could be used to identify hallucinations and other mistakes in mathematical proofs generated by AI programs. Having a proof be 95 percent correct, after all, may mean the proof isn’t correct at all. “One hallucination can break an entire mathematical argument because that’s the nature of mathematics,” Buzzard says.

For that reason, tech companies have been developing programs that combine AI tools like Google’s Gemini or OpenAI’s ChatGPT with the fact-checking rigor of Lean. So has the U.S. government: In early 2025, DARPA launched a program called Exponentiating Mathematics, or expMath, with the goal of using AI to accelerate the rate of mathematical discovery, primarily by offloading the finer details of constructing a proof.

All of these efforts tie directly into a more controversial and quickly evolving issue facing mathematics today: figuring out how AI is going to change the field, and whether the AI math invasion is a good thing.