Cogentic orchestrates multiple agents to discover new mathematical proofs
Cogentic: Multi-Agent Orchestration for Automated Proof Discovery
Artificial IntelligenceComputer Science and Game Theory
Summary
Mathematical problems often need many ideas and long reasoning steps that simple AI tries only once can’t handle. The authors created Cogentic, a system that uses many AI agents working together to try different proof ideas, check each other’s work, and keep track of important progress. This back-and-forth process helps tackle really hard math and computer science problems. Using this system, the authors found new solutions to five open problems in fields like online learning and auction design, verified by experts.
What this means in practice
- •For algorithm designers: Automate exploring multiple proof strategies for complex mathematical problems to accelerate innovation in algorithm analysis.
- •For automated reasoning engineers: Develop software tools that coordinate multiple AI provers to improve success rates in formal verification tasks.
Authors
Yang Cai, Vineet Gupta, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, Di Wang
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 .