ProofCouncil: An LLM Agent for Solving Open Mathematical Problems
06:00 · July 13, 2026 · arXiv cs.AI RSS
Large language models (LLMs) have shown increasing promise in solving open problems in mathematics. However, their performance can be further improved through agentic workflows tailored to real-world mathematical practice. To this end, we introduce ProofCouncil, a mathematical agent that is designed to tackle open problems using an author-critic architecture. ProofCouncil served as a submission to the second batch of FirstProof, a challenge consisting of 10 real-world mathematical problems that agents must solve autonomously. Its submissions for 6 of the 10 problems were judged by the referees to be correct up to at most minor revisions, showing the best performance among participating teams. We also evaluate ProofCouncil on 30 open problems collected from mathematical researchers. Among the 21 solutions that received human feedback, 5 were judged completely correct, 2 more were judged promising pending final verification, and a further 8 contained useful partial progress. In this short paper, we describe the development of ProofCouncil and the agent-building library used to create it, which we release as open source to the community.
Summary
ProofCouncil is an LLM-based agent built to tackle open mathematical problems through an iterative author-critic loop. An author agent, running GPT-5.5-Pro with code execution and search tools, maintains and revises a LaTeX proof file along with research notes and a bibliography. After each revision the critic, also based on GPT-5.5-Pro, reviews the files for gaps or errors. The critic normally retains conversation history across rounds but is reset every three iterations to reduce path dependence; acceptance occurs only when both the stateful critic and a freshly initialized critic agree that the proof is complete.
The author can issue structured requests for help outside this loop. A council of independent models (Gemini 3.1 Pro, Claude Opus 4.7, and GPT-5.5-Pro) answers targeted questions about the current draft, while a separate compute node, implemented with GPT-5.5-Pro and access to SageMath, GAP, Singular, and Pari, performs computer-algebra calculations. Responses from both auxiliaries are returned to the author in the subsequent round. The entire workflow is expressed as a conditional directed acyclic graph that supports bounded loops, conditional edges, and parallel execution of independent nodes.
The underlying agent-construction library that encodes these graphs is released as open source, together with ProofCouncil itself. Nodes in the library can represent LLM calls, Python blocks, deterministic checks, or nested agents, allowing future workflows to be assembled and executed in topological order once all dependencies and edge conditions are satisfied.
In the second FirstProof challenge, which required autonomous solution attempts on ten previously unsolved problems within a 24-hour limit, ProofCouncil produced submissions judged correct up to at most minor revisions for six of the ten problems, the strongest result among participating teams. On a separate collection of thirty open problems supplied by mathematical researchers, feedback was received for twenty-one attempts; five were deemed fully correct, two appeared promising pending final verification, and eight offered useful partial progress. No submission judged to claim a solution was found mathematically incorrect, although two solved easier variants of the stated problems.
Why it matters
This research is highly relevant for Dutch AI researchers as it features contributions from Leiden University and provides an open-source, state-of-the-art framework for building advanced AI agents. The conditional DAG architecture offers actionable methodologies for AI teams in the Netherlands developing complex reasoning systems.
