Agentic AI news, research notes, and industry analysis.
Tag
8 stories in this tag.
A new paper and blog post from Michael Noukhovitch identifies the "Matthew Effect" in RL training for LLMs: standard GRPO concentrates gains on problems a model can already mostly solve, while genuinely hard problems see minimal improvement. The fix — Never Give Up (NGU) — is an adaptive sampling strategy that keeps generating completions until it finds one that works, naturally redistributing compute toward the problems that need it.
Read more →Anthropic released a complete, machine-verified formalization of Fermat's Last Theorem in Lean 4. Claude worked for 11 days and produced 13 million lines of proof code—five times the size of Mathlib—checked independently by three separate verifiers. The interesting story is less "AI does math" and more how multi-agent coordination over a theorem dependency graph made it tractable.
Read more →Stephen Chung, Wenyu Du, and William Wesley's Station system — an open-world multi-agent environment where AI agents autonomously choose research directions without central coordination — produced novel results on five open mathematical problems, including new infinite families of finite-field Kakeya sets and improved kissing configurations in dimension 11.
Read more →Terry Tao and the Lean FRO launched Palomar on August 18 — a registry that runs submitted Lean proof repositories through a verification pipeline and publishes the exact formal statement, library dependencies, and reviewer comments. The project is a direct response to the surge in AI-generated Lean proofs, where the bottleneck has shifted from producing proofs to trusting them.
Read more →Ring-Zero scales pure reinforcement learning from verifiable task rewards — no human-labeled preference data — to one trillion parameters. Complex reasoning behaviors emerge spontaneously: self-verification, parallel reasoning, and something the authors call "context anxiety." The two-phase training dynamic (discovery then sharpening) appears to be a consistent pattern as these runs grow larger.
Read more →An internal OpenAI reasoning model disproved a conjecture in discrete geometry that had been open since 1946. It found a polynomial improvement to the best known lower bound for the planar unit distance problem — n^(1+δ) with δ = 0.014 — by importing tools from algebraic number theory that no human mathematician had previously applied to this problem. The proof was verified and endorsed by several leading mathematicians, including Fields Medalist Tim Gowers.
Read more →DeepMind's AI Co-Mathematician is a hierarchical multi-agent workbench for mathematics research. Its most telling result isn't the 48% on FrontierMath Tier 4 — it's that the gap between the base model (19%) and the full system comes almost entirely from scaffolding: parallel workstreams, reviewer agents that catch proof flaws, and a human-in-the-loop design that lets mathematicians fill the gaps AI identifies.
Read more →Sander Dieleman's post on flow maps frames diffusion model distillation as learning to compute the integral of the velocity field directly, rather than stepping along tangent directions. The reformulation unifies 20+ recent papers under three consistency constraints and explains why single-step sampling is achievable without sacrificing bijectivity.
Read more →