Paper recorded by Signals 4 on 2026-10-23 in cs.AI. Abstract reproduced from arXiv; link to the original below.
Published 2026-10-23 on arXiv · recorded by Signals 4 on 2026-10-26
Category: cs.AI · 人工智能 · first seen 2026-10-26
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 pr