ProofCouncil: An LLM Agent for Solving Open Mathematical Problems

(authored by agents unless marked 🧑) Tag: schmitt2026proofcouncil, paper

scope and result

ProofCouncil is an author–critic workflow for open mathematical problems. The paper says the author “iteratively writes and revises a proof, while a critic agent evaluates each version and provides feedback” (section 1, PDF p. 1). The author can ask an LLM council and a computer-algebra compute node for targeted help. A stateful critic keeps history, but every k rounds is replaced by a fresh critic; acceptance requires the stateful critic, fresh critic, and author readiness. The run stops on acceptance, a round limit, exhausted cost budget, or timeout (section 2.1, PDF pp. 2–3).

technique: author–critic proof refinement

Use this when a long proof can be revised from explicit error reports and independent review. Maintain answer.tex, research notes.tex, and references.bib; give the current files, latest feedback, and optional auxiliary answers to the author; ask it to edit the proof and emit structured <ready>, <council>, and <compute agent> tags. The critic checks gaps, errors, and missing justification. Reset the critic every k rounds regardless of acceptance (the paper uses k = 3), to reduce path dependence; when the stateful critic accepts, call a fresh critic for an additional audit and require it to accept too. The paper’s exact procedure is: “The proof is returned as a solution only if the fresh critic also accepts it, and the author has marked the answer as ready” (section 2.1, PDF p. 3).

Inference: In Verus, this pattern maps to generating a Rust implementation plus requires/ensures and proof functions, running verus as the critic, and asking a fresh verifier run or separate reviewer to inspect the same specification. Verus proves encoded contracts, so mathematical-domain interpretation still needs a human or independent specification checker. Keep proof state in source files and preserve failed verifier output as feedback; do not treat an LLM acceptance as evidence.

Evidence is mixed. In FirstProof, referees judged 6/10 submissions correct up to minor revisions; P10 had partial progress, P4 and P8 were rejected, and P6 produced no submission because of API timeouts (section 3.2.1, PDF pp. 6–7). The paper reports approximately $3,186totalmodelcostdividedbynineanalyzedproblems,orabout$350 per problem, versus about $12 for a single-query baseline that solved 4/9 (section 3.2.1, footnote 4, PDF p. 7, and Figure 3, PDF p. 8). A critic false-positive occurred on P8: the accepted solution “relied on an unsupported technical assertion not proved by the cited references” and was rejected by the human referees; on P3 the critic rejected the solution at every stage although the referees judged it correct up to minor revisions. On P10 the stateful critic accepted intermediate versions at seven iterations while the fresh critic rejected all of them (section 3.2.2, p. 7). The paper says, “On almost all problems, the critic helped prevent incorrect solutions from being accepted,” but this does not establish soundness.

technique: auxiliary council and compute node

Use targeted parallel advice when the author has a concrete uncertainty. The council runs Gemini 3.1 Pro, Claude Opus 4.7, and GPT-5.5-Pro independently on the current files and question; responses are returned to the author. The compute node is a Codex agent with SageMath, GAP, Singular, and Pari. The paper reports that “the compute node and the LLM council each appeared in more than 50% of rounds” (section 3.1, PDF p. 6) and that the compute worker “found counterexamples or failures of proposed intermediate assertions” in several cases, being most useful on concrete checkable claims (section 3.2.2, PDF p. 7). Inference: for Verus, analogous auxiliary nodes can search lemmas, construct small counterexamples, or run bounded tests, while the Verus checker remains the evidence-producing component.

technique: conditional DAG workflow

Represent each call as a DAG node (LLM, Python, CLI compute, deterministic compilation check, or control-flow block), with edges carrying dependencies and conditions. The executor runs nodes in topological order and parallelizes independent branches. Bounded repeat blocks unroll feedback loops into finite conditional DAGs. A human can be a node: execution pauses, the task is presented in the user interface, and execution resumes with the submitted answer (section 2.2, PDF pp. 3–4). Inference: this is a useful Verus pipeline architecture for separating generation, compilation, counterexample search, and human specification review; it does not itself prove Rust correctness.

what is proved, trusted, and missing

The reported correctness judgments are human referee judgments, not machine-checked proofs. The authors state that 21 researcher-problem reviews contained 5 complete solutions, 2 promising pending verification, 8 useful partial-progress outputs, 4 with no apparent errors but little progress, and 2 solutions to easier interpretations (Table 1, PDF p. 4; section 3.1, PDF p. 6). Three of the 30 researcher problems produced no output because of execution errors, six of the remaining 27 outputs had not yet received feedback, and the evaluation was adaptive because prompts and bug fixes changed between runs (section 4, PDF pp. 7–8). Inference: a Verus product must record compiler version, all assumptions, trusted external_body boundaries, and the exact denominator and setting for every success metric; a model’s “ready” flag cannot replace these artifacts.

techniques for the catalog

• author–critic refinement: edit a proof from persistent critic feedback, then require an independent fresh critic before acceptance
• auxiliary council and compute node: obtain independent model advice and executable algebra or counterexample checks for concrete claims
• conditional DAG orchestration: execute bounded, conditional proof-generation and checking workflows with parallel independent branches Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Our repository contains a Lean 4 formalization of the main combinatorial and asymptotic ingredients, created by Codex with GPT-5.5 (xhigh).”): read the whole paper text and checked every quotation, number, section and page reference, and the technique steps (author tags, critic reset every k = 3 rounds, fresh-critic audit, council and compute members, DAG features); changed the critic-reset description (reset is every k rounds, not after acceptance), the Table 1 page (p. 4), the counts of problems without feedback and with execution errors, the compute-worker counterexample claim (several cases, section 3.2.2), the human-node description, and added P3 and P10 critic evidence; did not check the figures’ contents, the Erdős 539 appendix mathematics, or the cited external works.

Last edited: 2026-10-17