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

421–430 of 533 posts

Re: Formalizing Fermat's Last Theorem

#421

Post by kinj28 »

irthomasthomas wrote: post #149
alch- wrote: post #115

Earlier quoted context omitted.

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

Because of the ongoing training costs. They are certainly making a healthy profit margin on inference.

I would like to imagine accounting inference revenue on trained model and the depreciation cost for training that specific model must already been capitalized + compute to serve would be a net positive margin business. Ongoing training must rather be for future models.

But again once future models arrive they would render older models useless, so the asset must be depreciating really fast.

Would love someone to throw light on revenue and cost recognition at the unit level for this.

Re: Formalizing Fermat's Last Theorem

#422

Post by well_ackshually »

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?

1 million dollars reinvested in the economy by a bunch of math nerds that need to buy food, get housing, pay for services, or 300k in Anthropic's pocket? I wonder which one makes society better off, hmmmm, very complicated question, nobody can answer that.

Re: Formalizing Fermat's Last Theorem

#423

Post by cindyllm »

well_ackshually wrote: post #422
jensgk wrote: post #89

Earlier quoted context omitted.

What would it cost to make a team of mathematicians do the same?

1 million dollars reinvested in the economy by a bunch of math nerds that need to buy food, get housing, pay for services, or 300k in Anthropic's pocket? I wonder which one makes society better off, hmmmm, very complicated question, nobody can answer that.

[dead]

Re: Formalizing Fermat's Last Theorem

#424

Post by voidhorse »

herbcso wrote: post #350

So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That…

To me, a lot of the child comments on this thread are technically correct (the best kind) in that, yes correctness bugs in Lean boil down to compiler bugs in a language like lean.

What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode is still a major problem and yes, extremely difficult when you have that many lines to pore over. But, if you're using LLMs to vibe code millions of lines of "proof" you've already stopped caring about that and presumably given your critical reasoning and concern over to pure faith in machine gods anyway.

Re: Formalizing Fermat's Last Theorem

#425

Post by thrance »

thevivekpandey wrote: post #352
herbcso wrote: post #350

So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That…

In lean, a theorem is specified by a type (in their highly complex "dependent type system") and proof is specified by a code that produces a term of that type. If the compiler certifies that the code indeed produces a term of that type, then the proof is correct. So, only need to trust: (1) That theorem statement is correctly encoded (FLT has a very short 1 liner description really) (2) Lean compiler is correct

And (3) the axioms are correctly encoded too.

Re: Formalizing Fermat's Last Theorem

#426

Post by latent-person »

voidhorse wrote: post #424
herbcso wrote: post #350

So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That…

To me, a lot of the child comments on this thread are technically correct (the best kind) in that, yes correctness bugs in Lean boil down to compiler bugs in a language like lean. What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode is still a major problem and yes, extremely difficult when you have that many lines to pore over. But, if you're using LLMs t…

From the article:

> The finished proof was checked by Lean; it uses just Lean’s three standard axioms, and a comparator confirmed that the theorem’s statement matches Mathlib’s own statement of FLT.

So it proved the statement of FLT made independently in Mathlib. So no reason to not trust it proved the correct thing.

Re: Formalizing Fermat's Last Theorem

#427

Post by FartyMcFarter »

voidhorse wrote: post #424
herbcso wrote: post #350

So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That…

To me, a lot of the child comments on this thread are technically correct (the best kind) in that, yes correctness bugs in Lean boil down to compiler bugs in a language like lean. What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode is still a major problem and yes, extremely difficult when you have that many lines to pore over. But, if you're using LLMs t…

> What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode

I don't think the comments are missing that at all. If the Lean compiler itself is bug-free, we can trust its verification of the 13 million lines of code. We don't need to verify them by hand.

The encoding of the theorem itself needs to be trusted, as does the compiler. The proof doesn't need to be trusted, it gets checked by the compiler.

Re: Formalizing Fermat's Last Theorem

#428

Post by FartyMcFarter »

throw567643u8 wrote: post #411
throw-qqqqq wrote: post #409

Earlier quoted context omitted.

Buffer overflows are trivial to check for at runtime (~proof-checking-time) and Lean does this. Just like Java does it. I’d wager a million gazillion bucks that this is not the case.

So would you also say no chance of a stack overflow or any type of surreptitious storage overflow anywhere in the runtime do you think?

Stack overflows are also trivial to check for, if one wants to. It's just comparing two pointers, plus checking for arithmetic overflow (in case the pointers run past the maximum value of the pointer type).

Re: Formalizing Fermat's Last Theorem

#429

Post by not-so-darkstar »

thevivekpandey wrote: post #352
herbcso wrote: post #350

So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That…

In lean, a theorem is specified by a type (in their highly complex "dependent type system") and proof is specified by a code that produces a term of that type. If the compiler certifies that the code indeed produces a term of that type, then the proof is correct. So, only need to trust: (1) That theorem statement is correctly encoded (FLT has a very short 1 liner description really) (2) Lean compiler is correct

What if the mathematical objects are not encoded "correctly"?

For example, everyone knows that the natural numbers and simple data structures like lists or trees can be encoded with inductive types, but what about the new objects introduced by the proof?

Re: Formalizing Fermat's Last Theorem

#430

Post by Smaug123 »

voidhorse wrote: post #424
herbcso wrote: post #350

So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That…

To me, a lot of the child comments on this thread are technically correct (the best kind) in that, yes correctness bugs in Lean boil down to compiler bugs in a language like lean. What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode is still a major problem and yes, extremely difficult when you have that many lines to pore over. But, if you're using LLMs t…

Fortunately FLT is an extremely simple statement. Much easier to satisfy yourself that its statement is what you wanted to say than it would be for most statements of interest!
Post reply on HN