When Lean came out, there were plenty of other proof assistants available, including Coq, which is the most similar to Lean — the logical foundations of both programs are based on dependent type theory. But Lean represented a chance to start fresh. Mathematicians created mathlib and eagerly began to fill it with the world’s mathematical knowledge. The work has the air of a barn raising. “If you were to quantify how much of mathematics is formalized, I’d say it’s way less than 0.001%.” It will probably take decades before mathlib has the content of an actual research library, but Lean users have shown that such a comprehensive catalog is at least possible — that getting there is merely a matter of programming in all the math. Last year, the Lean community put aside the accumulation of undergraduate math and skipped ahead to the vanguard of the field. The goal was to define one of the great innovations of 21st-century mathematics — an object called a perfectoid space that was developed over the last 10 years by Peter Scholze. In 2018, the work earned Scholze the Fields Medal.

This project just hit a major milestone, as Peter Scholze explains:

While this challenge has not been completed yet, I am excited to announce that the Experiment has verified the entire part of the argument that I was unsure about. I find it absolutely insane that interactive proof assistants are now at the level that within a very reasonable time span they can formally verify difficult original research. Congratulations to everyone involved in the formalization!!

In this Q&A-style blog post, I want to reflect on my experience watching this experiment.

How did the formalization proceed?
Initially, I imagined that the first step would be that a group of people study the whole proof in detail and write up a heavily digested version, broken up into many many small lemmas, and only afterwards start the formalization of each individual lemma. This is not what happened. Instead, the formalization followed quite closely the original lecture notes, and directly attacked Lemma after Lemma there. It did seem that the process was to directly type the proofs into Lean. Lean actually gives the user a very clear summary of what the current goal is, so one always needs to get a very clear sense of what the next few steps really are. Sometimes it was then realized that even on paper it does not seem clear how to proceed, and the issue was brought to attention in the chat, where it was usually quickly resolved. Only after a lemma was entirely formalized, the proof, now thoroughly digested, was again written up in the Blueprint in human readable form.

What did you learn about the process of formalization?
I learnt that it can now be possible to take a research paper and just start to explain lemma after lemma to a proof assistant, until you’ve formalized it all! I think this is a landmark achievement.

see also this earlier piece about using coq:

For 10 years, Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of mathematics and computer programming closer together. As he sees it, the move to computer formalization is necessary because some branches of mathematics have become too abstract to be reliably checked by people. “The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes”. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error. The real potential of type theory informed by homotopy theory is as a new foundation for mathematics that’s uniquely well-suited both to computerized verification and to studying higher-order relationships.

and even earlier efforts:

A grand objective of the field is to formalize the whole of mathematics, reproving its theorems with a negligible probability of error, all based on a small kernel (in the HOL Light system, the kernel is 500 lines of OCaml code).

and another backgrounder

As the towering mathematical enterprise reaches new heights, with more intricately and esoterically turreted peaks, each practitioner drilling down into minutiae that could never be understood by colleagues even in the same field, computers will be necessary for advancing the enterprise, and authenticating the integrity of the structure—a structure so complex in detail and so massive in scale that adjudication by mere human referee will no longer be feasible

one person’s perspective

I’m not concerned by the fact that no human mathematician can check this, because we can check it with other computer approaches

2023-06-01: Progress continues, and now LLM have entered the picture

We set out to tackle serious mathematics with a combination of hope and trepidation. We were able to formalize everything we set out to formalize and were never forced to discard a development part way through. “We have formalized results by 2 Fields medalists (Roth and Gowers), an Abel prize winner (Szemerédi) and of course Erdős too!” We’ve also seen impressive advances in search and language models to assist users in proof development. Although the effort required to formalize mathematical articles remains high, we can confidently predict that formalization will be playing a significant role in mathematical research in the next few years.

2025-09-11: Gauss

Using Gauss we produced ~25K lines of Lean code, comprising 1K theorems and definitions. Formal proofs of this scale have historically been major milestones, often the culmination of multi-year efforts. The largest singular formalization projects in history — career-defining efforts, which can span more than a decade — are only an order of magnitude larger at up to 500K LOC. Lean’s standard mathematical library, Mathlib, is 1 OOM beyond that, at 2M LOC, comprising 350K Lean theorems and definitions, and developed by 600 human contributors over 8 years. With further algorithmic improvements, we aim to increase the sum total of formal code by 2-3 OOM in the coming 12 months. This will serve as the training ground for a new paradigm — verified superintelligence and the machine polymaths that will power it.

• Uncategorized