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

351–360 of 527 posts

Re: Formalizing Fermat's Last Theorem

#351

Post by twiceaday »

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…

Lean is like a statically typed programming language and validity is guaranteed if it compiles. The only room for errors is in translating a non-Lean theorem into Lean, so that you are not proving what you think you are proving.

Re: Formalizing Fermat's Last Theorem

#352

Post by thevivekpandey »

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

Re: Formalizing Fermat's Last Theorem

#353

Post by QuesnayJr »

tatjam wrote: post #206
QuesnayJr wrote: post #147

Earlier quoted context omitted.

Of course it is. The interesting thing is that it was able to produce a Lean proof in 11 days, when there's been an ongoing project for several years to do the same thing (though a somewhat different proof) that is nowhere near done.

I think there's a big misunderstanding going on here, translating the proof to Lean is, well... a translation task. Formalizing the proof in a way that's useful (breaks the proof down into relatively independent blocks that can be used for other maths and, importantly, understood individually) is a quite bigger, more creative endeavor. Not sure if LLMs would be able to do it, maybe yes?

It wasn't clear that LLMs were up to a Lean translation task of this scale until now. The background required to formalize the FLT proof was tremendous, so many people assumed we would have to wait until all of that was formalized in Lean before we could ask it to formalize Wiles' proof. Now it seems like almost any mathematics paper we can ask an LLM to formalize, including all necessary background, and it can just do it.

Re: Formalizing Fermat's Last Theorem

#354

Post by s7atic »

tinfoilhatter wrote: post #107
nutjob2 wrote: post #101

Earlier quoted context omitted.

Most people want more life. For most people it's also the most terrifying part of "the natural human experience". If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?

I assume you mean that dying is the most terrifying pat of the natural human experience. Also, I'm not sure why you infer that me thinking death is a natural part of life, means that I'm happy or eager to die. There are many reasons that people living forever would be a problem for society, the most obvious being an ever-increasing population.

Fertility rates are below replacement, which means that population sizes are convergent. A decreasing population is a more likely future scenario for many western countries, even if human lifespan was indefinite.

Re: Formalizing Fermat's Last Theorem

#355

Post by CaptWorld »

fyredge wrote: post #338
CaptWorld wrote: post #194

Earlier quoted context omitted.

Like? I feel breakthroughs that can be found via AI might help us more in the long term where even previously non AI fields can be helped by AI. So you have specific non AI research in mind that we're underinvesting in? Because the USA is already spending crazy anyway for healthcare and I don't feel like funding is the issue but better incentives, reforms etc

Like funding education. Let's build up human intelligence instead, they seem to have made great breakthroughs in every single field! The US doesn't pay too much to healthcare, they pay too much to health insurance. Too much for too little value

But US also spends too much on education as well. The issue doesn't seem to be funding but the educational reform like in mississippi, where they increased student performance without increasing their budget too much. That's why you see bad k12 educational outcomes compared to the budget spent in blue states. It's all about efficiency. Give AIa chance in few years as I feel it can make great strides.. it's hard to imagine that chatgpt released in 2022 and look at the progress in just few years as it just changed software engineering field entirely.. i expect similar kinda progress where of course humans will still be making breakthroughs but it'll be accelerated with the help of AI.

Spending on health insurance is spending on health care.. Americans want free healthcare but no tax bump so health insurance is a compromise.. when even just ACA was passed and premiums increased, democrats got destroyed at midterms so Americans might be living in la la land.

Re: Formalizing Fermat's Last Theorem

#356

Post by fxd »

s7atic wrote: post #354
tinfoilhatter wrote: post #107

Earlier quoted context omitted.

I assume you mean that dying is the most terrifying pat of the natural human experience. Also, I'm not sure why you infer that me thinking death is a natural part of life, means that I'm happy or eager to die. There are many reasons that people living forever would be a problem for society, the most obvious being an ever-increasing population.

Fertility rates are below replacement, which means that population sizes are convergent. A decreasing population is a more likely future scenario for many western countries, even if human lifespan was indefinite.

[dead]

Re: Formalizing Fermat's Last Theorem

#357

Post by raincole »

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…

The answer is we don't really know [0]:

> In 2026, AIs designed to spot bugs in software were directed at Lean, and found several loopholes which were then fixed. Perhaps related to this effort, a purported disproof of the Collatz conjecture was announced as verified in Lean. However, this proof was soon determined to rely on a bug in Lean, and once the bug was fixed the proof was found invalid

However it's a bit different than the usual 'bugs' we encounter in normal software development. Lean is more like a type checker. If you can write a false proof in Lean then the bug is in Lean itself, not your code.

In other words, Lean can have bugs, but the amount of code we need to check scales with Lean itself, not with the length of proof. Just like the chance that C compiler has bugs doesn't increase as we write more C code. So the 13M lines of code doesn't really matter here.

[0]: https://en.wikipedia.org/wiki/Lean_(proof_assistant)

Re: Formalizing Fermat's Last Theorem

#358

Post by defrost »

s7atic wrote: post #354
tinfoilhatter wrote: post #107

Earlier quoted context omitted.

I assume you mean that dying is the most terrifying pat of the natural human experience. Also, I'm not sure why you infer that me thinking death is a natural part of life, means that I'm happy or eager to die. There are many reasons that people living forever would be a problem for society, the most obvious being an ever-increasing population.

Fertility rates are below replacement, which means that population sizes are convergent. A decreasing population is a more likely future scenario for many western countries, even if human lifespan was indefinite.

Fertility rates are currently below replacement, there's no good reason to imagine they will always be that way, particularly after global population numbers peak and fall to, say, half or a quarter of their peak.

Re: Formalizing Fermat's Last Theorem

#359

Post by musictubes »

_aavaa_ wrote: post #102
sebzim4500 wrote: post #93

Earlier quoted context omitted.

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.

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

And which they could not charge anyone for. Unless these were extra resources that would otherwise go unused it cost them the amount they could have charged for them. Normally I would expect most businesses to make reasonable tradeoffs when it comes to how to allocate resources. I’m not convinced that any of the AI providers should be given that benefit of the doubt.

Re: Formalizing Fermat's Last Theorem

#360

Post by cdelsolar »

Almondsetat wrote: post #269
andriy_koval wrote: post #261

Earlier quoted context omitted.

looks like we are in disagreement

A quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just wrong

What are you nerds fighting about please explain
Post reply on HN