Imagine a hypothetical project at the scale of the Linux kernel, with thousands of mathematicians building up organized and well-commented code, standing on each others shoulders.
I remember there being whole research groups trying to formalize a single (real world, as opposed to undergraduate) proof, and I remember reading that formalizing something like FLT is currently completely unfeasible.
In short, no, lean was not a tool to discover new math.
No, Kevin Buzzard is leading a project to formalise FLT for a couple of years now. Anthropic scooped him last month, but his project involves more than just producing a formal proof: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...
it might(?) work? but abstractions exist for a reason (mostly...)
Ie entrust the more tedious aspects but be able to follow along and still have references to check if you are curious about thoroughness.
Almost like a tap with a latex renderer at various insertion points?
Naturally eventually we got macro Assemblers, followed by other attempts until FORTRAN came to be.
I think the confusion stems from people being exposed to set theory, believing that formalisation is akin to writing those horrible set encodings of everything. Which I would agree would be akin to writing assembly.
But Lean, Rocq and Agda are all based in type theory. Which means it is more like the highest level programming language you can imagine! You have all the powers of abstraction, but you still have to convince the type checker – i.e. no “trust me, bro” casting, or even questionable while loops (“I promise this loop finishes at some point”).
These abstractions along with meta programming techniques (“tactics”) means that you can write readable correct proofs, but it takes effort. Math is extremely deep, and getting formalised all the way to the research frontier in a given subfield is a serious undertaking.
For anyone reading this, here is a very small example proof that + is associative over Nats in Agda (written using 1lab style equational reasoning syntax):
+-associative : (x y z : Nat) → x + (y + z) ≡ (x + y) + z
+-associative zero y z = refl
+-associative (suc x) y z =
suc x + (y + z) ≡⟨ ap suc (+-associative x y z) ⟩
suc (x + y + z) ≡⟨⟩
(suc x + y) + z ∎
In the `suc x` case we need to show that `suc x + (y + z) ≡ (suc x + y) + z`.
`suc x + (y + z)` computes to `suc (x + (y + z))` by the definition of `+`.
By recursively calling `+-associative x y z` we get `x + (y + z) ≡ (x + y) + z`. Then we need to prove that by congruence this is true under `suc`. We get this by passing our proof (from the recursive call to +-associative) into `ap suc`. `ap` says that given `a = b` it is true that `f a = f b`.
Finally, `(suc x + y) + z` computes to `suc ((x + y) + z)`, so the last step holds by computation, which is why it’s just `≡⟨⟩`.
Proof checkers like Lean/Agda/Rocq are literally total functional programming languages with rich type systems.
Everything above comes down to pattern matching and function application. The proof is just a function whose type is the statement we wanted to prove, and the type checker accepting it is what makes it a proof.
This is the Curry-Howard Correspondence in a nutshell. Propositions are types and proofs are programs.
-- An element has at most one two-sided inverse.
inverse-unique : ∀ (M : Monoid) (open Reasoning M)
(x y z : type M)
→ y ⋆ x ＝ unit M
→ x ⋆ z ＝ unit M
→ y ＝ z
inverse-unique M x y z leftInverse rightInverse =
begin
y ⟪ sym (unitᵣAt y) ⟫
y ⋆ unit M ⟪ mapᵣ (sym rightInverse) ⟫
y ⋆ (x ⋆ z) ⟪ sym (associativeAt y x z) ⟫
(y ⋆ x) ⋆ z ⟪ mapₗ leftInverse ⟫
unit M ⋆ z ⟪ unitₗAt z ⟫
z
∎
where open Reasoning M
(If you know Agda, I dare you to look carefully at this example!)
https://mathoverflow.net/questions/43690/whats-a-mathematici...
https://github.com/ityonemo/2b4m
The tradeoff is that it's more verbose, but you don't have to even know the language to properly decode a proof.
as an exercise for the language, I'm playing around with having Claude formalize an online algebra text:
https://github.com/ityonemo/2b4m/tree/main/aata
LMK what you think
You only compare to tactic heavy languages, which is what you don't like about them. Try looking at Agda, Idris, Mikan,... They work with pattern matching not just for definitions but for proofs as well, so the derivation is laid bear.
Not saying your niche doesn't have value, but you can get interesting ideas from there.
Aside: To some degree, the claudisms are the point since the PL is written by Claude and intended to be consumed by claude
> Humans have quite a bit of creativity but make a lot of mistakes. The Lean typecheck never makes a mistake but has no creativity. Get them to work together in an iterative loop and you get what we have now.
The point is that the there has to be an idea to try to check. Lean does not give you that.
Yes. Humans are slow.
I believe so. But the question I was responding to was whether humans working with Lean would be have been more creative.
(Former grad student in math here who has spent whole weeks formalizing in Lean lemmas that would be considered by professional mathematicians writing a mathematics text / paper as obvious ("without loss of generality we can assume that....", "it should be clear that...")
Probably very few or none.
These systems (mostly) don't help you discover new mathematics. They are a tool for formalization.
It just turns out that combining them with LLMs is the secret sauce. LLMs have quite a bit of creativity but make a lot of mistakes. The Lean typechecker never makes a mistake but has no creativity. Get them to work together in an iterative loop and you get what we have now.