From Trust to Verification: Lean’s Impact on Mathematics

For thousands of years, mathematicians have experienced the emotional roller coaster of checking and rechecking their work: Just when they think a proof is complete, the ground can drop out from under them because of a tiny error. They rebuild their theorems, only to uncover more errors that need fixing.

A new software tool could transform mathematical research, turning that roller coaster into a reassuringly steady climb to a proof. Introduced in 2013, the proof assistant Lean reduces the need for repeated manual checking, allowing researchers to focus on the thrills of mathematical research. When mathematicians formalize their work, or rewrite proofs into code that Lean can verify, they catalyze new ways of collaborating. No other proof assistant has ever been as widely embraced and evangelized as Lean, which boasts an impressive library of formalized work that future mathematicians can easily build upon.

“I think the math community loves most that Lean enables them to work together, even with people that they never met before,” says Leonardo de Moura, Lean’s creator. “It’s almost like the mathematician is a program manager who sets the architecture of the project, and then people all around the world contribute to it and fill the holes.”

Lean addresses a fundamental ‘trust bottleneck’ in mathematics: No researcher can personally verify every result needed to advance new work. As a consequence, mathematicians tend to rely on papers published by people they know or journals they trust. When papers include formalization, mathematicians can confidently build on those results regardless of where they were published. That shift is transforming how mathematicians work.

Lean’s Beginnings

Although several other proof assistants such as Coq, Isabelle and Mizar can check the logic of a proof, none are as widely used or scalable as Lean. In 2013, when de Moura realized the enormous potential of the debugging program he had written, he released Lean as opensource code and began working on what would become an unprecedented level of scalability and usability.

By 2015, Lean had a small community of users, including Jeremy Avigad, a professor at Carnegie Mellon University who had just taken on a master’s student, Sebastian Ullrich, who was visiting from the Karlsruhe Institute of Technology in Germany. For the next several years, Ullrich was the only person besides de Moura adding code to Lean.

2021 was a big year for the proof assistant. In the summer, renowned mathematician Peter Scholze asked the community to validate and clarify a complicated new proof using Lean. The freshly confirmed results were written up in Nature. That fall, billionaire Charles Hoskinson donated $20 million to Carnegie Mellon to establish a center focused on Lean under Avigad’s direction. A week later, the nonprofit incubator Convergent Research reached out to de Moura and Ullrich asking if they’d be interested in turning Lean into a new type of nonprofit organization.

In 2023, when Ullrich defended his Ph.D. thesis documenting the current version of Lean, the pair established the nonprofit Lean Focused Research Organization (FRO) with guidance from Convergent Research and generous philanthropy, including a $5 million gift from Simons Foundation International and related support from the Simons Foundation.

Like a cross between a startup and a university lab, an FRO incubates new research with philanthropic grants. After the five years are up, the Lean FRO will disband and transition into a nonprofit foundation, in the footsteps of foundations related to the Rust programming language and the Linux operating system. “Before the FRO, it was a research project: Sebastian was a grad student, we were writing papers and our focus was the research,” de Moura says. “Once the community grew a lot, people started expecting a product of better quality. Without this money, it would be impossible to run.”

A Global Shift

To encourage the adoption of Lean, the Simons Foundation hosted a two-week workshop in June 2025. Led by mathematicians Alex Kontorovich, Antoine Chambert-Loir and Heather MacBeth, the workshop brought together 57 postdocs, graduate students and early-career researchers from around the world at the Simons Foundation’s New York City headquarters. During the workshop, participants formalized solutions to undergraduate-level exercises and more advanced mathematics, including the prime number theorem. That theorem, which quantifies how prime numbers become rarer as they get larger, already had a ‘blueprint,’ or a map of the proof showing every formalized statement and how those statements depend on one another.

During the workshop, participants formalized solutions to undergraduate-level exercises and more advanced mathematics, including the prime number theorem. That theorem, which quantifies how prime numbers become rarer as they get larger, already had a ‘blueprint,’ or a map of the proof showing every formalized statement and how those statements depend on one another.

“We had had this large-scale formalization project where software engineers who had a few hours on the weekend would volunteer to solve one of these goals; we were slowly but surely making progress through this,” says workshop leader and blueprint designer Kontorovich, who is also a member of the Lean FRO strategic advisory board. During the second week of the workshop, “we worked for five days, eight hours a day, knocking off those [goals]. Once those things were done, I just put in the last step. So that proof formalization is thanks to the Simons Foundation.”

The formalization of the prime number theorem is exciting, even though the theorem itself is nearly a century old. That’s because the mathematical objects and subproofs — called lemmas — that workshop attendees coded into the math library of Lean can be used perpetually by future researchers, which means that Lean becomes easier and faster the more researchers use it. Lean’s verification powers mean that researchers can create and trust AI-generated proofs of lemmas without worrying about AI hallucinations or ‘slop.’

The Promise of Lean

Lean augurs a new future for mathematics. Kontorovich compares Lean to the typesetting program LaTeX, which was unpopular when it was developed in 1978 but is now standard throughout mathematics and science; he predicts that Lean will similarly become ubiquitous in a few generations. Lean is particularly useful in education, providing instantaneous feedback.

“It’s completely different from school when you submit your exercise sheet once a week and you hear back maybe a week later,” Ullrich says. “Just getting that feedback immediately about whether that proof makes sense or not, it’s a complete game changer.”

Lean will transform other realms as well. De Moura says, laughing, that “it feels like every week now some startup founder contacts us.” Lean was created to aid mathematicians and build trust in the field, but researchers are also finding it a powerful tool for AI-assisted mathematics. One AI startup that relies on Lean, Harmonic, won a gold medal at the International Mathematical Olympiad in 2025 after a Google AI chatbot that uses Lean was one point shy of gold in 2024. In early 2026, a 23-year-old used ChatGPT and Lean to solve Erdős Problem 1196, which had remained unsolved for 60 years, in just over 80 minutes of compute time.

As AI improves, it will undoubtedly formalize more math. In 2023, while serving as editor of the journal Experimental Mathematics, Kontorovich ran a special issue on proof assistants, including Lean. The experience convinced him that AI will not be replacing mathematicians anytime soon.

“There are two very separate things that a journal evaluates when it receives a paper: One, is the mathematics correct, and two, is the mathematics interesting,” Kontorovich says. “Lean does not evaluate two at all. Lean will prove that 17 plus 18 equals 35, and it will certify that the theorem is correct, which is not interesting. So, it’s still up to mathematicians to determine what our taste is [and] what our values are.”