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

Agentic workflow tailored to open math problems; council-style multi-agent orchestration pattern

Ask a follow-up

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

TL;DR¶

ProofCouncil is an LLM-based mathematical agent built on an author-critic architecture that solved 6 of 10 open problems in the FirstProof challenge. Alongside the agent, the authors release an open-source library for constructing agentic systems as conditional directed acyclic graphs (DAGs), which serves as a general-purpose meta-harness substrate.

Problem¶

Frontier LLMs alone underperform on open research-level mathematical problems because they lack iterative self-correction, independent verification, and the ability to invoke specialized compute resources. Existing agentic workflows are not easily generalizable or composable, limiting reproducibility and reuse by the community.

Method¶

ProofCouncil uses an author-critic loop: a primary author agent (GPT-5.5-Pro, xhigh reasoning) iteratively writes and revises a LaTeX proof stored in answer.tex, research_notes.tex, and references.bib. A stateful critic (also GPT-5.5-Pro, xhigh) evaluates each revision and provides feedback, retaining conversation history across rounds but resetting every $k=3$ rounds to reduce path dependence. Proof acceptance requires both the stateful critic and a freshly initialized critic to accept, plus the author to emit a <ready> tag. Two optional auxiliary components can be invoked on demand via structured XML tags: an LLM council (Gemini 3.1 Pro, Claude Opus 4.7, GPT-5.5-Pro answering independently) and a compute node (a Codex agent with SageMath, GAP, Singular, Pari). The system runs until one of four stopping conditions: acceptance, round limit, cost budget, or 24-hour timeout.

The underlying agent-building library represents agentic systems as conditional DAGs where nodes are LLM calls, Python blocks, CLI compute agents, deterministic gates, or human-in-the-loop nodes. Edges carry conditions for conditional execution; loops are represented as bounded repeat blocks that unroll into finite DAGs. Nodes execute in topological order with parallel dispatch of independent branches.

Key Contributions¶

ProofCouncil agent implementing an author-critic architecture with stateful/fresh critic dual-gating and optional LLM council + CAS compute node.
Open-source agent-building library expressing agentic workflows as conditional DAGs with a visual node editor (Blender-inspired), parallel execution of independent branches, and human-in-the-loop support.
Best-in-class result on FirstProof Batch 2: 6/10 problems solved (up to minor revisions), versus 4/9 for the single-query GPT-5.5-Pro baseline.
Evaluation on 30 open research problems: 5 complete solutions, 2 promising, 8 partial-progress among 21 reviewed.

Results¶

FirstProof Batch 2: 6/10 problems (P1, P2, P3, P5, P7, P9) judged correct up to minor revisions; 1 partial (P10); 2 rejected (P4, P8); 1 excluded (P6, timeout). Best performance among participating teams.
Single-query GPT-5.5-Pro baseline: 4/9 problems solved at ~$12/problem vs. ProofCouncil's ~$350/problem.
Researcher-submitted problems (21 reviews received): 5 complete, 2 possibly complete, 8 meaningful partial, 4 no progress, 2 misinterpretation.
Total FirstProof run cost: $3,186 across 9 problems; author consumed 48.8% ($1,555), critic 31.6% ($1,008), GPT-5.5-Pro council 11.3% ($361).
Fresh critic was critical on P10: stateful critic accepted incorrect intermediate proofs 7 times; fresh critic rejected all 7.
Council and compute node each invoked in >50% of rounds in the open-question runs.

Limitations¶

Cost: ~$213–$350 per problem, driven by repeated frontier-model calls; no cost optimization was performed.
Problem misinterpretation: 2/21 reviewed outputs solved easier versions of the stated problem; misinterpretations propagate through the author-critic loop because both agents share the same (mis)reading.
Local minima: agent frequently got stuck patching one specific proof gap without global strategy revision.
Human readability: outputs optimized for correctness, not exposition; proofs described as dense and unsuitable for non-experts without expansion.
Evaluation reliability: FirstProof grading allows minor revisions (not full formal verification); researcher feedback is adaptive (prompt changes between runs); 6/27 non-Erdős outputs have no feedback yet.
Execution fragility: P6 excluded due to unrecovered API timeout errors.

Relevance to Harnesses / Meta-Harnesses¶

ProofCouncil's agent-building library is a direct instance of a meta-harness: it provides a runtime that composes heterogeneous agents (LLM nodes, Python blocks, CAS workers, human nodes) into conditional DAGs with parallel branch dispatch, bounded loop unrolling, and structured inter-node I/O via YAML tags — exactly the orchestration primitives that define a general-purpose harness substrate. The dual-gating critic pattern (stateful critic + fresh critic before acceptance) is a concrete harness-level reliability mechanism showing how independent re-evaluation stages can be wired into a DAG without modifying individual agent prompts. The cost breakdown by component ($3,186 across 9 problems) also provides rare empirical data on the resource profile of a multi-agent harness under real-world load, directly informing harness design tradeoffs between verification depth and budget.