SemantEq: Faithful Bidirectional Equivalence of Formal Statements.

arXiv:2610.32919v1 Announce Type: new Abstract: Statement autoformalization translates mathematics from natural language into a proof assistant such as Lean 4, and models now do it at scale. As provers get stronger, the burden of correctness shifts from the pr