AI startup Resolution (formerly Sequent) reports that it has automatically formalized Hironaka’s resolution of singularities in the Lean proof assistant. The formalization produced a substantial Lean library that the team is using to investigate connections between loss landscape geometry and generalization in statistical learning theory.
How the formalization was carried out
Resolution describes the work as an agent-orchestrated pipeline. A researcher first worked with agents to produce two plans: a high-level, human-interpretable plan and a detailed, 112-page plan broken into atomic steps that closely followed the existing literature. An orchestrator agent was then tasked with executing the detailed plan, spawning agents responsible for pen-and-paper style mathematical reasoning, writing Lean code, and supporting functions such as progress checking.
According to the team, the execution phase required little additional scaffolding beyond the initial plans and agent skills distilled from earlier internal autoformalization efforts. This indicates that a well-structured multi-agent workflow can autonomously carry out complex formalization tasks.
Resources used and outputs
The project took about a week. Resolution reports using on the order of 100 billion input tokens (about 90% cache reads) and roughly 300 million output tokens, with an estimated token spend of $135,000. The formalization produced approximately 600,000 lines of Lean code.
Benefits for follow-up research
Resolution says the formalized library has already accelerated related research directions. Formalizing resolution of singularities enables more automation of parts of singular learning theory, for example helping to better understand sampling behavior. That improved theoretical understanding feeds into the team’s efforts to shape how models learn, a capability they refer to as “patterning.”
Why this matters for AI safety and alignment
Although advanced pure mathematics may appear distant from applied AI development, this example shows how automated formalization can bridge that gap. AI-driven formalization lowers the time and cost barriers that previously made large-scale formal work impractical for most research teams, allowing such work to be integrated into a startup’s research roadmap.
Resolution frames these developments as steps toward an "industrialization of mathematics," which they expect will enable a more rigorous science of research automation. In turn, better automated mathematical tools and libraries could support more principled approaches to understanding and steering model behavior, with implications for AI safety and alignment.
Conclusion
Resolution’s work demonstrates that modern LLM-based agent systems can be used to produce substantive formal mathematical artifacts at scale. The reported token usage, timeline, and 600,000 lines of Lean suggest the approach is both technically feasible and economically significant. Continued progress in automated formalization could open new opportunities for research automation relevant to AI safety.
