Comment by emil-lp

No, the correctness isn't for the "inside the Lean proofs", but for the translation of "human language math" and its formal Lean variant.