Jagged AI and verification
Models spike on benchmarks and crater on the next problem. Math is where verification loops work — and where the gap between MCTS credit assignment and LLM RL shows up sharpest.
AI math capability is jagged. A model clears a competition benchmark and fails an adjacent problem that looks identical to a human. That jaggedness is not noise — it is structural. Domains with cheap verifiers — code that runs, proofs that check, equations with closed-form answers — advance faster than domains where success is subjective. Karpathy’s coding-agent story and the math-verification loop are the same pattern seen from two angles.
The canonical mechanism: a verification loop — generate, check, iterate — can grind out progress even when raw generation is uneven. Nick Turley at OpenAI said code has “escape velocity” because it is testable and RL-friendly. The same property makes automated AI research bump against an LLM capability boundary: models can execute steps but struggle to choose the right research question — an open question on the wiki.
Nick Bostrom, on Odd Lots in August, used chess. Computers exceeded humans; people still play. “Maybe mathematics will ultimately become more like a hobby pursuit.” A philosophical parallel. Not a benchmark. Dwarkesh Patel, on the same show, said IMO gold “did not have transformative effects on the world” — the things you cannot make benchmarks for are also the things, in the current paradigm, you cannot easily train for.
The lab ran the inner loop
On August 28 Anthropic published what it called automated alignment researchers. Claude hill-climbed ten alignment failures that already have benches — literature, then method and data, then about thirty minutes of training on one H200, then a test on public benches — and closed a substantial share of the measured safety gap. The ten types were named by humans: sycophancy, jailbreaks, prompt injection, power seeking, deception, hallucination, social bias, privacy violation, reward hacking, concealing uncertainty. Anthropic’s own limit is the point: failures without a benchmark are out of scope.
That is Jang’s verifiable inner loop, dated, from a frontier lab. It is not direction-selection. The wiki’s question — can the model choose the next experiment, or the definition, when the checker is weak — stays open. Human-written initial directions did not improve the run. There is no documented dead-end escape, and no unprompted “what should we even be measuring.” Grant Sanderson’s June line still sits next to it: theorem-proving is the trainable spike; the premium tier is the conjecture generator. Karpathy’s March version is the same split — ideas can come from the loop; enactment stays queued by humans.
Two counts disagree and both stay. The blog says just over 2,000 training examples; the long-form report says about 2,400. Prefer the long-form if one number must be used. The harness was announced as open source. No GitHub URL was on the fetched page. Do not invent one.
September 4 is another dated inner loop, not a close of the question. Anthropic’s science blog said Claude autoformalized Fermat’s Last Theorem in Lean: eleven days, thirteen million lines, roughly 29,500 to 30,300 intermediate theorems. The path is Darmon–Diamond–Taylor / Wiles — a known proof. Tianyi Peng steered at a high level. The scaffolding was Prove2Me, a DAG that keeps theorem statements and proofs in separate files. Anthropic contrasts the artifact with recent Riemann-adjacent novel work. That contrast is the point. Lean checked a flood of formalization. It did not pick a new definition. Sanderson’s conjecture-generator tier is still empty. The wiki’s question stays open.
September 5 and 6 added two more dated misses on the same question. Meta’s AIRA₃ swarm claimed gold on a privately graded Kaggle, a 27 percent production-GPU-kernel latency cut, and gold-level Akkadian translation by changing only the task specification. That is a human-named graded task — Jang’s verifiable inner loop — not a documented dead-end escape or an unprompted “what should we even be measuring.” OpenAI’s September 6 research-acceleration post claimed an automated research intern for well-defined tasks under human direction, 3.1 agent-workdays per human workday, and “strong progress” toward an automated researcher by March 2028. People still set priorities. Full aligned RSI, the same post said, is unsolved. Do not close the question as yes.
September 8 piled more Lean checks onto the same fence, and still did not pick a definition. Tristan Buckmaster and Levent Alpöge posted Lean-checked finite-time blowups with smooth forcing for incompressible porous media, Boussinesq, and 3D Euler. The program idea, they said, is Córdoba and Martínez-Zoroa’s; the LLMs — Claude, Codex, especially GPT-5.6 Sol — pushed it to smooth forcing. Astra was “only used for writeups and auditing.” That is not Fermat. It is not Clay’s unforced Navier–Stokes prize. They believe they also have hypo-dissipative Navier–Stokes and are not releasing it: Lean unfinished. The same morning Anima Anandkumar’s group reported a PINN-found unforced 3D Euler singularity candidate on free space. Tao, via her cite, said a rigorous stability demonstration is still lacking. Candidate, not a finished Lean theorem.
That afternoon OpenAI published an issuer claim of its own. A forced Navier–Stokes existence-and-smoothness writeup, framed as Clay/Fefferman C and D: fluid at rest, a smooth external force, energy finite, a singularity in finite time. The lab says it does not intend to claim the Millennium Prize. The model is internal, “significantly more capable than GPT-6 Astra,” trained since about August 28. Process metrics on the same page: about 10,000 concurrent agents, about 88 hours to a Saturday resolution, Lean formalization about 17 hours via Astra, about 2.7 million messages. A companion unforced-Euler writeup is filed as an “easier” related problem — about 100 agents, about 50 hours. OpenAI congratulated Buckmaster and Alpöge for forced-Euler priority and said the proofs differ. Issuer Lean plus a public repo is not independent math review. Forced C/D is not unforced A/B. Do not write “Navier–Stokes solved.” Do not close the question as yes.
MCTS versus token RL
Monte Carlo Tree Search assigns credit per move with a clear tree structure. LLM reinforcement learning assigns credit across long token sequences where the reward signal is sparse and delayed. The mismatch makes MCTS-per-move targets inefficient to imitate with standard LLM RL. RL information inefficiency is the broader label: you need many samples to move a capability that MCTS would localize in a branch.
By mid-2026 the “are we at AGI?” question has fractured. Demis Hassabis points at 2029 and deriving relativity. Others say generality arrived with GPT-2 and few-shot learning. Benchmark saturation — models hitting ceiling scores while real-world failure modes persist — sits in the same concept cluster. Jensen Huang, on September 6, planted another flag: “AGI has arrived,” citing GPT-6 Astra trained on about 100,000-plus NVIDIA Grace Blackwell NVLink72 systems, plus 400,000 GPUs coming online next. Nvidia CEO rhetoric, not a lab capability paper. The wiki keeps the label contested. Definitions disagree; the jagged edge remains.