Formalizing Fermat's Last Theorem • Hacker News Board

Re: Formalizing Fermat's Last Theorem

#31

Post by aquafox » Fri, Sep 04, 2026, 7:20 PM UTC

faitswulff wrote: post #20

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’m not very good at mathematics, but it seems like Kevin should take his girlfriend on trips more often for the good of all mathematicians.

We should start a gofundme to send him 2 months to a remote tribe in the Amazon. Chances are, we see the Riemann hypothesis and twin prime conjecture proven. ;)

Re: Formalizing Fermat's Last Theorem

#32

Post by sweetheart » Fri, Sep 04, 2026, 7:20 PM UTC

anony-123 wrote: post #29

So, what I am thinking is that, the AI generated numbers or tried to find numbers "a", "b" and "c" to check if aⁿ + bⁿ = cⁿ Can not we do it by code?

Lean _is_ code. FLT cannot be proven by exhaustion because it's domain is an infinite set: the natural numbers above 2.

Re: Formalizing Fermat's Last Theorem

#33

Post by estetlinus » Fri, Sep 04, 2026, 7:21 PM UTC

anony-123 wrote: post #29

So, what I am thinking is that, the AI generated numbers or tried to find numbers "a", "b" and "c" to check if aⁿ + bⁿ = cⁿ Can not we do it by code?

Sure, go on and try it ;)

Re: Formalizing Fermat's Last Theorem

#34

Post by drivebyhooting » Fri, Sep 04, 2026, 7:22 PM UTC

LLMs are pretty good at slogging through. When will they come up with brilliant breakthroughs like Andrew Wiles?

Re: Formalizing Fermat's Last Theorem

#35

Post by kbelder » Fri, Sep 04, 2026, 7:23 PM UTC

anony-123 wrote: post #29

So, what I am thinking is that, the AI generated numbers or tried to find numbers "a", "b" and "c" to check if aⁿ + bⁿ = cⁿ Can not we do it by code?

Just loop through all values of a, b, c, and n?

Re: Formalizing Fermat's Last Theorem

#36

Post by bjourne » Fri, Sep 04, 2026, 7:23 PM UTC

jrflo wrote: post #17

Holy shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?

Yep. There may be only 25-50 people alive today in the whole world who can credibly claim to understand Wiles' proof. Now we add an LLM to that list. Absolutely mind-blowing stuff.

Re: Formalizing Fermat's Last Theorem

#37

Post by voxl » Fri, Sep 04, 2026, 7:23 PM UTC

rao-v wrote: post #6

An aside on Lean and it's massive library of results: As someone who's put non trivial effort into slowly learning geometric algebra, lie theory and other slightly advanced math topics, I have to say my brain cannot read Lean. It feels so unprocessable. I've tried the various intros to Lean multiple times (even before Lean 4 came out) and something about the way Lean proofs are written does not align with how I think…

Hearing someone say "the future of proofs is Lean" is a bit like hearing someone say "the future of programming is Rust." Sorry to disappoint, or happy to inform, there are hundreds of programming languages actively being used, and Rust is not even the most used language. To think that proof assistants, fancy programming languages, would be any different is suspiciously motivated.

Re: Formalizing Fermat's Last Theorem

#38

Post by estetlinus » Fri, Sep 04, 2026, 7:24 PM UTC

I can recommend the book telling the full story behind Fermats Last Theorem (by Simon Singh). It’s quite fascinating, and paved with really, _really_ weird characters each chipping in on the final solution.

Re: Formalizing Fermat's Last Theorem

#39

Post by KaiserPister » Fri, Sep 04, 2026, 7:25 PM UTC

13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?

Re: Formalizing Fermat's Last Theorem

#40

Post by kzrdude » Fri, Sep 04, 2026, 7:25 PM UTC

The part about prove2.me was interesting. That means that a co-working tool was instrumental in the project, and I think AI companies will take note of this. Is this proof specific or will we need to give agents access to JIRA or similar tools to solve large projects in the future?