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

121–130 of 526 posts

Re: Formalizing Fermat's Last Theorem

#121

Post by Jblx2 »

tossandthrow wrote: post #63
KaiserPister wrote: post #39

13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?

The proof system is relatively easy to verify. I am not entirely sure about lean, but the core algebras for systems like lean are in the 100s of lines of code. You can likely convince yourself it is correct in a weekend or less - especially with an Ai to help you understand it.

the Nanoda type-checker for Lean is ~5,000 lines of Rust:

https://leodemoura.github.io/blog/2026-3-16-who-watches-the-...

...and for those who are looking to roll-their-own:

https://ammkrn.github.io/type_checking_in_lean4/title_page.h...

...and some thoughts on putting stuff in the kernel:

https://lawrencecpaulson.github.io/2026/07/30/Collatz.html

Re: Formalizing Fermat's Last Theorem

#122

Post by dist-epoch »

alch- wrote: post #115
_aavaa_ wrote: post #102

Earlier quoted context omitted.

Unlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn’t charge themselves.

I don't think Anthropic is turning a profit ;)

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

Re: Formalizing Fermat's Last Theorem

#123

Post by dang »

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.

Thanks! I've added that link to the toptext.

I'd really like to make it the top link (and relegate https://www.anthropic.com/research/formalizing-fermats-last-... to the toptext) since HN has been tracking the work of https://news.ycombinator.com/user?id=kevinbuzzard for a long time and we're big fans. But I guess that would be overkill.

Re: Formalizing Fermat's Last Theorem

#124

Post by t_gamer_kle »

sigmar wrote: post #12

>The speed with which we were able to produce this proof demonstrates that it is now possible to formalize large swaths of mathematics, which may both catch errors in the common body of mathematical proofs and reduce the burden of refereeing new work. ^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.

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

Re: Formalizing Fermat's Last Theorem

#125

Post by dist-epoch »

tonyarkles wrote: post #91
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.

When writing software with Codex 95+% of tokens are cache, I would assume the same in your case (if you also used it for coding).

Re: Formalizing Fermat's Last Theorem

#126

Post by dakolli »

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.

Please tell me how AI is going to make regular people's lives better. You optimisitic types keep saying "just wait, its going to cure diseases" without any outlook on how thats going to happen. You're actually just repeating marketing jargon from AI companies who want people to think they're going to possibly live longer if you let them build more datacenters, so they can make another 30%. Its all about money, thats it.

It seems to me that it is making everyone (including myself and the researchers we need to cure diseases) lazy and dependent on thinking machines owned by tech companies. Just how autocomplete and gps made us worse at spelling and navigating, llms make us less able to exercise our ability to think and problem solve. This will have 100% strictly negative consequences on you and the world as a whole. .

And even if there was a cure to many diseases the eugenics types who are embedded in worldwide power structures definately arent going to share that universally.

Re: Formalizing Fermat's Last Theorem

#127

Post by dist-epoch »

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?

More importantly how many years it would take.

Re: Formalizing Fermat's Last Theorem

#128

Post by dist-epoch »

andriy_koval wrote: post #83
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.

especially compared to existing 129 pages proof by human

Insert meme with 200 pages needed to prove 1+1=2 rigurously

Re: Formalizing Fermat's Last Theorem

#129

Post by floweronthehill »

ojo-rojo wrote: post #95

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.

I wonder if AI can come up with mathematical conjectures. As in, they feel it's right but can't prove it. What even happened in Fermat's brain to sense it was true?

Re: Formalizing Fermat's Last Theorem

#130

Post by paxys »

sigmar wrote: post #12

>The speed with which we were able to produce this proof demonstrates that it is now possible to formalize large swaths of mathematics, which may both catch errors in the common body of mathematical proofs and reduce the burden of refereeing new work. ^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.

Nah they should have released it in a 14-part tweet instead.
Post reply on HN