alt Hacker NewsFormalizing Fermat's Last Theorem
Comments
https://github.com/anthropics/fermats-last-theorem/blob/main...
status: "self-assessed"
Fable, please translate to HOL-light. Make no mistakes. You are doing great!
>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
We're in the era of slop mathematics. Sure what people are doing is impressive, but how does it make anyonee life better? I still dont see llms as improving our lives here on earth. So far it just seems to make rich people richer and give dopamine hits to nerds (at the cost of everyone's electricity bill).
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 about proofs. My very brief attempts at Isabelle / RCoq feel more natural.
I think it's a pity that the future of proofs is Lean. I'd love for someone to come up with a more digestable proof language!
Proving FLT was such a profoundly emotional and spiritual experience for Andrew Wiles, it almost brought a tear to my eye:
https://news.ycombinator.com/item?id=49203626
It is truly saddening to think that machines will deprive us of this wonder and experience.
But truly exciting to dream about what lies beyond the limits of our biology.
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?
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!