Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- First of all, this is an amazing result. Second, I'm not too surprised, given all what has happened before.
The thing is: LLMs are not grounded in reality enough as much as we are. Using Lean is exactly what that is: grounding LLMs in reality.
We have (at least) 30 FPS vision, and can detect 5 ms audio delays, we do that in real-time. LLMs have access to some images and large amounts of text. Their propensity is to predict the next token. So the propensity to be additive and just say something (aka predict the next token) is higher than predicting something to stop.
If LLMs would have: - 30 FPS vision - similar hearing ability - an ability to feel their lived experience - consequences to their "life"
They'd be making more intelligent decisions than they are doing now. Simply because they have more context.
Because in this sense, we have a lot more context than LLMs. Yet, I see people sometimes treating them as if they are at the same level as humans because their intelligence is similar. And that might be true, but where they get their data from is vastly different. Given our tasks, they are at a disadvantage. They need to sense more of reality.
Have fun sharing the room with these digital intelligences. Given the topics they can consume, they are already better generalists than any individual. I might be wrong of course, I'd love to meet any individual that's a better generalist than an LLM.
by mettamage - Back in February, I was talking with my PhD advisor about using Lean to formally verify automated optimization modeling outputs. It eventually turned into this paper [1]. It’s been truly incredible to see how much the frontier models have progressed in both autoformalization and automated theorem proving in the last six months. Back in February, it was cool to see them prove the validity of some simple cutting planes. Now it can churn out a min-cut max-flow duality formalization (not to mention FLT). Very exciting times!
I’ll also share a Python package I wrote for automated theorem proving that has been super useful in my own research [2].
- 13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?by KaiserPister
- The proof system is relatively easy to verify.
I am not entirely sure about lean, but the core algebras for systems like lean are in the 100s of lines of code.
You can likely convince yourself it is correct in a weekend or less - especially with an Ai to help you understand it.
by tossandthrow - Not just lean, but math foundation itself, I am not strong expert, but my understanding is that there is no fully recognized axiomatic foundation for modern math, all proposals could lead to some weird results.by andriy_koval
- Nope! :(
Meaning, people and LLMs are finding 1=0 bugs in formal verification tools. I have no idea how likely this is in this case, though!
- Anthropic surely is well aware. Most likely they asked separate agents multiple times to code review the proof and look for exploits.by dist-epoch
- That must have slipped through Kevin Buzzard's review, which is not entirely unplausible with 29500 theorems to verify...
I think they should spend another few billion tokens and let agents try to disprove any of those statements or links between them. Then I'd be a lot more convinced.
by jmusall - It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.by Smaug123
- This is a crucial point. There have been many bugs in Lean (and in other proof assistants for that matter). Proof assistants work well on human input, because it was created with a certain intent.
We simply don’t know what those 13M contain and whether it “makes sense” and doesn’t trigger Lean bugs. (There are “independent” lean verifiers, but historically they contained the same, or similar, bugs.)
by Jaxan - The AI labs have out considerable effort in trying to find and patch lean exploits. They explicitly set agents and have them try to prove false.
> Daniel used OpenAI internal models to discover new soundness issues in the official Lean kernel and runtime
https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...
They found several bugs and they have patched them. Lots of work going into making sure lean is sound.
by kingstnap - We'll increasingly observe announcements of this kind as AI tooling scales. As impressive as agentic coding is, it pales in comparison to the value proposition of medical, mathematical, and physics research.
I optimistically expect to witness the advent of a global 'panacea' in my lifetime thanks to AI's efforts. Cost effective large scale genetic engineering, a cure for every disease, potentially even a cure for aging.
The future is both beautiful and terrifying.
by Vakaiser - I dont think it will happen. AI models are kneecapped. Only a tiny tiny tiny fraction of people are on the list of even being able to use these tools for such things.by rowanG077
- It's wild to think that aging is something that needs to be cured, and isn't a part of the natural human experience. I'm so tired of people trying to play the role of God, as well as people that cheer these sorts of things on.
- What’s interesting is it’s not obvious how this is leveraged to ‘cure disease’. But I’d love to know.the advantage of this is there is a clear measure of success. Here is a rule language. Prove this. You are done when your proof passes. You can sit quietly and spin for billions of tokens.
How does that work for drugs? We can’t let AIs make millions of test drugs and try them out on people.
by CJefferson - > I optimistically expect to witness the advent of a global 'panacea' in my lifetime thanks to AI's efforts
this is a religious belief, maybe you should stop to really examine that (because it might be unintentionally so), but just know that it is obvious to anyone reading these words (anyone who is not mesmerized by technology)
by andersonpico - Note that this proof while impressive does not add any value to mathematics as a human pursuit. But it does show we can throw these LLM beasts at much gnarlier problems than we could have imagined previously. Maybe even formally verify papers the day they are posted?
I'd love to see an e2e compiler or OS kernel verification or Full-stack chip design with formal equivalence checking at each stage that would be pretty cool.
What else is interesting is how they staged this problem : (a) maintain an explicit DAG/roadmap of sub-goals rather than one flat prompt, (b) separate statements from proofs so many agents can work on different nodes without stepping on each other, (c) keep a natural-language index alongside the formal one so search/reuse works... I feel like this is the future of long horizon agents and how you can do work that's making the most of every agent. This approach will likely be baked into the next versions of coding harnesses
by imranq - > Note that this proof while impressive does not add any value to mathematics as a human pursuit.
I don't see how this can be stated with such certainty. We don't yet know what the implications of large scale autoformalization and proof verification will be on the human pursuit of mathematics. I'm open to the idea that it might be a benefit to the human pursuit once the human pursuit adapts.
by jebarker - On a tangential note, I highly recommend this book by Simon Singh. https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)by somberi
- one of the most popular books in india growing up. used to see it everywhereby dominotw
- 100% It is a very insightful bookby raverbashing
- Makes me feel old again. I read this over twenty years ago.by OroPla
- “The Code Book” and “The Simpsons and Their Mathematical Secrets” are also great books by the same author.by wrboyce
- > a team of agents completed the proof in a little under two weeks, consuming about six billion output tokens from a general-purpose internal research model roughly comparable to Claude Fable 5.1.
At $50/M output tokens, this would have cost on the order of $300k (plus a bit for input/prefill tokens) at API rates.
by davmre - What would it cost to make a team of mathematicians do the same?by jensgk
- But also achievable on a $150/mo (CAD) Max 5 subscription (I currently have 11.6B tokens in the last 30 days) according to /usage. It doesn’t break down input vs. output tokens as far as I can tell.by tonyarkles
- And human salaries for those who worked on the prover harness etc. which isn't just standard Fable.
It also uses Prove2Me, which uses a graph like previous automated theorem provers. A fact that LLM hawks have categorically denied here before, with opposition naturally flagged.
Now they have it in writing.
by 3192987 - > Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.
Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model.
by m_w_ - especially compared to existing 129 pages proof by humanby andriy_koval
- It’s common for formal proof efforts about software and hardware to involve thousands to tens of thousands of small lemmas.
13M lines does seem extreme and there is probably a lot of inefficiency given the way the proof was developed. Cutting it down is probably a long road, but is also a very well defined problem that AIs can probably just go do with enough time and budget now.