Resolution autoformalizes resolution of singularities using AI agents

AI startup Resolution has autoformalized the resolution of singularities in statistical learning theory, producing 600,000 lines of Lean code. The work, costing an estimated $135,000 in token spend, demonstrates how AI can automate complex mathematical research, potentially enabling a rigorous science of research automation.