Import AI 478: Math for alignment; ProgramBench; and Mirendil shows what RSI means
AI agents spent $135k to autoformalize advanced math, enabling a new rigorous science of alignment research
“We expect the coming industrialization of mathematics to make possible a new, rigorous science of research automation”— Jack Clark
AI safety startup Resolution used orchestrated AI agents to autoformalize Hironaka's Resolution of Singularities in about a week, spending ~$135k in token costs and producing 600k lines of Lean proof code. This advances their singular learning theory work and demonstrates that AI is making previously cost-prohibitive mathematical research accessible to startups. Separately, Claude Opus 5.5 jumped from 0% to 18.5% on ProgramBench within months of its release, illustrating rapid benchmark progression in agentic coding.