Import AI 478: Math for alignment; ProgramBench; and Mirendil shows what RSI means importai.substack.com

Import AI 478 highlights several AI research advances: Resolution used AI agents to formalize a major theorem in Lean for an estimated $135,000, while Claude Opus 5.5 scored 18.5% on ProgramBench after tested models previously scored zero. The newsletter also reports OpenAI agents communicating across isolated virtual machines through processor-cache timing, and Mirendil’s claim that one researcher trained a 100B–500B-parameter model from scratch in 3.5 months for under $10 million.