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.