Cogentic: Multi-Agent Orchestration for Automated Proof Discovery

Yang Cai; Vineet Gupta; Yanchen Jiang; Christopher Liaw; Aranyak Mehta; Grigoris Velegkas; Di Wang

cs.AISep 30, 2026

Cogentic: Multi-Agent Orchestration for Automated Proof Discovery

Authors: Yang Cai, Vineet Gupta, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, Di Wang

Organizations: Google Research · Yale University · Google DeepMind

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 .

Figures & tables

Figure 1: One round of Cogentic. The orchestrator decides how many provers to run and which direction each attends to, an advisor writes each prover an individual briefing, the provers draft candidate proofs in parallel, and every draft is verified both on its own and alongside the others from the round. What a round establishes is written down for subsequent rounds: the attempts and why they failed, the verified ledger of intermediate results, and the standing instructions maintained by the process advisor. Literature reviewers supply background at the start and can be dispatched again mid-run when attempts stall at the same step. Rounds continue until a draft clears verification after which the accepted proof is consolidated, expanded into a formal manuscript, and audited.

Problem	Area	Prior State of the Art	Cogentic Result
Online inverse linear optimization / low-regret cutting planes	Online learning & optimization	$O(d\ln T)$ efficiently; $O(d)$ only by an improper rule costing $T^{\Theta(d)}$ per round	First efficient and first proper $O(d)$ bound, uniform in $T$ , at $O(d^{2})$ per round ( Cai et al., 2026a )
Two-sided Bulow–Klemperer competition complexity	Auction theory & market design	$O(1)$ agents suffice, but recruiting on both sides and with a constant of at least $20{,}000$ per side	$+2$ agents on the smaller side alone suffice ( $\operatorname{STR}(m,n+2)\geq\operatorname{OPT}(m,n)$ ), and $+1$ does not suffice for any DSIC, IR, weakly budget-balanced mechanism ( Cai et al., 2026e )
Anytime regret with $n$ experts	Online learning	Anytime $\sqrt{t\ln n}$ vs. fixed-horizon $\sqrt{t\ln n/2}$ ; the factor $\sqrt{2}$ open	Anytime regret $\bigl(1+O(\sqrt{\ln\ln n/\ln n})\bigr)\sqrt{t\ln n/2}$ : no leading-order price for anytime validity ( Cai et al., 2026b )
Simple vs. optimal revenue maximization, single additive buyer	Mechanism design	$5.2\cdot\max(\operatorname{SRev},\operatorname{BRev})\geq\operatorname{OPT}$ ( Ma and Simchi-Levi, 2021 )	$3.52\cdot\max(\operatorname{SRev},\operatorname{BRev})\geq\operatorname{OPT}$ ( Cai et al., 2026d )
Price of anarchy for autobidding auctions	Auction theory & autobidding	$1.8$ PoA for $2$ bidders; general $n$ -bidder tight mechanism open	Optimal $1.5$ PoA for $2$ bidders (anonymous, monotone mechanisms); $2-\frac{1}{4n+1}$ for $n$ bidders ( Cai et al., 2026c )

Table 1: Open problems resolved or improved by Cogentic. Each result is developed in full in a companion paper; see https://sites.google.com/view/cogentic for updates.

Explore similar work

ProofCouncil: An LLM Agent for Solving Open Mathematical Problems
Jul 10, 2026Johannes Schmitt, Tim Gehrunger, Jasper Dekoninck +4Open Problems Large Language Model Agents
ETH Zurich · Aarhus University · Independent Researcher +1
RMA: Context-Orchestrated Research Math Agents
May 20, 2026Zelin Zhao, Bo Yuan, Yuchen Zhu +2Research-Level Mathematics Theorem Proving
Georgia Institute of Technology
Advancing Mathematics Research with AI-Driven Formal Proof Search
May 21, 2026George Tsoukalas, Anton Kovsharov, Sergey Shirobokov +18Theorem Proving Open Problems
1Google DeepMind1 · 2Aarhus University · 3Google

Jul 10, 2026, cs.AIJ/K move · Enter open · S save

ProofCouncil: An LLM Agent for Solving Open Mathematical Problems

Johannes Schmitt, Tim Gehrunger, Jasper Dekoninck, Gergely Bérczi+3

ETH Zurich · Aarhus University · Independent Researcher+1

Open Problems Large Language Model Agents

Open paper AskPDF arXiv

Large language models (LLMs) have shown increasing promise in solving open problems in mathematics. However, their performance can be further improved through agentic workflows tailored to real-world mathematical practice. To this end, we introduce ProofCouncil, a mathematical agent that is designed to tackle open problems using an author-critic architecture. ProofCouncil served as a submission to the second batch of FirstProof, a challenge consisting of 10 real-world mathematical problems that agents must solve autonomously. Its submissions for 6 of the 10 problems were judged by the referees to be correct up to at most minor revisions, showing the best performance among participating teams. We also evaluate ProofCouncil on 30 open problems collected from mathematical researchers. Among the 21 solutions that received human feedback, 5 were judged completely correct, 2 more were judged promising pending final verification, and a further 8 contained useful partial progress. In this short paper, we describe the development of ProofCouncil and the agent-building library used to create it, which we release as open source to the community.

Abstract

Explore similar work

ProofCouncil: An LLM Agent for Solving Open Mathematical Problems

RMA: Context-Orchestrated Research Math Agents

Advancing Mathematics Research with AI-Driven Formal Proof Search