amazing, it's a huge achievement. can someone clarify, where the writeup says "The finished proof was checked by Lean; it uses just Lean’s three standard axioms" what does this mean? Aren't there a large set of standard axioms that are also necessary? (i.e. ZFC+)? if not, since it's only three axioms, can someone say what they were?

Very impressive! I was a child when that proof came out. I've read a book about it a few years later and used it on my final high school exam. I remember some friends trying to understand parts of it at univ. It was all like black magic to me and the vibe was "maybe a few people in the world understand it".

I hope soon enough we will have one of the big ones proved by AI!

https://github.com/anthropics/fermats-last-theorem/blob/main...

  status: "self-assessed"

13 million lines of Lean, where the Lean and Nanoda kernels missed the Collatz hack.

Fable, please translate to HOL-light. Make no mistakes. You are doing great!

that's crazy

Holy shit. The proof of FLT is a giant detour through several different areas of mathematics, so formalizing it is a lot of work.

An interesting next target would be formalizing the classification of finite simple groups. The original proof scattered over thousands of pages of journal articles, plus Aschbacher and Smith's 1300 page 2 volume monograph. It's so long it's hard to know if there are any gaps. Researchers have been working on a streamlined new proof, but it's already many volumes long.

I call bullshit on 13 million lines makes no sense

>The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway).

What is even the point? Have claude do it.

I'm not trying to be snarky here. I'm being serious. What is the point? This is an important question that needs to be answered. If something is definitively better, why not have that something take over?

I know people talk about the importance of human endeavor or the "joy" of doing something. But I don't care for those answers because it's weak. The question is deeper than this. AI is better than us, what is the logical point other than attempting to monopolize human effort even though it is inferior.

[flagged]

[dead]

I won't be impressed until it identifies the proof he wrote in the margin. /s