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-theoretic intuition and strict formal type theory. This ga…