Cogentic coordinates provers and adversarial reviewers to tackle open mathematical problem

An unsuccessful mathematical proof can still contain a useful lemma. Cogentic gives those fragments a separate verification process and preserves the ones that survive, so later attempts can build on them instead of starting over. In the Cogentic paper, Google Research authors describe a multi-agent system built around that accumulation of checked progress.
Using Gemini as the base model, the authors report new results on five open problems in online learning, auction theory and mechanism design. They say the problems fall within their own research expertise. Each result received independent verification by domain experts and has a companion paper.

Separate proof construction from checking

An orchestrator assigns independent provers to different research directions. A direction might mean establishing a particular bound, finding a counterexample or repairing an earlier argument. The orchestrator manages work and context without performing mathematical derivations itself. Literature reviewers retrieve definitions and existing theorems, including targeted searches when a proof attempt gets stuck.
After a prover finishes, one verifier checks its draft individually. Another reads all drafts from that round together to identify shared weaknesses and compare their arguments. A draft is accepted only after both verification passes. The verifiers begin by treating steps as unjustified and citations as incorrect until checked.
Cogentic also records why attempts failed. Summarizers prepare different briefings for subsequent provers, drawing on the attempt history and verified results. A process advisor examines recurring mistakes and adjusts instructions. The paper explicitly prohibits both that advisor and the orchestrator from recommending mathematical techniques or expressing opinions about the likely answer.

Preserve useful lemmas from rejected proofs

Rejecting a complete argument does not automatically discard everything inside it. An auditor extracts intermediate lemmas that verifiers confirmed, rewrites them as self-contained statements and submits them for another check in isolation. Surviving lemmas enter a shared ledger for later rounds. Verified counterexamples also record excluded bounds, helping agents avoid revisiting established dead ends.
Once a run finishes, a comparator selects the strongest verified proof. A writer expands it into a manuscript, followed by an audit against the accepted argument to check that the exposition introduced no errors. Cogentic produces natural-language mathematical proofs for domain experts to check. This differs from Lean, Coq or Isabelle workflows that provide machine-checked guarantees.
One reported result concerns selling independent items to a single buyer with additive valuations. The authors improve the approximation factor comparing optimal revenue with the better of separate-item pricing and selling one bundle from 5.2 to 3.52. Those assumptions matter: this is a theorem about a specified economic model, not a measured revenue increase for a business. The paper says the optimal constant remains unknown.

Read the results within their evaluation scope

The authors say each run starts from the problem statement without human mathematical intervention, with experts verifying the proof afterward. They describe inference budgets on the order of 100 Gemini calls for most reported problems and 1,000 for the hardest. Those figures are approximate call counts, not a quoted financial cost or a runtime guarantee.
The five selected results show what this workflow produced in areas the authors could evaluate themselves. They do not establish a success rate over arbitrary open problems. For anyone assessing the system, the companion proofs and their assumptions are central: the harness's own acceptance decision remains distinct from the experts' subsequent mathematical verification.