Comments
In other words, how much of the developments this year are directly attributable to LLMs using lean, versus lean just being a significantly more productive language for some subset of mathematics compared to English and LaTeX?
Given how much we’ve seen formalized this year it feels hard to believe that this couldn’t have happened earlier.
Follow up question: do you think mathematicians would be as upset about the rapid changes in their field if they were the result of a collective shared effort on github, authored entirely by humans who all share the credit, versus that same outcome but authored by a large language model?
In other words, are the mathematicians upset about large language models, or are they really just upset that formalization and massive collaboration have turned out to be highly effective and has negated the heroic angle that mathematicians previously enjoyed, thinking in a locked room by themselves?
Food for thought.
A coworker recently remarked that lean seems like a new foundational language family that every programmer should be able to read, on par with C and Python, and I think it’s pretty hard to disagree with that. Next generations of models are going to be RL’d on Lean more and more because it pays dividends in winning the math war against their competitors, and this will benefit users of lean not only for mathematics but also as a general programming language and as a vehicle for other DSLs. For example, I think Sparkle (a Lean based HDL) or something like it makes a lot of sense in 2026 and beyond.
(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.
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 formalizing an online algebra text:
https://github.com/ityonemo/2b4m/tree/main/aata
LMK what you think
https://mathoverflow.net/questions/43690/whats-a-mathematici...
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?
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.
Naturally eventually we got macro Assemblers, followed by other attempts until FORTRAN came to be.
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...
> 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.
I believe so. But the question I was responding to was whether humans working with Lean would be have been more creative.
Yes. Humans are slow.
Absolutely none of them. I have some experience formalizing math by hand in the pre-LLM era. I never started with making the formal proof. It is way too difficult. I don't think I've ever heard of any mathematician starting with a formal proof vs writing a natural language proof. Starting with a formal proof vs a natural language proof is putting the cart before the horse.
Without a natural language proof, or at least an idea of how to write the natural language proof, it is very difficult to write a formal proof. It's flying blind. I can blindly apply tactics, but without some larger plan to guide my formal proof, it's near impossible to make progress on all but the most trivial proofs. I don't think it has ever happened that a major proof was formalized before its natural language proof was written.
I don't think people appreciate just how labor-intensive it previously was to write a formal proof. It takes easily 10-1000x as much time for a human to write a formal proof vs a natural language proof. Even just formalizing a single undergraduate math textbook for certain subjects by hand was considered a multi-year project for a professional mathematician to undertake.
Formalizing a new paper, even if it was building on previously already formalized theorems, could be months of work just by itself, even with the natural language proof in hand.
It is no surprise that OpenAI releases natural language proofs before they release formal proofs. Presumably the same difficulty difference applies to LLMs as well.
Maths is a language, and learning a language takes time. Its like if I say that japanese made an effort to obfuscate their language just because i cannot read it or read it as fast as english.
LLMs are autimating some part of maths which is formal manipulation. It happens that computers are much better than humans at formal manipulation. In the same way that computers are much better at mathematical computations. That is the huge change in the field. But any working mathematitian can tell you that formal manipulation is just part of the research job.
The powerfull thing about maths is that formal manipulation has allowed humans to go further "for free": you just need to understand the foundations, and the formal system allows you to compute new results for free without needing to reunderstand them.
Reading very charitably: you can say that at the moment a lot of the AI's advantages seem to come from: (a) having read approximately everything, and (b) being willing and able to try out lots and lots of approaches without tiring or getting bored. You don't need to have superhuman intelligence, yet, when superhuman persistence still yields so much low hanging fruit.
If I want to understand some mathematics, my first step is always translating it to code. Modern code (excluding array languages) no longer has a culture of minimizing character count, and omitting "obvious" steps is not possible. LLMs are based on an architecture (transformers) that was originally designed for natural language translation, so it doesn't surprise me that they're good at this.
You need to think of mathematical writing as being both symbols/words and also a picture. You're meant to see patterns in what is in front of you. The short names are necessary for the picture. Without them you can't see it. It's like you've zoomed into the individual pixels; the information is all there but you'll never make sense of it that way. You're meant to read the "zoomed out" view where you have short placeholders as names.
computer science, or "Informatik/informatique" how some Europeans call it, was a branch of mathematics, and "the industry" pushed _very_ hard to get it "practical", make colleges and universities produce programmers, not computer scientists.
so they removed all "challenging" maths requirements from the curriculum, and you can graduate with much less formal rigour, and certainly without being a matematician.
that's also how python replaced scheme as a first teaching language.
There is space for both but in the real world we need more engineers who know how to build systems properly than theorists who are great at formal reasoning. It's like structural engineering and physics.
Not so fast. There were plenty more horses in that race.
You can easily make an argument that Python is a 'worse' language than Scheme as a first teaching language (though not necessarily one I would subscribe to: they are both dynamically typed and mostly differ in syntax). But Python (and Scheme and even Basic) are a lot better than starting people off with C or Java, or, God forbid, C++.
Obviously there are people who you can lock in a dimly lit closet with just an outdated reference manual to a made up machine and they'll can't help but pick up programming; and those won't have much trouble coping with Java or C++. But those who actually need to be taught will be better off with Python (and Scheme).
Mathematicians are also not upset about Lean. They're upset because they feel like they're becoming redundant. And that has everything to do with LLMs and not Lean.
This is putting the cart before the horse: Progress in verification has been huge because of LLMs. Mathlib PRs spiked at the release of Opus 4.6, any of the big formalizations would not have been here without LLMs.
More surprising to me, OpenAI claims they're doing informal reasoning and only after do the formalization. This seems to match the way in which they release things. Of course they will have Lean in the training data, but I think this supports the mirror hypothesis: We'd have the same progress in mathematics if proof assistants didn't exist, it would just be a pain to verify correctness.
Fully agree on the potential for Lean as a generic programming language.
I have always felt that a huge amount of brain power has to be expended in understanding the jargon and getting used to the machinery. Once we get past that, what people would think are highly challenging subjects become rather simple and logical. An analogy I like to use is old people struggling with simple tech tasks. I remember an uncle of mine who approached me to fix their laptop which wasn't connecting to the internet. Turns out the laptop had not been booted in a while and the public certs shipped with the machine had expired. Said person is a highly accomplished person in their field but was helpless when it came to this task. After I solved the issue, the uncle was eager to know what the problem was and I tried to ELI5 it but to no avail. It is possible I did a really bad job of explaining it but there was too much basic machinery to cover. Why is there a public and private key, what is symmetric/asymmetric, why do certs even expire etc. I couldn't even touch on the foundational math underpinning all of it so I left him in a confused daze.
To any SWE, all this is table stakes but for non-tech people it is way too much jargon. Today, I'm confident my uncle could prompt his way to a working understanding of PKI - heck maybe even some aspects of cryptography and prime number math that makes it work. This is where I see LLMs making a massive difference - they can crunch a massive amount of jargon and leave only the actual trick/idea for you to understand.
This is also what people like Szegedy and Tao have also said - LLMs will make math closer to what SWE is - a lot more people doing it in workmanlike fashion rather than a small community writing papers. At one point, dynamic programming was some research topic that Bellman worked on and now every 20 year old works on tens to hundreds of these problems in the hopes of cracking a job. But I'm sure the Math field will go through some turbulence and I wish them the best. There will always be a need for SMEs who deeply understand a subject and can come up with interesting problems.
Lean isn't super special in that regard. If you know Haskell or OCaml you are already pretty far along in at least being able to read Lean, as it comes out of a similar-enough tradition.
You really have to wrap your head around dependent types and _≡_. In my experience it was far more mind blowing than just FP.
But yes, you have to wrap your head around dependent types.
It's the kind of low yield completionist task that you just don't do without something equivalent to cheap slave labor.
AI makes formalization more accessible and makes it more important: The current superpower of LLM powered research is that the LLM is absolutely relentless, but the relentless is a liability without a source of truth to check against.
While everything seems crazy right now, the building blocks have been coming together for a long time now.
Extraordinary claim requires extraordinary evidence.
Why? I’ve worked a bit with proving systems in my studies, but it seems to me that it is very hard to turn precise mathematical statements into useful programs. Perhaps for the core logic, but GUIs or any other state with the outside world is going to be difficult it seems to me
Software "engineers" really just want to be button pushers and design overly complex Rube Goldberg machines.
Waiting for "i made this" posts for formalized code ...
Before AI it was super tedious to formally express your software models in Lean, with AI this is super easy. See formal verification of consensus core in Ultima Cluster: https://github.com/PeterKnego/ultima_cluster/blob/main/docs/...
Since there can be bugs in its compiler and runtime, they translated the code into Rust (con-ron), and verified the resulting kernel with another Rust-based verification tool.
There is also an ongoing verification project of Lean4, which is written in Lean4 itself. (My mental model is Lean4 := Raku and Lean := Perl)
So we have two verified kernels now, and another is awaiting release.
It's a marketing post at the end of the day is what I'm trying to say. Regardless, Lean is probably the most trustworthy proof assistant on the planet at this point.
Programming as a hand-crafted art is really diminishing fast.
An awful lot of references for arbitrary precision arithmetic are just repackaging Knuth’s explanations, so I wonder if there could in fact be a bug in common (Although you would like to assume every other piece of software using them would have also hit any issues by now, so maybe it is fine)