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

91–100 of 526 posts

Re: Formalizing Fermat's Last Theorem

#91

Post by tonyarkles »

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.

But also achievable on a $150/mo (CAD) Max 5 subscription (I currently have 11.6B tokens in the last 30 days) according to /usage. It doesn’t break down input vs. output tokens as far as I can tell.

Re: Formalizing Fermat's Last Theorem

#93

Post by sebzim4500 »

BeetleB wrote: post #27
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...

It sounds plausible they spent more, given the output tokens (6 billion of them) would cost $300k at API prices and presumably there will have been many more input tokens than output tokens.

Re: Formalizing Fermat's Last Theorem

#95

Post by ojo-rojo »

I'm really impressed by mathematicians. It's cool that Fermat had the intuition to conjecture that "aⁿ + bⁿ = cⁿ" could not be satisfied for n > 2, and that other mathematicians can create proofs, and that others still can understand AI's formulation of those proofs. Really cool.

Re: Formalizing Fermat's Last Theorem

#96

Post by justonepost2 »

yesitcan wrote: post #49
dakolli wrote: post #30

Earlier quoted context omitted.

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.

So much doom and gloom on this site. Makes it almost not worth reading.

maybe that's because the doom and gloom is the transparently correct outcome?

Re: Formalizing Fermat's Last Theorem

#97

Post by dudefeliciano »

yesitcan wrote: post #49
dakolli wrote: post #30

Earlier quoted context omitted.

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.

So much doom and gloom on this site. Makes it almost not worth reading.

Right let's give those AI companies a break, it's not like swarms of autonomous agents are committing felonies

Re: Formalizing Fermat's Last Theorem

#98

Post by sebzim4500 »

tinfoilhatter wrote: post #75
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…

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.

I hope you keep these horrible thoughts to yourself if you ever walk through a paediatric hospital

Re: Formalizing Fermat's Last Theorem

#99

Post by sebzim4500 »

rowanG077 wrote: post #28
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.

Even in a world where these models are heavily restricted, surely the likes of cancer researchers will be among those who have access

Re: Formalizing Fermat's Last Theorem

#100

Post by bananaflag »

jameshart wrote: post #59
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.

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

I am really interested in whether AI will find a significantly easier (1920 level or so) proof of FLT.
Post reply on HN