PMA Publisher: Published from the Principia Machina source

2026-10-15T19:35:35Z

Published from the Principia Machina source

← Older revision		Revision as of 19:35, 15 October 2026
Line 1:		Line 1:
	{{DISPLAYTITLE:Research mathematics}}		{{DISPLAYTITLE:Research mathematics}}
			{{Lean theorem prover map}}
	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: [[Lean theorem prover/Applications/The polynomial Freiman-Ruzsa conjecture\|the polynomial Freiman–Ruzsa conjecture]], [[Lean theorem prover/Applications/The Fermat's Last Theorem project\|the Fermat's Last Theorem project]] and [[Lean theorem prover/Applications/The equational theories project\|the equational theories project]].		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: [[Lean theorem prover/Applications/The polynomial Freiman-Ruzsa conjecture\|the polynomial Freiman–Ruzsa conjecture]], [[Lean theorem prover/Applications/The Fermat's Last Theorem project\|the Fermat's Last Theorem project]] and [[Lean theorem prover/Applications/The equational theories project\|the equational theories project]].

PMA Publisher: Published from the Principia Machina source

2026-10-14T18:01:16Z

Published from the Principia Machina source

New page

{{DISPLAYTITLE:Research mathematics}}
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: [[Lean theorem prover/Applications/The polynomial Freiman-Ruzsa conjecture|the polynomial Freiman–Ruzsa conjecture]], [[Lean theorem prover/Applications/The Fermat's Last Theorem project|the Fermat's Last Theorem project]] and [[Lean theorem prover/Applications/The equational theories project|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.<ref name="mathlib">The mathlib Community, "The Lean mathematical library", in ''Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)'', 2020. arXiv:1910.09336. doi:10.1145/3372885.3373824</ref> 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 [[Lean theorem prover/History/Mathlib and its community|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.<ref name="perfectoid">Kevin Buzzard, Johan Commelin and Patrick Massot, "Formalising perfectoid spaces", in ''CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs'', 2020, pp. 299–312. doi:10.1145/3372885.3373830. arXiv:1910.12320</ref>

'''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.<ref name="lte">The mathlib community, "Completion of the Liquid Tensor Experiment", Lean community blog, 15 July 2022. https://leanprover-community.github.io/blog/posts/lte-final/</ref> The story is told in [[Lean theorem prover/History/The Liquid Tensor Experiment|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.<ref name="eversion">Patrick Massot, Floris van Doorn and Oliver Nash, "Formalising the h-principle and sphere eversion", arXiv:2210.07746, October 2022. https://arxiv.org/abs/2210.07746</ref>

'''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.<ref name="carleson" /> Its final version, revised in August 2025, is presented as a guide to the accompanying Lean code.<ref name="carlesonbp">Lars Becker, María Inés de Frutos-Fernández, Leo Diedering, Floris van Doorn, Sébastien Gouëzel, et al., "A blueprint for the formalization of Carleson's theorem on convergence of Fourier series", arXiv:2405.06423, May 2024 (revised 6 August 2025). https://arxiv.org/abs/2405.06423</ref> 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.<ref name="carleson">Floris van Doorn et al., "Formalization of a generalized Carleson's theorem" (project description, read 13 October 2026). https://github.com/fpvandoorn/carleson</ref>

'''Sphere packing in dimension 8.''' In 2016 Maryna Viazovska proved that the <math>E_8</math> 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.<ref name="packing">Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux and Maryna Viazovska, "Progress in Formalizing Sphere Packing in Dimension 8", arXiv:2604.23468, April 2026 (revised May 2026). https://arxiv.org/abs/2604.23468</ref> 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.<ref name="epfl">EPFL, "Prof. Viazovska's proofs of sphere packing formalized with AI", EPFL news, March 2026. https://actu.epfl.ch/news/prof-viazovska-s-proofs-of-sphere-packing-formaliz/</ref>

== 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.<ref name="scholze">Peter Scholze, "Half a year of the Liquid Tensor Experiment: amazing developments", guest post on ''Xena'' (blog), 5 June 2021. https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/</ref>

'''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.<ref name="flt">Kevin Buzzard, "Fermat's Last Theorem — how it's going", ''Xena'' (blog), 11 December 2024. https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/</ref> 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.<ref name="annals">Kevin Buzzard, "The Annals Challenge", ''Xena'' (blog), 13 August 2026. https://xenaproject.wordpress.com/2026/08/13/the-annals-challenge/</ref>

'''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.<ref name="etp">Matthew Bolan, Joachim Breitner, Jose Brox, et al. (34 authors, including Terence Tao), "The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale", arXiv:2512.07087, December 2025. https://arxiv.org/abs/2512.07087</ref>

'''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.<ref name="annals" /> 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.<ref name="general">Kevin Buzzard, "A Lean formalisation of Fermat's Last Theorem" (the project's general information), written December 2023. https://github.com/ImperialCollegeLondon/FLT/blob/main/GENERAL.md</ref>

'''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.<ref name="annals" /> The use of Lean as a checker for machine-generated proofs is the subject of [[Lean theorem prover/Applications/Machine learning and theorem proving|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.<ref name="annals" /> 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.<ref name="beaten">Kevin Buzzard, "FLT: Anthropic has beaten me to it", ''Xena'' (blog), 4 September 2026. https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/</ref>

== Next ==

* [[Lean theorem prover/Applications/The polynomial Freiman-Ruzsa conjecture|The polynomial Freiman–Ruzsa conjecture]], a research result checked within weeks of its proof.
* [[Lean theorem prover/Explainers/Stating the right thing|Stating the right thing]], on the limit named above.

== References ==
<references />

Lean theorem prover/Applications/Research mathematics - Revision history

PMA Publisher: Published from the Principia Machina source

PMA Publisher: Published from the Principia Machina source