Agentic LLM System Autoformalizes Research Math into Lean 4
A new agentic autoformalization system uses general-purpose coding LLMs to translate novel research mathematics into Lean 4, extending libraries on the fly and checking proofs mechanically. It succeeded on a random sample of 32 Putnam problems and formalized main theorems from five STOC papers, two of which required only Lean's kernel axioms.