Fermat's Last Theorem in Lean 4 (github.com)

82 pointsby aaraujo00210 hours ago15 comments

black_knight 7 hours ago

I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the existing Lean libraries.

My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof! (Repost of a earlier comment, but I feel it fits better here)

Jhsto 7 hours ago

My anecdotal experience is that while LLMs are quite good at closing theorems given an LSP to inspect the proof-tree, they suffer from similar kind of problems with proofs as they do with bigger codebases in any language -- finding reusable parts that can be built into libraries (that's lemmas in Lean 4 sense). However, Buzzard has many times said that he wouldn't care how big the proof is and how ugly it would be, as long as there would be a proof.

black_knight 7 hours ago

Kevin might not care, but I care more about building the foundation for future proofs and human understanding than I do about this particular result.

refulgentis 7 hours ago

Is any piece you've seen in good enough shape to be in a Lean library?

kmoser 6 hours ago

Serious question: how do you prove that the Lean interpreter itself (not to mention the toolchain built around it) is error-free? Isn't this turtles all the way down to some degree?

ezwoodland 6 hours ago

You can only do so in another framework that might itself have bugs.

Lean is called that because the hope is the part that has to be correct by inspection ("the kernel") is small or "lean".

The kernel does have bugs sometimes.

michael0church 4 hours ago

You can’t, so you keep the kernel small. The Lean tactics language is rich, so users can autogenerate proofs for the truly trivial bits, but the core language is checkable in dependent type theory.

Kernel bugs, like compiler bugs, exist. As of now, a prover is considered good if it has no known bugs that would thwart a mathematician working in good faith. It’s not considered responsible yet for being impervious to adverse users, but that may change in the age of Ai.

jibal 4 hours ago

You haven't thought that through. The regress obviously isn't infinite, and it bottoms out in things that are immediately true by inspection. And seriously, how likely is it that you have stumbled upon a fundamental problem with the whole notion of automated proof that no one in the field has thought of?

https://www.youtube.com/watch?v=RxV4PQcJ1fw ("The Proof in the Code: How Lean Is Quietly Rewriting Trust in Math")

RantyDave 5 hours ago

I love that “grind” is a keyword.

michael0church 4 hours ago

It’s a tactic.

laylomo2 3 hours ago

So is “simp”

abhv 7 hours ago

This is a very impressive result. Bravo to that team.

rawling 9 hours ago

Front-page discussion: https://news.ycombinator.com/item?id=49568506

ks2048 8 hours ago

Now we have what Fermat tried to write in the margin: aa2d8b34692b16c70f699536de0d8e75b9a3e9ef

DoctorOetker 10 hours ago

Mine is much shorter though...