Suppose lean in its current state existed 15 years ago, and suppose the math community eagerly started contributing en masse to a shared repository of code. How much of the breakthroughs and longstanding questions in mathematics that we’ve seen answered this year do you think we would have solved?
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.
This is my hypothesis too. I work with LLMs daily. I use frontier models all the time, and I work in a startup that trains its own special-purpose models. At no point in the course of my work do I see anything resembling superhuman intelligence. I see superhuman stupidity, ie. stupidity so extreme that it exceeds what any human is capable of by orders of magnitude. So where are the superhuman math results coming from? Simple: translation. I've already thought this for a long time, that math is an obsfucated field and that programming already makes it far simpler to understand. So you train a machine to throw tons of compute at translating math into programming, and blow the field out of the water because it's effectively been deobfuscated. Math proofs had a sort of security by obscurity; they were not genuinely supremely difficult, but rather very few people worldwide worked on them and their work was heavily obscured, so the great deobfuscation machine comes along and trivialises that aspect and suddenly the facade crumbles. I think all of this could have been achieved a long time ago had humans done the deobfuscation, but there wasn't sufficient programming <--> maths cross-domain expertise or financial incentive to develop it.
I don't understand what you're saying. Writing lean doesn't make it easier to formulate a proof. These LLMs are writing natural language proofs then formalizing after the NL proof is done. If humans were theorizing and exploring open problems in lean for the last 15 years, we'd be moving much slower than we have been with natural language.
> Suppose lean in its current state existed 15 years ago, and suppose the math community eagerly started contributing en masse to a shared repository of code. How much of the breakthroughs and longstanding questions in mathematics that we’ve seen answered this year do you think we would have solved?
(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.
Is that because you were starting from scratch and working alone, though?
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.
Make a trivial adjustment to your final proposition and it would still hold, no?
> 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 proposal is that multiple checkers are unlikely to all have the same bugs so the more kernels you can use to check the results the more likely it is that the proof/code is consistent & correct (modulo set theoretic assumptions necessary for the correctness of the kernel).
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.
https://github.com/Verilean/sparkle
(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.
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.
> 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.