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.<p>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)
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?
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.
This is a very impressive result. Bravo to that team.
Front-page discussion: <a href="https://news.ycombinator.com/item?id=49568506">https://news.ycombinator.com/item?id=49568506</a>
Now we have what Fermat tried to write in the margin: aa2d8b34692b16c70f699536de0d8e75b9a3e9ef
Mine is much shorter though...