AlphaEvolve: pointing a model at problems that come with an objective scoring function
Google DeepMind's coding-agent-driven evolutionary search: Gemini Flash proposes candidates in volume and Gemini Pro in quality, automatic evaluators score them, and high scorers stay in the population as next-round context, i.e. evolutionary search with an LLM as the mutation operator; it applies only where an automatic evaluator exists, hence the math and agents filing. An evolved scheduling heuristic has run in production in Google data centres (Borg) for over a year, recovering 0.7% of Google's global compute (Google's compute, not all compute on earth), the card reading and the only result validated by long-running production. An evolved matmul kernel is 23% faster at specific sizes, and about 20% of 50+ open maths problems improved, including 4x4 complex matrix multiplication in 48 multiplications against Strassen's 1969 record of 49. Verification differs from the prover line: a Lean check is mathematical correctness, "23% faster" is an empirical reading on specific hardware. No public weights, Early Access is a waitlist, and the precondition is an evaluator you write yourself. Graded B (contested): a year of production behind the Borg result, nothing reproduced.
0.7%Google global compute recovered (production-verified)Contested · 2025-05
ProductionGoogle DeepMindSite AlphaEvolve: pointing a model at problems that come with an objective scoring functionDeepSeek-Prover-V2: making the Lean kernel, not the model, the judge of correctness
DeepSeek's formal theorem proving model: a 671B MoE base shared with DeepSeek-V3 and Lean 4 as target language, so formal alignment on a flagship base. The core move is recursive subgoal decomposition at cold start: one-shot proofs of competition statements succeed so rarely that RL has almost no positive samples, so DeepSeek-V3 splits a statement into subgoals, a 7B model proves each, and the composed proofs become training data, trading decomposability for data density; the RL reward is binary and comes from the Lean kernel. Vendor-reported: MiniF2F-test 88.9% at pass@8192, PutnamBench 49/658 (about 7.4%), own ProverBench 325 problems. Read them together: MiniF2F is near saturation at that budget while hard Putnam problems drop an order of magnitude, and ProverBench is self-built and self-run. The public repo (about 1304 stars) ships a ZIP of proofs you can run through Lean, putting verifiability a tier above closed models. Limits: pass@8192 means eight thousand-plus candidates per problem, not comparable with pass@1. Not commensurable with Kimina-Prover's 92.2%, so list both without ranking. Graded C (vendor-stated): nothing recomputed in a standard Lean 4 + mathlib environment.
88.9%MiniF2F-testVendor Claim · 2025-07
DeepSeek-Prover-V2: making the Lean kernel, not the model, the judge of correctnessKimina-Prover: reaching 92.2% on miniF2F with whole-proof RL and no search tree
The Lean 4 theorem proving line from Moonshot AI with Numina, deliberately contrarian: no prover feedback in training or inference, no Monte Carlo tree search, value function or process reward model (arXiv:2504.11354), so search is internalised into a single whole-proof generation, and a custom Formal Reasoning Pattern writes a natural-language draft before Lean code, recasting a sparse binary reward as a language problem. The base is Qwen2.5-72B with up to 32K context. Keep two generations apart: Preview (2025-04) reached 80.7% on miniF2F-test at pass@8192, the first public result above 80%; the 72B model (2025-07-10) reached 92.2% after adding TTRL search and error repair, the highest public reading then and the number on the card, while pass@1 under the same protocol is only 63.9%. Equal-budget pass@1/32/1024 of 63.9/84.0/87.7 leads the 671B DeepSeek-Prover-V2 (61.9/82.4/86.6) at all three budgets. Discounts: that table is Kimina's own and its DeepSeek rows are their reruns, the repo declares no licence, and miniF2F holds 244 problems now past 92%, so its power to separate frontier models is decaying. No third-party board exists here, so read the numbers as direction. Graded C (vendor-stated): nothing recomputed on a pinned commit.
92.2%miniF2F (after TTRL search)Vendor Claim · 2025-07
ResearchMoonshot AI (Numina & Kimi)SiteRepo Kimina-Prover: reaching 92.2% on miniF2F with whole-proof RL and no search tree