Comment by gowld

18 hours ago

What else could a theorem prove if not its own statement? (barring bugs in Lean, which have been detected and exploited)

The theorem might not be encoded correctly, as happened with the Riemann hypothesis thanks to how numbers are encoded.