Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis
arXiv:2604.16538v1 Announce Type: cross Abstract: Automatic translation of natural language mathematics into faithful Lean 4 code is hindered by the fundamental dissonance between informal set-theoret