Formalizing Fermat's Last Theorem • Hacker News Board

Re: Formalizing Fermat's Last Theorem

#271

Post by SP3269 » Fri, Sep 04, 2026, 10:54 PM UTC

deepsun wrote: post #207

andriy_koval wrote: post #90

Earlier quoted context omitted.

Not just lean, but math foundation itself, I am not strong expert, but my understanding is that there is no fully recognized axiomatic foundation for modern math, all proposals could lead to some weird results.

There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless. You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itse…

Interestingly, in his ICM 2026 lecture, Terence Tao specifically mentioned that Lean is not based on ZFC.

Re: Formalizing Fermat's Last Theorem

#272

Post by andriy_koval » Fri, Sep 04, 2026, 10:55 PM UTC

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

you are entitled to have your opinion :-)

Re: Formalizing Fermat's Last Theorem

#273

Post by sanxiyn » Fri, Sep 04, 2026, 10:55 PM UTC

mnewme wrote: post #186

Do I miss something? But isnt there the whole code and paper of Kevin Buzzard in the training data of Claude?

Yes, but Claude formalized a different proof than Buzzard is trying to, so it helps less than you think. (It certainly helps!)

Re: Formalizing Fermat's Last Theorem

#274

Post by margorczynski » Fri, Sep 04, 2026, 10:55 PM UTC

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?

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.

Re: Formalizing Fermat's Last Theorem

#275

Post by itishappy » Fri, Sep 04, 2026, 10:55 PM 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.

A published formalization is code. I would not think humans have any edge when it comes to citing previously published results.

Re: Formalizing Fermat's Last Theorem

#276

Post by blondie9x » Fri, Sep 04, 2026, 10:57 PM UTC

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…"

Re: Formalizing Fermat's Last Theorem

#277

Post by Philpax » Fri, Sep 04, 2026, 10:58 PM UTC

mikmoila wrote: post #270

johnsmith1840 wrote: post #263

Earlier quoted context omitted.

A literal rock we carved patterns on and shot lightning into has accomplished something no human has. How much more magical do you want this to be? Tool or not it did something you could never have accomplished.

"you could never have accomplished"; I am not able to follow the logic here - there is no "magic" in LLMs, they're built by humans and we know what they do.

We don't know what they do. We shape them, but our understanding of how they get to their result is comparatively minimal.

Re: Formalizing Fermat's Last Theorem

#278

Post by margorczynski » Fri, Sep 04, 2026, 10:59 PM UTC

With how capable and cheap automatic proof verification is becoming I wonder how many proofs assumed to be true by almost all of the math community will be proven false. And not by some marginal easy to fix error by some fundamental flaw in reasoning.

Re: Formalizing Fermat's Last Theorem

#279

Post by mikmoila » Fri, Sep 04, 2026, 11:02 PM UTC

Philpax wrote: post #277

mikmoila wrote: post #270

Earlier quoted context omitted.

"you could never have accomplished"; I am not able to follow the logic here - there is no "magic" in LLMs, they're built by humans and we know what they do.

We don't know what they do. We shape them, but our understanding of how they get to their result is comparatively minimal.

I think you're referring to the fact that the sheer amount of computations is something too time consuming for us to follow? But still it is not "magical" - in theory we could follow all the steps, there's no hidden information.

Re: Formalizing Fermat's Last Theorem

#280

Post by jeremyjh » Fri, Sep 04, 2026, 11:02 PM UTC

margorczynski wrote: post #278

With how capable and cheap automatic proof verification is becoming I wonder how many proofs assumed to be true by almost all of the math community will be proven false. And not by some marginal easy to fix error by some fundamental flaw in reasoning.

I will not be surprised if the number is zero. It should have already happened if it were possible.

Proving that a conjecture is false is very different than what you are proposing. You are proposing an existing proof is simply wrong, that the proof can be checked in Lean, and that no one has bothered to check it yet.