alt Hacker NewsI'm not an expert at it myself, but my understanding is there are numerous ways to "cheat" in a Lean proof (via `sorry` and similar). They're taking responsibility for fully verifying that none of these cheats were used (and that the theorem statements themselves were all correctly formalized.)
Even beyond cheating with sorries or kernel bugs, the lean encoded theorems (or specifications) must be checked by humans to see if they truly mirror the real theorem authentically.