ProofCouncil: An LLM Agent for Solving Open Mathema... | AI Research

ProofCouncil is an AI agent designed to tackle complex, open-ended mathematical problems autonomously. By utilizing an "author-critic" architecture, the system mimics the collaborative nature of mathematical research, where one agent drafts and refines proofs while another evaluates them for errors and logical gaps. The project aims to improve the reliability of AI-generated mathematics by integrating specialized tools and multi-model feedback into a structured, iterative workflow.

How ProofCouncil Works

The core of ProofCouncil is a loop where an "author" agent drafts a proof in LaTeX and maintains research notes. A "critic" agent reviews these drafts, providing feedback that the author uses to revise the work. To prevent the system from getting stuck in biased patterns, the critic is periodically reset to provide a fresh, independent perspective.
Beyond this loop, the author can request help from two auxiliary sources:

• LLM Council: A group of diverse, high-performing language models that provide independent feedback on the author's current progress.

• Compute Node: A specialized agent that can run computer algebra systems (such as SageMath or GAP) to perform calculations, verify claims, or search for counterexamples.
  The system is built on an open-source library that represents these agents as a conditional directed acyclic graph (DAG). This structure allows for flexible, complex workflows where different agents can be triggered based on specific conditions or intermediate results.

Performance and Results

ProofCouncil was tested in the FirstProof challenge, a competition involving 10 real-world mathematical problems. It achieved the best performance among participating teams, with 6 of its 10 submissions judged as correct or requiring only minor revisions.
In a separate evaluation, the researchers tested the agent on 30 open problems submitted by mathematicians. Of the 21 solutions that received human feedback, 5 were deemed completely correct, 2 were considered promising, and 8 showed useful partial progress. Notably, no expert reported that any of the agent's outputs were mathematically false, though some problems were misinterpreted or solved in a simplified form.

Limitations and Future Directions

While ProofCouncil demonstrates significant potential, it faces several challenges:

• High Costs: The system is expensive to run, costing over $200 per problem due to the heavy use of frontier AI models.

• Problem Interpretation: The agent sometimes misinterprets the scope of a problem, leading it to solve a simpler version than intended. Because the critic shares the author's interpretation, these errors can be difficult for the system to catch on its own.

• Readability: The agent is optimized for finding correct proofs rather than writing them for human readers. The resulting documents are often dense and would require significant editing to be suitable for a standard research paper.
  The authors have released their agent-building library as open source, providing a framework for other researchers to build and experiment with their own agentic mathematical systems.