Cogentic: Multi-Agent Orchestration for Automated Proof Discovery
Yang Cai, Vineet Gupta, Aranyak Mehta, Di Wang and colleagues at Google Research present Cogentic, a multi-agent harness built on Gemini that works on open research problems in theoretical computer science and produces natural-language proofs that domain experts then verify.
Ask this paper
Research-group structure. An orchestrator assigns prover slots across proof directions, literature reviewers fetch definitions and theorems, parallel provers draft proofs, and adversarial verifiers start from the assumption that each draft is wrong.
Verified ledger. Lemmas that survive verification are promoted into a persistent ledger, and a record of failed attempts with verifier critiques feeds later briefings, so progress carries across rounds.
Results. Starting from problem statements with no expert hints, Cogentic produced new results on five open problems in online learning, auction theory and mechanism design, including the first efficient proper O(d) regret bound for online inverse linear optimization and a proof that two extra traders on the smaller side suffice in two-sided Bulow-Klemperer competition.
Low budget. Most problems took on the order of 100 Gemini calls and the hardest about 1,000, far below the inference scale of recent headline math results.
Open issue. The authors note the system produces candidate results faster than experts can read them, and point to Lean formalization as one way to close that gap.
Abstract
We present Cogentic, a multi-agent harness for automated proof discovery on open research problems. While frontier language models can generate strong mathematical ideas in a single shot, single-shot generation is often insufficient for open problems that require exploring multiple competing conjectures, overcoming subtle technical obstructions, and retaining intermediate progress over a long horizon. Cogentic addresses these challenges through an iterative prove--verify loop in which an orchestrator allocates a population of independent provers across distinct proof directions, subjects their output to adversarial verification by several specialized components, and promotes confirmed intermediate results into a persistent verified ledger that later rounds build on. The harness is designed to be able to solve research-level math and theoretical computer science problems. Using Gemini as the base model, Cogentic produced novel results on five open problems across online learning, auction theory, and mechanism design. Each result was independently verified by domain experts and is developed in full in companion papers. We list these results, and new ones as they are verified, at https://sites.google.com/view/cogentic .