Prépublication · 2026
SemantEq: Faithful Bidirectional Equivalence of Formal Statements
Xinrui Li, Pawan Sasanka Ammanamanchi et al. — Monde
Source : arXiv
Résumé
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 proof to the statement, that is, to whether the formal statement faithfully translates its source. Given a trusted reference formalization, the natural test is logical equivalence, and it proves too much. $P \leftrightarrow Q$ holds trivially for any two statements $P$ and $Q$ that the library proves, because a prover can prove each separately and pass through $P \leftrightarrow \mathrm{…