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.