Cogentic: Multi-Agent Orchestration for Automated Proof Discovery
Yang Cai, Vineet Gupta, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, Di Wang
cs.AI, cs.GT
2026-10-01
Cogentic pairs parallel Gemini provers with adversarial verifiers and a verified-lemma ledger; it resolved five open math problems, most within O(100) calls, each expert-verified.
Frontier LLMs produce solid mathematical ideas in a single shot. Open research problems are a different beast: they involve betting on several competing conjectures at once, working around subtle technical obstructions, and carrying intermediate progress across a long horizon. One-shot generation fails at all three, and sampling more attempts just repeats at the same depth.
Existing automation routes each carry a precondition. Interactive theorem provers such as Lean give machine-checked guarantees once the problem is formalized. Program-search systems like FunSearch and AlphaEvolve found new constructions in extremal combinatorics, but they need a cheap, faithful, machine-computable score. Cogentic targets problems with no such score: open theory questions at STOC/FOCS level, proven in natural language and checked by domain experts.
The harness is organized like a research group: an orchestrator decides what gets worked on, provers draft in parallel, verifiers look for holes. One round runs plan, brief, draft, verify; whatever survives is written into ledgers that the next round starts from, and the loop ends when a draft clears all verification.
At termination a comparator picks the strongest verified proof, a formal writer expands it into a full manuscript, and a final audit checks the compiled document against the accepted proof. Most problems took O(100) Gemini calls end to end; the hardest took O(1000).
All five open problems were resolved, each verified independently by domain experts and written up in companion papers.
| Problem | Prior best | Cogentic result |
| Online inverse linear optimization regret | O(d ln T) efficiently; O(d) only via an improper rule costing T^Θ(d) tests | First efficient and first proper O(d) bound, uniform in T, O(d²) arithmetic per round, within O(√d) of optimal |
| Two-sided competition complexity | Both sides recruited, at least 20,000 per side | +2 agents on the smaller side suffice; +1 fails for any DSIC, IR, weakly budget-balanced mechanism |
| Anytime regret with n experts | √(t ln n), a factor 2 worse than fixed-horizon | (1+O(√(ln ln n/ln n)))·√(t ln n/2), no leading-order cost |
| Simple vs. optimal revenue, additive buyer | 5.2·max(SRev,BRev) ≥ OPT | 3.52·max(SRev,BRev) ≥ OPT |
| Autobidding auction PoA | 1.8 for 2 bidders; tight n-bidder mechanism open | 1.5 for 2 bidders, and tight; 2−1/(4n+1) for n bidders |
Two details carry the most signal. On the two-bidder PoA, the authors had conjectured the 1.5 bound for the proportional first-price auction but had no proof; Cogentic proved both the upper and the lower bound. On the n-bidder half, the authors had never studied the question and gave no hints; the mechanism and its analysis were invented by the system. After the inverse-optimization companion paper appeared, Sakaue obtained a tight O(√d) bound, though inefficiently; an efficient O(√d) algorithm remains open.
The five results are peer-reviewable mathematics, not toy benchmarks. For practitioners the transferable part is the recipe: the ledger plus the attempt record solves progress persistence in long-horizon work, dual adversarial verification pushes the trust question down to a granularity humans can actually check, and separating process control from mathematical content keeps the scheduler from contaminating exploration. Nothing in that skeleton is specific to mathematics; any long-horizon task with verifiable intermediate artifacts could adopt it.
The budget is modest by current test-time-compute standards: hundreds of Gemini calls for STOC/FOCS-level questions.
The authors are upfront: the problems sit inside their own areas of expertise, because that is the only way natural-language proofs could be checked; some companion papers include coauthors who were already working on those problems; humans wrote the exposition and in some cases pushed the arguments further than the harness did. The output still needs expert post-processing.
What the paper does not show: no comparison against other agentic math systems (the authors explicitly decline one), and no failure rate, so how many runs produced nothing is unknown and the visible record is all successes. Verification is human, not mechanical; the authors themselves worry the system can produce candidate results faster than they can be read, with the gap widening as compute grows, and that formalizing in Lean would settle correctness while human understanding lags. The n-bidder PoA upper bound additionally assumes bids are undominated.