Lea: An Agent Backbone for Mathematician-Controlled Formalization in Lean

Shaswat Patel, Daniel Aarao Reis Arturi, Kevin Gomez +6

Agentic systems now formalize research-level mathematics in Lean, but they are built for autonomy: the mathematician states a target and inspects a result. The alternative, a gener…