Formalizing Fermat's Last Theorem • Hacker News Board

Re: Formalizing Fermat's Last Theorem

#521

Post by aurareturn » Sun, Sep 06, 2026, 10:51 AM UTC

Brian_K_White wrote: post #520

aurareturn wrote: post #517

Earlier quoted context omitted.

Well, it's taken 4 billion years for life to evolve into humans to be able to do math. That's a lot of resources, right? Likewise, LLMs also needed the same amount of evolution. My point is that it's silly to make these comparisons on resources. A single SOTA trained LLM isn't just doing advanced math research. It's used by hundreds of millions or even billions daily for various tasks. It's just a tool humans invente…

It's just a wildly inefficient tool whos inefficiency is obscured so no one realizes how bad it is and everyone thinks the good part is the only part.

It doesn’t seem so inefficient to me. It seems incredibly efficient in workplace productivity.

Re: Formalizing Fermat's Last Theorem

#522

Post by deepsun » Sun, Sep 06, 2026, 11:27 AM UTC

deterministic wrote: post #342

deepsun wrote: post #207

Earlier quoted context omitted.

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…

Lean is based on Type Theory not ZFC.

I always wanted to, say, look at any theorem and see what axiomatic it requires. Or in other way, see the theorem tree like in the article under a different set of axioms.

Of course, for some results there are proofs discovered only under one axiomatic, but it's true under some others as well, just the proof wasn't discovered yet.

Re: Formalizing Fermat's Last Theorem

#523

Post by Brian_K_White » Sun, Sep 06, 2026, 11:36 AM UTC

aurareturn wrote: post #521

Brian_K_White wrote: post #520

Earlier quoted context omitted.

It's just a wildly inefficient tool whos inefficiency is obscured so no one realizes how bad it is and everyone thinks the good part is the only part.

It doesn’t seem so inefficient to me. It seems incredibly efficient in workplace productivity.

Le duh.

Re: Formalizing Fermat's Last Theorem

#524

Post by auggierose » Sun, Sep 06, 2026, 12:54 PM UTC

vitriol83 wrote: post #518

auggierose wrote: post #511

Earlier quoted context omitted.

Yes. But that is a problem for pure mathematics, not for society. I think that pure mathematics is over. At the same time, applied mathematics will probably subsume most of pure mathematics. Fermat's theorem now is applied mathematics! It will be used to improve implementations of proof assistants for a long time.

facepalm yet pure mathematics has been instrumental in all scientific progress in modern human history including LLMs, very short sighted view

Yes, it has been. And in the form of applied mathematics it will continue to be. It is not so much that pure mathematics disappears, but that in the future there will be just mathematics, and of course it is applied. You would be surprised what kind of mathematics appears when you actually try to formalise your applications properly. It pretty much includes everything that is thought of as pure mathematics today, and much more.

Re: Formalizing Fermat's Last Theorem

#525

Post by DoctorOetker » Sun, Sep 06, 2026, 3:36 PM UTC

fspeech wrote: post #492

DoctorOetker wrote: post #486

Earlier quoted context omitted.

I wish they would cryptographically sign the repository, so potential Lean "exploits" can be discovered in due time.

I don't think the truth of the theorem is ever in doubt so any attack would be silly. But the proof would enable tutorials like this: https://github.com/htzh/flt_for_human/blob/main/math/001-fre... which would be hard to do without a proof outline as agents are not good at math per se, even though they are very knowledgeable and capable.

I don't dispute the truth of the theorem (since I possess my own proof of it, much more concise than the putative Lean or Wiles proofs, i.e. just a few pages).

The Lean system has already experienced soundness bugs.

The question is, will future generations doublecheck this proof with a frozen Lean system of today? There is a lot of incentive in having LLM's be the first to find high profile theorems like this.

I wouldn't vouch my hand in fire in asserting the validity of this gigantic proof.

Re: Formalizing Fermat's Last Theorem

#526

Post by ddosmax556 » Sun, Sep 06, 2026, 3:57 PM UTC

3192987 wrote: post #87

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.

And human salaries for those who worked on the prover harness etc. which isn't just standard Fable. It also uses Prove2Me, which uses a graph like previous automated theorem provers. A fact that LLM hawks have categorically denied here before, with opposition naturally flagged. Now they have it in writing.

Your comment appears to imply that the fact that LLMs used prove2me makes their accomplishment in any way less powerful. But consider that we just witnessed an AI system generate an automated proof that was previously unthinkable within 11 days and 300k+ of money. What tools were used along the way is kind of irrelevant, would you not say?