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

151–160 of 526 posts

Re: Formalizing Fermat's Last Theorem

#151

Post by vessenes »

Jblx2 wrote: post #85
stabbles wrote: post #60

Earlier quoted context omitted.

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

True, .. and. In this case, the original proof is considered rigorously checked, so finding a bug in the kernel would be nice to know about, but in my opinion would not take away from the accomplishment (FLT in lean using agents) nor the many benefits of getting these mathematical objects formalized and usable in Lean in the future.

Re: Formalizing Fermat's Last Theorem

#152

Post by fn-mote »

hyperhello wrote: post #88
stratos123 wrote: post #71

Earlier quoted context omitted.

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

This would be funny if it were relevant. Seems like a statement about false negatives instead of false positives.

False negative = could not find a proof of a true theorem.

False positive = erroneous proof of a theorem.

Re: Formalizing Fermat's Last Theorem

#153

Post by vatsachak »

This is quite useless actually. The whole point of formalizing FLT was to clean up modern number theory into reusable abstractions that prove it.

If its 13 million LoC, it might involve so much spaghetti that its unusable other than the result

Re: Formalizing Fermat's Last Theorem

#157

Post by bjourne »

bigstrat2003 wrote: post #143
bjourne wrote: post #36

Earlier quoted context omitted.

Yep. There may be only 25-50 people alive today in the whole world who can credibly claim to understand Wiles' proof. Now we add an LLM to that list. Absolutely mind-blowing stuff.

> Now we add an LLM to that list. No we cannot. LLMs do not, by their very nature, understand a single thing. You are giving far too much credence to hype and marketing.

A meme free of charge for you, sir: https://www.reddit.com/r/singularity/comments/1jl5qfs/its_ju...

Re: Formalizing Fermat's Last Theorem

#158

Post by CaptWorld »

caughtinthought wrote: post #146
dist-epoch wrote: post #122

Earlier quoted context omitted.

Neither did Amazon for it's first 25 years ;)

I think you're missing the point of the comment you responded to, lol.

Regardless the profit margin as a talking point seems to be bad as AI as a tech might never be reversed whether anthropic failed or succeeded. Indeed it's imperative we subsidize AI companies and tech to make them explore more solutions to scientific problems which has a downstream effect on human flourishing.

Re: Formalizing Fermat's Last Theorem

#159

Post by vlovich123 »

zamadatix wrote: post #137
jameshart wrote: post #59

Earlier quoted context omitted.

There is no way Fermat could have fit that in the margin. Definitely vindicated.

While pretty much everyone is certain Fermat was mistaken in believing he had a valid proof for the theorem, this is an expanded (compared to proof presentations) version of one proof - not the shortest presentation of the shortest valid proof.

Given the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won’t fit in the margin.

My strong hunch is that it was a joke - he knew how difficult the problem was and claiming he had a solution was I think a huge motivating factor for many mathematicians trying to prove it. The greatest nerd snipe troll in history.

Post reply on HN