Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

An author–critic LLM agent can autonomously produce solutions to open mathematical problems that expert referees and researchers judge correct or nearly correct.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-13 02:45 UTC pith:OQTPTKJH

load-bearing objection Solid systems paper with external FirstProof referee grades and a real Erdős-539 construction; the 6/10 claim is authority-backed rather than checkable from the manuscript alone. the 3 major comments →

arxiv 2607.09474 v1 pith:OQTPTKJH submitted 2026-07-10 cs.AI

ProofCouncil: An LLM Agent for Solving Open Mathematical Problems

Johannes Schmitt , Tim Gehrunger , Jasper Dekoninck , Gergely B\'erczi , Uri Kreitner , Liam Price , David Holmes This is my paper
classification cs.AI MSC 68T2003B35
keywords LLM agentsmathematical problem solvingauthor-critic architectureopen problemsproof verificationcomputer algebra systemsagent workflowsconditional DAGs
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper introduces ProofCouncil, an agent built to attack open mathematical problems the way working mathematicians do: write a proof, take criticism, revise, and only stop when an independent check accepts the result. On a fixed challenge of ten problems with no public solutions, its autonomous submissions for six problems were judged correct up to at most minor revisions, the strongest showing among participating systems. On thirty open problems collected from researchers, human feedback on twenty-one outputs counted five complete solutions, two promising near-solutions, and eight cases of useful partial progress, with no claimed full solution reported as mathematically false. The same work releases an open library that builds such agents as conditional directed graphs of model and tool calls, so others can reuse the pattern.

Core claim

ProofCouncil’s iterative author–critic workflow—augmented by optional multi-model council advice, computer-algebra compute help, and periodic fresh-critic audits—can solve real open research problems well enough that expert referees accept six of ten challenge submissions with only minor revisions and researchers accept five complete solutions among the outputs they reviewed.

What carries the argument

The author–critic loop: an author revises a LaTeX proof and research notes while a critic reviews them; the critic’s history is reset every few rounds, and a solution is returned only when both the author and a freshly initialized critic mark the proof ready, with optional side calls to an LLM council and a CAS-equipped compute worker.

Load-bearing premise

That human referee grades of “correct up to minor revisions” and researcher feedback truly certify the mathematics, and that prompt and bug fixes made during evaluation do not inflate success relative to a single frozen system.

What would settle it

Independent expert re-checks of the six challenge submissions and five claimed complete researcher solutions that find a material mathematical error in any output that claimed a full solution, or a frozen-configuration re-run that fails to reproduce comparable solve rates under the same time and cost limits.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Author–critic agentic workflows can raise solve rates on open math challenges relative to single-query frontier models (six versus four of nine analyzed problems in the reported challenge run).
  • Fresh independent critic audits can reject incomplete drafts that a history-carrying critic has already accepted.
  • CAS-backed compute workers can catch false intermediate claims and supply literature or counterexamples the main loop can reuse.
  • An open conditional-DAG agent library lets others compose similar proof, critique, and tool workflows without rebuilding the harness.
  • Problem interpretation remains a distinct failure mode: the system can correctly solve an easier reading of a statement that both author and critic share.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Running several author–critic threads in parallel, as the paper itself suggests against local minima, is a direct way to trade cost for more diverse proof strategies.
  • An external statement-auditor that does not share the author’s reading of the problem would address the misinterpretation cases the internal loop cannot catch.
  • Routing lighter subtasks to cheaper models, as the cost discussion proposes, is a concrete next experiment if the goal is wider use rather than peak solve rate.
  • The Erdős-problem case study shows the same loop can improve published asymptotic bounds and hand off core combinatorial arguments to formal proof assistants.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper introduces ProofCouncil, an LLM agent for open mathematical problems built around an author–critic loop with optional LLM-council and CAS compute assistance, plus an open-source library that represents agent workflows as conditional DAGs. The main empirical claims are that ProofCouncil’s autonomous FirstProof (second batch) submissions for 6 of 10 problems were judged by appointed expert referees correct up to at most minor revisions (best among participating teams), and that on 30 researcher-supplied open problems, among 21 outputs with human feedback, 5 were complete solutions, 2 promising pending verification, and 8 useful partial progress, with no claimed full solution reported as mathematically false. The manuscript describes the architecture, prompts, cost breakdown, qualitative component utility, limitations (cost, adaptive development evaluation, problem misinterpretation, human-judgment dependence), and a detailed Erdős Problem 539 case study with a Lean formalization of main combinatorial ingredients.

