When autoformalization translates math to formal proofs, checking logical equivalence isn't enough—SemantEq instead verifies that statements transform into each other only through semantically meaningful steps, achieving 100% precision on detecting non-equivalent pairs while improving recall fr...
This paper introduces SemantEq, a method to verify whether formal mathematical statements in proof assistants like Lean 4 faithfully translate their natural language sources. Rather than checking logical equivalence (which is too permissive), SemantEq requires statements to transform into each other only through specific allowed steps like logical rearrangement and library equations.