Comment by hn_throwaway_99

Lean is a theorem prover. If it "compiles", and the proposition as coded in Lean is equivalent to what the theorem proposes in natural language, the theorem is correct. https://en.wikipedia.org/wiki/Lean_(proof_assistant)