Significance. If the reported outcomes hold under independent scrutiny, this is a meaningful systems contribution: an openly released agent and DAG library aimed at research-level mathematics, evaluated on genuinely open problems rather than closed benchmarks, with external FirstProof referee grades and researcher feedback, transparent cost accounting, and an explicit Lean-backed combinatorial case study (App. A). Strengths include the open-source release, the honest failure-mode discussion (misinterpretation, local minima, one critic false positive on P8), and the machine-checked formalization of the main Erdős-539 ingredients. The work is significant primarily as an engineering and evaluation report for agentic mathematical practice, not as a pure theorem paper.

major comments (3)
  1. [Sec. 3.2.1] Sec. 3.2.1 / Abstract: the headline claim that 6 of 10 FirstProof submissions (P1–P3, P5, P7, P9) were correct up to at most minor revisions is load-bearing for the systems contribution, yet the manuscript provides neither the six proofs, referee reports, nor short technical summaries of the arguments. An external reader therefore cannot check mathematical correctness, the substance of “minor revisions,” or whether problem interpretation affected any accepted case. At minimum, the paper should add checkable technical abstracts of each accepted solution (or point to a public FirstProof artifact dump if available) and state explicitly what remains confidential and why.
  2. [Sec. 3.1, Sec. 4] Sec. 3.1 and Sec. 4: the researcher-problem statistics (5 complete / 2 promising / 8 partial among 21 reviews) come from an adaptive development process—prompt changes and bug fixes between runs informed by earlier feedback—and three problems in the first 10-problem run hit execution errors. As written, these numbers are not an evaluation of a single frozen configuration. The paper should either (i) report a frozen-config re-run on a held-out subset, or (ii) restructure Tab. 1 / Fig. 2 to separate development runs from any fixed evaluation and avoid presenting the pooled counts as a single success rate.
  3. [Sec. 3.2.2] Sec. 3.2.2: component utility (critic resets, council members, compute worker) is discussed only qualitatively from one competition run, with no controlled ablations (e.g., author-only vs author–critic vs full system; k=3 vs no reset). Given that cost is ~$350/problem and the architecture’s novelty is the multi-agent design, at least one small ablation or leave-one-component-out comparison on a fixed problem subset is needed to support claims that the author–critic loop and auxiliaries drive the solve-rate gain over the single-query GPT-5.5-Pro baseline (4/9 vs 6/9).
minor comments (5)
  1. [Fig. 2, Sec. 3.1] Fig. 2 progress scores are GPT-5.5-Pro postscreen estimates of intermediate logs; the caption and Sec. 3.1 already caution interpretation, but the main text still leans on “some problems were only marked as solved after several rounds.” Soften causal language or move the panel fully to an appendix as exploratory.
  2. [App. A, Sec. 3] App. A is a strong, checkable mathematical artifact, but it is partial progress on Erdős 539, not one of the six FirstProof solves. Cross-reference more clearly in Sec. 3 so readers do not treat App. A as representative of the FirstProof acceptances.
  3. [Sec. 3.2.1, Fig. 3] Cost figures ($213/problem open set; ~$350/problem FirstProof; Fig. 3) are useful; add a short reproducibility note on model versions, reasoning-effort settings, and whether the released library can reproduce the exact FirstProof harness configuration.
  4. [Throughout] Typographical/consistency nits: “research notes.tex” vs “research_notes.tex” naming in prose vs prompts; occasional spacing issues (e.g., “B´ erczi”); ensure all arXiv/FirstProof citations that are still “2026” preprints are stable enough for the camera-ready version.
  5. [Sec. 2.1] Sec. 2.1: state the stopping criteria (max rounds, budget, timeout, dual acceptance) more formally, including the exact k=3 reset policy and the dual-critic acceptance rule, in one place rather than distributed across text and figure caption.

