1. Reusability and library‑ready formalizations
Commenters stress the desire to extract usable lemmas and foundations from the proof rather than treating it as a one‑off result.
- black_knight: “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.”
- Jhsto: “…finding reusable parts that can be built into libraries (that's lemmas in Lean 4 sense).”
- black_knight: “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.”
2. Admiration for the achievement
Many participants simply celebrate the result as impressive work.
- abhv: “This is a very impressive result. Bravo to that team.”
3. Concerns about the trustworthiness of the proof system
A recurring theme is skepticism about whether the Lean kernel and its toolchain can be guaranteed error‑free.
- kmoser: “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: “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.”