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…