Looking forward to the 5 billion LoC proof of the Riemann hypothesis.
If AI manages to prove, or disprove, I wonder what would Clay Foundation do for the prize.
Formalizing Fermat's Last Theorem
321–330 of 524 posts
Re: Formalizing Fermat's Last Theorem
#322I call bullshit on 13 million lines makes no sense
The repo is public. You can just go look! It's really not that surprising; FLT is huge and has a ton of dependencies that need to be implemented, and there's a degree of sloppification that is probably blowing up the size by a few factors.
Re: Formalizing Fermat's Last Theorem
#323Ok, let’s get a rabid pack of agents cranking on P = NP? next!
Re: Formalizing Fermat's Last Theorem
#324Earlier quoted context omitted.
"I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money…" Gives you an idea of the scale...
I burned $70 on fable 5.1 Max in about 2 hours. I suggest never using fable 5.1 on higher than High reasoning unless someone else is paying for it.
Yeah, "major conjecture proved" with unlimited token budget bankrolled by trillion dollar firm.
Re: Formalizing Fermat's Last Theorem
#325Earlier quoted context omitted.
There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless. You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itse…
> Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic. Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems.
ZFC has greater consistency strength than PA.
If we take ZFC (or some other set theory) as our meta theory, we can easily see that the axiom of infinity (of ZFC) gives a set of natural numbers (using the von Neumann encoding), which, when equipped with the successor function, is a model of the natural numbers.
Re: Formalizing Fermat's Last Theorem
#326Earlier quoted context omitted.
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.
Most people want more life. For most people it's also the most terrifying part of "the natural human experience". If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?
Yes, I think it's a problem for society. Death in old age frees up social, economic, physical, and political resources for the next generation of the living. If the rich and powerful escape death, because after all they will the people with the resources to do so, society will lose the adaptability and natural change that comes from new generations taking the reins.
Re: Formalizing Fermat's Last Theorem
#327Earlier quoted context omitted.
as mentioned elsewhere, there was a bug in the lean kernel exploited by AI to prove a false statement roughly a month ago https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
Got it. Thanks. I feel people are using this single story to downplay this feat. There's definitely a chance but I don't see any indication of similar bugs in here or the openai's proofs that were created a month ago as i think these companies might've vetted it enough and the other team who's working on similar lean proof for this also seems to have acknowledged this feat
How about all of these bugs from last week?
https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...
...I'm not saying this FLT result is compromised. I suppose things depend on your perspective where we are on the spectrum of "finding more bugs means there are fewer left to discover" vs. "finding more bugs probably means there are still unexplored corners out there".
Re: Formalizing Fermat's Last Theorem
#328Earlier quoted context omitted.
ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.
do we know if claude's formalization is built on top of zfc and not zfc+extra? zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.
Within a given inference system, one can define concepts. This doesn’t add any axioms. It is, in essence, just a way to abbreviate things.
Re: Formalizing Fermat's Last Theorem
#329Hmm kind of funny, some years ago someone claimed LLMs can do math, and I replied if it could prove fermants theorem:
https://news.ycombinator.com/item?id=33176996#33177939
> Now try to make a computer prove that there are no natural numbers a,b,c; so that a^n + b^n = c^n for any n > 2.
> > Shifting the goal posts a bit, aren't we?
I guess the goalposts did change a bit, and in a pretty short time.
Re: Formalizing Fermat's Last Theorem
#330Earlier quoted context omitted.
looks like we are in disagreement
That increases the likelihood that they are right. > support your point with explanation or be ignored :-) Anyone who says "Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems" and isn't joking warrants a permanent ignore. https://math.stackexchange.com/questions/1366560/why-does-g%... https://math.stackexchange.com/questions/1090437/how-to-prov.…
imo, those two links are example of rather low quality weird math discussions, but you can keep your opinion