Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy +3

Theorem-proving benchmarks evaluate proof search against fixed formal statements, but natural-language-to-Lean formalization must generate the formal statement itself. In this sett…