Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Formalizing Fermat's Last Theorem

anthropic.com

Post reply on HN
Print view View original

221–230 of 523 posts

Re: Formalizing Fermat's Last Theorem

#221

Post by mswphd »

jrflo wrote: post #17

Holy shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?

not really. it's one of the most difficult ones so far for sure, but pales in comparison to something like the classification of finite simple groups.

This was initially "completed" in the 80s. You can see the timeline for cleaning up the proof in e.g. this mathoverflow answer

https://mathoverflow.net/questions/114943/where-are-the-seco...

it's something that some people have been waiting decades for, and is not yet completed.

Re: Formalizing Fermat's Last Theorem

#223

Post by HappyPanacea »

salomonk_mur wrote: post #132
t_gamer_kle wrote: post #124

Earlier quoted context omitted.

Forgive the authors of the article for assuming readers would complete it.

For any body of text (or in general, any exposition of any kind), the responsibility to explain the value of the article is very much in the author's side. Explaining the value of what you are showing should always go towards the start. Else, why would anyone bother with the rest?

Buzzard is writing for his blog audience - mostly mathematicians and not the casual visiting HN user.

Re: Formalizing Fermat's Last Theorem

#224

Post by mswphd »

CaptWorld wrote: post #184
bobmarleybiceps wrote: post #112

Earlier quoted context omitted.

guaranteed, up to lean itself having bugs that are exploited by the LLM :shrug:

Do you have proof of this bug or something? Is this just envy against computers now ?

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...

Re: Formalizing Fermat's Last Theorem

#225

Post by jovas »

glimshe wrote: post #205

"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenst…

Yes, I'm a mathematician.

But not an expert on this.

While I don't know the specifics, and someone more "in-the-field" than me would recognize all the "named" theorems etc

I am aware that there have been minor issues that have come up with the formalization specifically, and that previous proofs for lower values of n were always needed.

Though it used to be n=5 and lower needed to be checked.

Re: Formalizing Fermat's Last Theorem

#226

Post by andriy_koval »

deepsun wrote: post #207
andriy_koval wrote: post #90

Earlier quoted context omitted.

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.

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.

Re: Formalizing Fermat's Last Theorem

#227

Post by nearbuy »

jensgk wrote: post #89
davmre wrote: post #74

> 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?

The Kevin Buzzard post linked at the top says they budgeted £1M over 5 years for a smaller proof.

Re: Formalizing Fermat's Last Theorem

#228

Post by skobes »

m_w_ wrote: post #7

> 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.

Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct?

How have we not merely substituted one verification problem for another?

Re: Formalizing Fermat's Last Theorem

#230

Post by CogDisco »

glimshe wrote: post #205

"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenst…

Yep. While I'm not focussed on these areas, I know enough from scoping out a "learn about the proof of FLT" course that it's covering all the usual suspects and says the right-enough words. Patching their weaker results with someone else's seem like a good strategy (and I could find the result on arXiv so it isn't obviously hallucinated).

This is very different to believing the proof, which would require at least a pass understanding the general approach, seeing that it all actually fits together, then going deeper. At some point you transition to relying on the Lean all hanging together, but as mathematicians we all draw that line somewhere.

But yeah, makes sense. Same thing if you saw news on someone's new database technique to improve performance. If they say the right words, don't say the wrong words, and if you cared enough you'd do spot checks proportional to the claim. If pressed you'd examine the source code, and run independent checks. But if smells roughly right, that's a good first approximation.

Post reply on HN