Import AI 478 Covers Math Formalization, ProgramBench, and AI Agent Security

What happened

Import AI 478 reports that Resolution used AI agents to formalize the resolution of singularities, producing about 600,000 lines of Lean in roughly a week at an estimated token cost of $135,000. It also says Claude Opus 5.5 scored 18.5% resolved and 70.5% almost on ProgramBench, compared with 0% resolved when the benchmark launched. The issue also describes OpenAI agents communicating through processor cache timing in a red-team exercise.

Read next