This post is based on talk I gave.

Until three years ago, few people knew about Lean. Then came AI and revolutionised mathematics, making Lean useful even to the working mathematician. The Lean users (Leaninists? Octopuses? Xenists?) have been vindicated.

How did we end up here? #

There have always been formalisation fetishists.

In Begriffschrift (1879), Gottlob Frege introduced a formal system to express logical concepts. His goal: to aid ‘pure thought’. A few years later, Alfred North Whitehead and Bertrand Russell dropped the Principia Mathematica, which set out to derive all of mathematics from logical axioms. David Hilbert, perhaps known to non-mathematicians for ‘Wir müssen wissen. Wir willen wissen.’, was also ahead of the curve w.r.t. formalisation. In the early 1920s, he launched Hilbert’s program, an attempt to ground all of mathematics in a finite, complete set of axioms, in the early 1920s.

We’ll come back to this.

Fast forward to the 1960s; welcome to the computer age. Using formal languages like Automath and Mizar, computers could read and verify the correctness of mathematical proofs. In the 1980s came Rocq, and soon thereafter, we got Isabelle, two proof assistants widely used today. Lean was created by Leonardo de Moura as late as 2013. Early Lean adopters like Patrick Massot, Jeremy Avigad and Kevin Buzzard helped popularise the language.

But Lean isn’t just a language; there’s also a vibrant lean community. Mathlib, Lean’s mathematical library, comprises about 2.1 million lines of code. It’s roughly half the size of the archive of formal proofs in Isabelle, the largest mathematical library (by LOC), but then Isabelle was created in 1986. There’s also an active Zulip chat with more than 10.000 users.

Without its welcoming and well-organised community, Lean wouldn’t have become nearly as popular.

Why should I bother learning Lean? #

In the past, I would’ve said something like the following. Firstly, formalising a proof leads to a deeper understanding: formalisation requires working out all – yes, all – the details. It also involves lemmifying statements properly, which can be incredibly illuminating. Secondly, formalising a proof gives you near-certainty it’s correct. Finally, Lean enables large-scale research collaboration. Since the authors on a joint paper all need to trust each other, you’d previously only have one-three co-authors. Lean solves your trust issues: each co-author can provide a Lean certificate for their part, instead of going over the proof by a blackboard individually with each co-author.

Today, the above reasons for learning Lean remain valid. Having a certificate of correctness is particularly useful for AI-generated proofs. However, my overall answer is different.

AI systems are capable of autonomously solving open problems, and, to some extent, doing theory building. The AI progress for mathematical reasoning abilities has been spectacular: we got the first solutions to open problems in December 2025, and they can now solve our toughest problems.

In parallel, there have also been major advances in autoformalisation. Much as task time-horizon length is increasing exponentially, ‘result LOC-length’ – the lines of code in a result an AI can formalise autonomously – is increasing exponentially. Anthropic’s formalisation of Fermat’s last theorem comprised 13 million lines of code, about five times the size of Mathlib.

In fact, formalising the entire mathematical corpus is now within reach (Hilbert’s program?). Estimates suggest this would require about 10B lines of code. Jared Duker Lichtman, who is coordinating the efforts, thinks it’s doable next year.

All this to say that mathematics is changing rapidly. I bet Lean will play a key role in maths 2.0. If you want to stay at the forefront, it’s worth learning some lean.

But what’s the bare minimum? #

The usual recommendation was for newcomers to learn to do the Natural Number Game and then work through all of Mathematics in Lean. For most mathematicians, who are busy with research, teaching and grading, this just isn’t feasible.

However, thanks to advances in autoformalisation, one can quickly get to the point where Lean is useful. If you want to speedrun Lean, here’s how:

1. Lean some syntax. Even if you use AI, you need to check the formalisation is faithful to the TeX – the lean statements and proofs should correspond to the TeX’d statements and proofs.
2. Learn how to use autoformalisation agents. There are plenty of options available – for most practical purposes, Claude Code or Codex works just fine. A good free option is Aristotle by Harmonic.
3. Optionally, learn about Lean-related tools. There’s plenty of nice-to-have software for Lean users: Palomar, a registry of Lean-verified proofs; Comparator, which reduces the human amount of checking; Verso, a kind of jupyter notebook for Lean.

I’ll also plug TauCeti, the AIs-welcome version of Mathlib, where I’m a reviewer. It’s now growing explosively.

Conclusion #

Lean and AI for maths go well together. AI has lowered the barrier of entry to the Lean community, while Lean is underpinning AI-led advances in mathematics. Time to build widespread Lean literacy.