From Trust to Verification: Lean’s Impact on Mathematics

You are using an outdated browser. Please upgrade your browser to improve your experience.

Annual Reports

Home

Annual Reports<br>2025 Annual Report

By Yen Duong<br>June 23, 2026

Series<br>2025 Annual Report

An example of what it’s like to work on a proof using Lean. This proof demonstrates that an infinite number of prime numbers exists. Lean FRO

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.

Rutgers University mathematician Alex Kontorovich, one of the leaders of a 2025 workshop for Lean at the Simons Foundation. Nick Romanenko/Rutgers University

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.

Mathematicians Antoine Chambert-Loir of the University of Paris and Heather MacBeth of Fordham University — together with Alex Kontorovich — co-led a 2025 Lean workshop at the Simons Foundation. Ivonne Vetter/MFO; Petra Lein/MFO

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...