2 papers
cs.AI2026
Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy +3
Lean verifies that a generated declaration is well typed, but not that it expresses the statement a user intended. We study two questions for autoformalization without canonical Le…
cs.SE2026
Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis
Ke Zhang, Patricio Gallardo, Maziar Raissi +1
Automatic translation of natural language mathematics into faithful Lean 4 code is hindered by the fundamental dissonance between informal set-theoretic intuition and strict formal…