Circularity Check

0 steps flagged

No significant circularity: empirical solve-rate claims rest on external referee/researcher judgments, and the Erdős-539 case study is an independent combinatorial construction.

full rationale

ProofCouncil is a systems/evaluation paper whose load-bearing claims are empirical performance numbers (6/10 FirstProof submissions judged correct up to minor revisions by appointed external referees; 5 complete + 2 promising + 8 partial among 21 researcher-problem reviews). Those numbers are not derived from any fitted parameter, self-defined quantity, or uniqueness theorem internal to the paper; they are authority citations to independent human graders. The only detailed mathematical derivation (App. A, Erdős 539) proceeds by explicit constructions (base strip BW, separated suspension SK(F), iteration of exponents αs = bs/as, optimization of suspension depth) that produce a new upper bound h(n) ≤ n^{1/2} exp(C √log n) and the limit lim log h(n)/log n = 1/2; the argument does not redefine its target in terms of itself, nor does it import a load-bearing uniqueness result from the authors’ prior work. Minor self-citations (e.g., Schmitt 2025 on AI-assisted math) appear only as background and are not used to force the FirstProof or researcher-problem claims. Adaptive development and withheld solution artifacts raise verification/correctness concerns, but those are outside the circularity criteria. Hence score 0 with empty steps.

Axiom & Free-Parameter Ledger

3 free parameters · 4 axioms · 2 invented entities

As a systems/evaluation paper the load-bearing premises are engineering choices and evaluation assumptions rather than physical free parameters. The mathematical case study rests on standard number-theory and combinatorial constructions. No new physical entities are postulated.

free parameters (3)
  • critic_reset_period_k = 3
    Stateful critic is reset every k rounds (k=3 in experiments); choice affects path-dependence vs. independence of audits.
  • max_rounds_and_cost_timeout = up to 200 rounds / 24h / ~$200–350 per problem
    Stopping criteria (max rounds up to 200, 24h, cost budget) are hand-set and determine how far the loop can search.
  • model_and_effort_choices
    Author/critic use GPT-5.5-Pro (xhigh); council uses Gemini 3.1 Pro, Claude Opus 4.7, GPT-5.5-Pro; compute uses GPT-5.5 (xhigh). These are design choices that dominate performance and cost.
axioms (4)
  • standard math Standard number theory and combinatorial difference-set facts used in the Erdős-539 appendix (unique factorization, positive orthant projection equivalence, difference-set size lemmas).
    Background for Theorem A.1 and Lemmas A.2–A.6; not novel axioms of the systems paper.
  • domain assumption Human expert referees and problem authors can reliably judge mathematical correctness up to minor revisions.
    Central to all reported solve rates in Sec. 3; acknowledged as a limitation in Sec. 4.
  • domain assumption Frontier LLMs with code execution, web search, and CAS tools can produce and critique research-level proofs when orchestrated in an author-critic loop.
    Operational premise of the entire architecture (Sec. 2).
  • ad hoc to paper Adaptive prompt and bug fixes between development runs do not invalidate the reported open-problem statistics as evidence of system capability.
    Explicitly flagged in Sec. 4 as making the researcher-problem results an adaptive development evaluation rather than a frozen-config evaluation.
invented entities (2)
  • ProofCouncil author-critic-council-compute architecture independent evidence
    purpose: Orchestrate iterative proof writing, critique, multi-model advice, and CAS computation for open math problems.
    Engineered system, not a postulated natural entity; independent evidence is the empirical FirstProof and researcher evaluations plus released code.
  • Conditional-DAG agent-building library independent evidence
    purpose: Represent agent workflows as conditional directed acyclic graphs with hierarchical nodes, human-in-the-loop, and visual editing.
    Software artifact released open-source; evidence is the repository and screenshots in App. B.

