Research mathematics

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

Since about 2019 working mathematicians have used Lean to formalise current research, not only textbook material. This page gives an overview: a few of the results that have been formalised, the reasons mathematicians give for doing it, and the limits of what it establishes. Three projects have pages of their own: the polynomial Freiman–Ruzsa conjecture, the Fermat's Last Theorem project and the equational theories project.

The library underneath

Almost all of this work rests on Mathlib, a single library of mathematics formalised in Lean and maintained by its community. Its authors describe it as built on dependent type theory, focused on classical mathematics, organised around a large hierarchy of structures, and run as a distributed, community project. A research project usually adds new definitions and theorems on top of it, and moves the general ones into it later. Its history is told in Mathlib and its community.

Some formalised results

Perfectoid spaces. Peter Scholze introduced perfectoid spaces in 2012. Kevin Buzzard, Johan Commelin and Patrick Massot formalised enough topology, algebra and geometry in Lean to define them. Their point was that a proof assistant can handle the complexity of advanced definitions, not only long proofs about simple objects.

Liquid vector spaces. In December 2020 Scholze challenged the Lean community to check a theorem of his and Dustin Clausen's in the theory of condensed mathematics. The formalisation was completed on 14 July 2022. The story is told in The Liquid Tensor Experiment.

Sphere eversion. Massot, Floris van Doorn and Oliver Nash formalised the local h-principle for first-order, open, ample differential relations, a result of Gromov from 1973, and derived from it Smale's theorem that a sphere can be turned inside out through immersions. They took it as evidence that geometric mathematics, not only algebra, can be formalised.

Carleson's theorem. Carleson's theorem says that the Fourier series of a continuous periodic function converges to it at almost every point. A team of 17 authors wrote a blueprint that reduces it to a new, more general theorem on doubling metric measure spaces due to harmonic analysts in Bonn, and proves that theorem. Its final version, revised in August 2025, is presented as a guide to the accompanying Lean code. The project's description states that the proof has been formalised and names the Lean theorems for the classical statement and for both general forms.

Sphere packing in dimension 8. In 2016 Maryna Viazovska proved that the $E_8$ lattice gives the densest packing of equal spheres in eight dimensions. In March 2024 Sidharth Hariharan and Viazovska began formalising the proof in Lean. The main result was formally verified in February 2026, with the final stages carried out by Gauss, an autoformalisation model of the company Math, Inc. EPFL reported in March 2026 that, after the team had written a detailed blueprint and progressively translated it into Lean, Gauss's help let the dimension 8 case be wrapped up in five days, and the considerably larger case of dimension 24 in two weeks.

Why mathematicians do it

To settle a doubt. Scholze's liquid tensor challenge centred on one theorem in his notes with Clausen, the only result in them that he was worried about. The check confirmed the argument but found a few small gaps, all repairable, of the kind he had feared. He also reported that the work showed him why the argument works, which he had not understood when he set the challenge.

To find errors in the literature. Formalisation cannot pass over a gap. The Fermat project found a lemma in a 1965 paper on divided powers that appeared to be false, and the gap had to be repaired before the work could go on. In August 2026 a team led by Buzzard announced a dataset of Lean statements of 50 theorems published in the Annals of Mathematics in the 2020s. He reported that the work had already found several typos that made main theorems false as printed, four of them in papers by Fields medallists, and that each of those four was a missing hypothesis.

To collaborate without trusting every contributor. In the polynomial Freiman–Ruzsa and equational theories projects, people who had not read the whole argument contributed pieces, and Lean, not an organiser, decided whether each piece was correct.

To be able to state modern mathematics at all. Buzzard's team stated the main theorems of about 20 per cent of the papers that the Annals has published since 2020. Many others mention objects, such as cuspidal automorphic representations, that Mathlib does not yet define, so their statements cannot be written in Lean until those definitions are built. The Fermat project gave the same gap as one of its reasons: many standard objects of modern number theory had not been defined in any theorem prover.

To check machine-written mathematics. Buzzard has argued that a proof which comes with Lean code at least guarantees that the argument is correct, so that a reader of AI-generated mathematics can be more confident that the reading is not wasted. The use of Lean as a checker for machine-generated proofs is the subject of Machine learning and theorem proving.

What it does not establish

A formal proof establishes that the Lean statement follows from Lean's axioms. It does not establish that the Lean statement says what the paper meant; that has to be read by people, and it is the hard part when the definitions are new. Buzzard concedes that formalisation by machine forgoes a gain that formalisation by hand has historically brought: teaching people new abstractions. Formalising a known proof need not add new mathematics either: Buzzard wrote of the machine-written proof of Fermat's Last Theorem that it follows the literature faithfully and adds nothing.

Next

• The polynomial Freiman–Ruzsa conjecture, a research result checked within weeks of its proof.
• Stating the right thing, on the limit named above.