LLMs are pretty good at slogging through. When will they come up with brilliant breakthroughs like Andrew Wiles?
About two month ago: https://en.wikipedia.org/wiki/Jacobian_conjecture
Come on, you can't compare that with Wiles's proof.
Formalizing Fermat's Last Theorem
81–90 of 524 posts
Re: Formalizing Fermat's Last Theorem
#82An aside on Lean and it's massive library of results: As someone who's put non trivial effort into slowly learning geometric algebra, lie theory and other slightly advanced math topics, I have to say my brain cannot read Lean. It feels so unprocessable. I've tried the various intros to Lean multiple times (even before Lean 4 came out) and something about the way Lean proofs are written does not align with how I think…
The nice thing is, once all of these proofs are formalized in a machine-checkable language, it should be relatively straightforward to translate the corpus between different languages, if someone finds something with a nicer syntax.
Re: Formalizing Fermat's Last Theorem
#83> 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.
especially compared to existing 129 pages proof by human
Re: Formalizing Fermat's Last Theorem
#84[deleted]
Re: Formalizing Fermat's Last Theorem
#85Can someone with more knowledge help me with this silly question in my head? >>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems Did a human check the 13 million lines of code? How does QA'ing this type of work works?
There is a simple piece of code that can check simple steps, and many people agree this checker is correct. Then there is a formalization of the theorem which many people agree defines the theorem accurately. Then there is 13 million lines of proof that nobody has read, but the proof checker validated each step. That's enough. So, all you have to verify is the formalization of the theorem, and believe that the proof…
You still have to trust that the AI didn't exploit a bug in the Lean kernel. There was just such an instance of a bug a little over a month ago:
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
Re: Formalizing Fermat's Last Theorem
#86Proving FLT was such a profoundly emotional and spiritual experience for Andrew Wiles, it almost brought a tear to my eye: https://news.ycombinator.com/item?id=49203626 It is truly saddening to think that machines will deprive us of this wonder and experience. But truly exciting to dream about what lies beyond the limits of our biology.
> It is truly saddening to think that machines will deprive us of this wonder and experience. It won't deprive us. Recent video I've watched from Brandon Sanderson, IMO also applies to all the things we love and not just art: https://youtu.be/mb3uK-_QkOo?si=SG1uvGUbN6SOYI_J
If the Riemann hypothesis is solved primarily by a AI system it will not be as awe inspiring as if a human solved it.
That is just how it is.
Re: Formalizing Fermat's Last Theorem
#87> 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.
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.
Re: Formalizing Fermat's Last Theorem
#88Earlier quoted context omitted.
The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled. Note to other users: don’t downvote this kind of comment, answer it.
encode mathematical reasoning in a way that can’t be fooled. I would be a bit careful asserting that in full generality, given https://github.com/James-Hanson/junk-theorems-in-lean
Isn’t there some theorem that any sufficiently complex mathematical languages will have statements that can’t be proven? :)
Re: Formalizing Fermat's Last Theorem
#89> 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.
What would it cost to make a team of mathematicians do the same?
Re: Formalizing Fermat's Last Theorem
#9013M LoC, are we sure it didn't exploit any latent issues in the lean proof system?
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.