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

21–30 of 524 posts

Re: Formalizing Fermat's Last Theorem

#21

Post by arjie »

kdavis wrote: post #2

Impressive! Buzzard's group[1] got scooped. [1] https://github.com/ImperialCollegeLondon/FLT

Seems to have taken it in good spirit:

> We shared the resulting proof with Kevin Buzzard, who said:

> > This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.

Re: Formalizing Fermat's Last Theorem

#24

Post by c7b »

rao-v wrote: post #6

An 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…

If you're doing it for fun anyway, why not use the language that gives you the most pleasure?

Re: Formalizing Fermat's Last Theorem

#25

Post by bluecalm »

Very impressive! I was a child when that proof came out. I've read a book about it a few years later and used it on my final high school exam. I remember some friends trying to understand parts of it at univ. It was all like black magic to me and the vibe was "maybe a few people in the world understand it".

I hope soon enough we will have one of the big ones proved by AI!

Re: Formalizing Fermat's Last Theorem

#27

Post by BeetleB »

lalitmaganti wrote: post #3

I suggest also reading Kevin Buzzard's blog post which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h... Provides great context on this accomplishment, what it means but also doesn't mean.

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

Re: Formalizing Fermat's Last Theorem

#28

Post by rowanG077 »

Vakaiser wrote: post #9

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 agi…

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.

Re: Formalizing Fermat's Last Theorem

#30

Post by dakolli »

atleastoptimal wrote: post #18

It seems clear AI has the potential to perform any cognitive task at far greater speeds, reliability, and scale than any human. The question is whether it will be allowed to scale to that point, and what will happen to humans after this occurs.

You'll get mass poverty and violence which the owners of AI will qwell with AI surveillance and weapons. AI will be used to pit us against eachother and justify wars to keep us busy. Fun times ahead.

Not sure why anyone is excited about this tech.

Post reply on HN