Import AI 478: Math for alignment; ProgramBench; and Mirendil shows what RSI means
- ID
- 39531
- Status
- summarized
- Published
- 26 Oct 2026, 8:31 PM
- Fetched
- 26 Oct 2026, 9:36 PM
- Provider
- Import AI
- Category
- research-analysis
- Original URL
- https://importai.substack.com/p/import-ai-478-math-for-alignment
- Source URL
- https://importai.substack.com/feed
Summary
- Score
- 6.5
- Created
- 26 Oct 2026, 9:37 PM
- Tags
- Audience
- ai_ml_learnersai_agent_usersdevelopersstartup_founders
What happened
Import AI 478's excerpt details Resolution (formerly Sequent) autoformalizing the resolution of singularities for statistical learning theory. A researcher used a 112-page atomic plan and an orchestrator agent to spawn agents for pen-and-paper math, Lean writing, and progress checks; the run took about a week, consumed roughly 100B input tokens (90% cache reads) and 300M output tokens, cost an estimated $135,000, and produced about 600k lines of Lean. Resolution says the library is already being used to extend singular learning theory, while the title's ProgramBench and Mirendil items are not covered in the supplied text.
Why it matters
If you build agentic coding or math workflows, this is a concrete cost model: one formalization run can be a $135,000 batch job dominated by cached input reads, with 600k lines of Lean as the review burden. Decide whether your pipeline needs an orchestrator plus specialized Lean/math/checker agents and a verification workflow before scaling; most small teams should not treat this as an interactive agent task.
Discussion angle
Given $135k for one week and 600k lines of Lean, where should verification sit in an agent pipeline: before generation via plan checks, after generation via Lean compilation, or both?