Formalizing Fermat's Last Theorem • Hacker News Board

Re: Formalizing Fermat's Last Theorem

#371

Post by aureianimus » Sat, Sep 05, 2026, 5:25 AM UTC

gorgolo wrote: post #367

thevivekpandey wrote: post #352

Earlier quoted context omitted.

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

> That theorem statement is correctly encoded (FLT has a very short 1 liner description really) As someone not very familiar with Lean, does it really just depend on the entry point / theorem being correctly encoded? Can intermediate statements ever be mis encoded or misinterpreted, or is this what would count as a “bug in the Lean compiler”?

There's no guarantee that the intermediate statements match the informal mathematical intermediate statements, but if there is a mismatch, then this has to be repaired elsewhere to yield a proof that passes the Comparator tool. Running this tool indeed reduces the correctness question to what the parent comment mentioned.

Re: Formalizing Fermat's Last Theorem

#372

Post by artifact_44 » Sat, Sep 05, 2026, 5:25 AM UTC

lukewarm707 wrote: post #306

CaptWorld wrote: post #243

Earlier quoted context omitted.

Which metrics are poisoned? Can you provide your arguments for why Good heart's law applies here and how and which metrics are bad measures? For b, can the writer at least provide their own thoughts or are they gonna leave it as exercise for some others to fill in?

a) classic goodhart is using gdp as a measure of prosperity. the government sets a prosperity target. to increase prosperity the government makes workers increase gdp by working 16 hours per day. gdp increases. prosperity is up! the metric is now poisoned. b) how and why could human welfare get worse in a growing economy, really the list is long. one example, unsustainable industries grow but do not create surplus. t…

[dead]

Re: Formalizing Fermat's Last Theorem

#373

Post by raincole » Sat, Sep 05, 2026, 5:31 AM UTC

gorgolo wrote: post #367

thevivekpandey wrote: post #352

Earlier quoted context omitted.

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

> That theorem statement is correctly encoded (FLT has a very short 1 liner description really) As someone not very familiar with Lean, does it really just depend on the entry point / theorem being correctly encoded? Can intermediate statements ever be mis encoded or misinterpreted, or is this what would count as a “bug in the Lean compiler”?

If you just "translate" an existing proof step by step to Lean, then of course you could mis-encode the intermediate statements too. But if you mis-encode the steps and still pass Lean check, it means you found a new proof! (Or you found a bug in Lean)

Re: Formalizing Fermat's Last Theorem

#374

Post by robotpepi » Sat, Sep 05, 2026, 5:32 AM UTC

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.

> reduce the burden of refereeing new work.

As a professional mathematician, I rarely need to worry about the correctness of a paper. The main difficulty of writing a review is instead understanding what the results of the paper mean in its context, how the results are presented, etc.

Re: Formalizing Fermat's Last Theorem

#375

Post by artifact_44 » Sat, Sep 05, 2026, 5:40 AM UTC

dakolli wrote: post #126

yesitcan wrote: post #49

Earlier quoted context omitted.

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…

[dead]

Re: Formalizing Fermat's Last Theorem

#376

Post by drchickensalad » Sat, Sep 05, 2026, 5:47 AM UTC

chpatrick wrote: post #308

btilly wrote: post #302

Earlier quoted context omitted.

Amazon didn't make a profit because they were reinvesting money into starting new lines of business. Basically there was a choice between taking the money, and growing. They chose growth.

As opposed to...?

Spending all your money on extremely quickly depreciating graphics hardware and model training

Re: Formalizing Fermat's Last Theorem

#377

Post by Jaxan » Sat, Sep 05, 2026, 5:48 AM UTC

black_knight wrote: post #191

andriy_koval wrote: post #83

Earlier quoted context omitted.

especially compared to existing 129 pages proof by human

A human can cite previous published results. I am sure a lot of this development was formalising the prerequisites.

Wouldn’t a lot already be in leans mathlib?

Re: Formalizing Fermat's Last Theorem

#378

Post by emil-lp » Sat, Sep 05, 2026, 6:00 AM UTC

jascination wrote: post #289

margorczynski wrote: post #274

Earlier quoted context omitted.

Buzzard was given 1kk GBP and 5 years and his goal I think wasn't the full thing like Anthropic did. So much more cash and orders of magnitude more time. The proof is about 5x the whole Mathlib library which was developed over many years by dozens of people.

1kk? Why not say 1M?

You mean why not say £ 1MM?

Re: Formalizing Fermat's Last Theorem

#379

Post by throw567643u8 » Sat, Sep 05, 2026, 6:06 AM UTC

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…

With the size of the proof object, a potential buffer overflow comes to mind.

Re: Formalizing Fermat's Last Theorem

#380

Post by JacobAsmuth » Sat, Sep 05, 2026, 6:09 AM UTC

qbane wrote: post #179

vagab0nd wrote: post #156

> it wrote 13 million lines of Lean Is this basically like opening up a black box and seeing 13 million gears all rotating seemingly randomly and still having no idea how the machine actually works?

That is already the case for most neural networks and LLMs.

Except there's 10 trillion gears