ProofCouncil: An LLM Agent for Solving Open Mathematical Problems¶

🕒 Published (v1): 2026-07-10 14:46 UTC · Source: Arxiv · link

Why this paper was selected

ETH Zurich; Planner-Worker-Verifier agent for open math problems; strong group on reasoning + formal methods

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

TL;DR¶

ProofCouncil is an LLM agent that solves open mathematical research problems using an author-critic architecture augmented by an LLM council and a computer algebra system (CAS) compute node. It achieved the best performance among all teams in the second batch of the FirstProof challenge, solving 6 of 10 problems correctly (up to minor revisions). On 30 researcher-submitted open problems, it produced 5 complete correct solutions and meaningful partial progress in 8 more.

Problem¶

Existing LLM approaches to mathematics either operate as single-query systems or lack agentic workflows matched to real-world mathematical practice—iterative proof refinement, independent verification, and heterogeneous tool use. There is a gap between LLM capability and the multi-step, expert-critical process that open-problem research mathematics requires.

Method¶

ProofCouncil implements an author-critic loop over a fixed-horizon unrolled conditional DAG:

Author (GPT-5.5-Pro, xhigh effort): maintains answer.tex, research_notes.tex, and references.bib via code execution; optionally emits <council> and <compute_agent> XML tags to solicit auxiliary help.
Stateful Critic (GPT-5.5-Pro, xhigh): receives the full proof history and provides structured feedback; reset every $k=3$ rounds to reduce path dependence.
Fresh Critic: an independently initialized critic that must also accept the proof before it is returned, guarding against critic capture.
LLM Council: Gemini 3.1 Pro (high), Claude Opus 4.7 (max), and GPT-5.5-Pro (xhigh) answer author queries independently.
Compute Node: a Codex agent (GPT-5.5, xhigh) with access to SageMath, GAP, Singular, and Pari for CAS verification and counterexample search.

The system is built on an open-source library that represents agent workflows as conditional DAGs, supporting parallel independent nodes, bounded repeat blocks, conditional edges, and human-in-the-loop pauses.

Key Contributions¶

ProofCouncil agent: author-critic architecture with council and CAS compute augmentation for solving open mathematical problems.
Open-source conditional-DAG agent library: represents agentic workflows as directed acyclic graphs with conditional edges, parallel execution of independent nodes, and human-in-the-loop support.
FirstProof challenge result: 6/10 problems solved (up to minor revisions), best among all participating teams.
Open-problem evaluation: 5 complete solutions and 8 with meaningful partial progress out of 21 expert-reviewed attempts on 30 researcher-submitted problems.

Results¶

FirstProof (batch 2): 6/9 analyzed problems accepted (P1, P2, P3, P5, P7, P9); 1 partial (P10); 2 rejected (P4, P8); P6 excluded due to API timeout. Best performance among participating teams.
Single-query GPT-5.5-Pro baseline (also evaluated in the challenge): solved 4/9 at ~$12/problem vs. ProofCouncil's 6/9 at ~$350/problem.
Researcher-problem evaluation (21 responses out of 30 submitted): 5 complete solutions, 2 promising pending verification, 8 meaningful partial progress, 4 no progress, 2 misinterpreted.
Cost: ~$213/problem on researcher runs; ~$350/problem on FirstProof run (total $3,186 over 9 problems). Author accounted for 48.8% of spend ($1,555); critic 31.6% ($1,008); GPT-5.5-Pro council 11.3% ($361).
Council and compute node each appeared in >50% of rounds across runs.
Fresh critic was critical on P10: stateful critic accepted intermediate (incorrect) solutions 7 times; fresh critic rejected all of them.

Limitations¶

High cost: >$200 per problem; dominated by repeated frontier-model inference; no cost optimization was performed.
Problem misinterpretation: 2 outputs solved easier variants of the stated problem; the critic shares the author's reading, so internal feedback cannot catch shared misreadings.
Local minima: the agent frequently became stuck patching a single proof gap without broader strategy change; parallel author-critic threads would increase cost further.
Evaluation reliability: FirstProof grades are "up to minor revisions" rather than fully verified; researcher-problem results are from an adaptive development evaluation (prompts adjusted between runs), not a frozen configuration.
Human readability: proofs are dense and were noted by expert reviewers as not yet suitable for publication without significant expansion and exposition.
Execution errors: 3 of 30 researcher problems and 1 FirstProof problem (P6) produced no output due to runtime/API failures.

Relevance to Agentic AI / LLM Agents¶

ProofCouncil is a concrete instance of multi-agent collaboration applied to a domain with ground-truth verifiability (mathematical correctness), making it a high-signal testbed for agentic design choices such as stateful-vs.-fresh critics, heterogeneous model councils, and conditional DAG control flow. The dual-critic mechanism (stateful + fresh) and the separation between a reasoning loop and auxiliary specialist nodes (CAS, council) are architectural patterns directly transferable to other agentic systems requiring iterative drafting and independent verification. The conditional DAG library, released openly, provides infrastructure for researchers building structured multi-agent workflows beyond single-chain-of-thought approaches. The FirstProof benchmark itself is an emerging standard for evaluating agents on real open problems, situating this work at the frontier of agentic AI evaluation methodology.