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)
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.
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)
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.