pith-pipeline@v1.1.0-grok45 · 25016 in / 3159 out tokens · 35052 ms · 2026-07-13T02:45:18.159734+00:00 · methodology

0 comments
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2607.09474 by David Holmes, Gergely B\'erczi, Jasper Dekoninck, Johannes Schmitt, Liam Price, Tim Gehrunger, Uri Kreitner.

Figure 1
Figure 1. Figure 1: Overview of ProofCouncil. The author agent iteratively edits the proof in response [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Progress panel for all 33 attempted problems: rows R1–R3 show the three 10- [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: ProofCouncil model spend by component in the official FirstProof run. [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: View of the execution page, just after starting a run. [PITH_FULL_IMAGE:figures/full_fig_p015_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Node-add menu for inserting reusable workflow components into a DAG. [PITH_FULL_IMAGE:figures/full_fig_p016_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Graph view for inspecting workflow structure and the state of individual nodes. [PITH_FULL_IMAGE:figures/full_fig_p016_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Node editor for changing prompts, model configuration, input bindings, and output [PITH_FULL_IMAGE:figures/full_fig_p017_7.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Albilich: Steerable Proof-State Orchestration for LLM-Based Mathematical Research with CAS Integration

    cs.AI 2026-07 reject novelty 5.0

    Albilich, an agentic math-research harness with persistent proof state, CAS integration, and an advisor role, reports 10/10 RealMath solves and two Kourovka results, but with no public artifacts or independent verification.

Reference graph

Works this paper leans on

12 extracted references · cited by 1 Pith paper

  1. [1]

    Read each input file from its read-only path (it will be empty on round 0)

  2. [2]

    Build the new contents (in memory, or by copying then editing)

  3. [3]

    /mnt/data/<name>

    Write the new contents to the canonical write path with``Path("/mnt/data/<name>").write text(...)``. Do not write to``.new``/``.bak``/ sibling paths | only the canonical paths are picked up by the infrastructure after your turn

  4. [4]

    thinking summary

    Run``pdflatex /mnt/data/answer.tex``from a code interpreter cell to confirm it compiles before claiming readiness. Do NOT paste the file contents in your reply text. Anything in the reply text outside the optional control blocks below is treated as a brief free-text "thinking summary" for the Critic. Research ambition and problem interpretation. Your goal...

  5. [5]

    Read its current contents from the listed read-only path

  6. [6]

    Build the new contents

  7. [7]

    /mnt/data/<name>

    Write to the canonical write path with``Path("/mnt/data/<name>").write text(...)``. Do not write to``.new``/``.bak``/sibling paths | only canonical write paths are picked up

  8. [8]

    thinking summary

    Compile-check answer.tex with``pdflatex``before claiming readiness. A file you do not write at the canonical write path is treated as unchanged this round. **``research notes.tex``is your persistent scratchpad across rounds.** Accumulate definitions, intermediate lemmas, computational sanity-checks, alternative-approach sketches, dead ends you ruled out, ...

  9. [9]

    Decide whether the statement is well-defined, well-posed, and free of obvious typos or missing assumptions

  10. [10]

    Do a brief literature scan (web search) and a small computational sanity check (code interpreter) when useful, to see whether the problem has a known answer or is much easier or much harder than it appears

  11. [11]

    Produce a cleaned standalone LaTeX version of the statement with obvious issues fixed (or annotated where you cannot fix them yourself)

  12. [12]

    Be terse and precise

    Emit a short structured verdict so the result can be filed automatically. Be terse and precise. Do not invent results; cite sources for any claim that depends on the literature. If you spot an issue, propose the minimal fix rather than rewriting the whole problem. Use``$...$``for inline math and``$$...$$``for display math in the markdown report so it rend...