The scarce resource is the runtime

Epistemic status: A reading note on AI-for-math systems work in September 2026, centered on Anthropic's machine-checked formalization of Fermat's Last Theorem and the Prove2Me multi-agent ablation. Di