{"id":"19431770-ba0c-47f9-8e50-aa90131b749c","arxiv_id":"2607.09474","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"partial","parameter_count":3,"one_line_summary":"An author-critic LLM agent with council and compute auxiliaries solved 6/10 FirstProof open math problems and several researcher open problems, with open-source tooling.","lead":"ProofCouncil is an author-critic LLM agent that solved 6 of 10 open problems in the FirstProof challenge up to minor revisions, best among teams. It also produced complete or partial progress on many researcher-submitted open math problems and releases an open-source DAG agent library.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"The 6/10 FirstProof claim rests on referee grades of withheld submissions, so independent verification of mathematical correctness is not possible from the paper alone.","rationale":"The Reader correctly flags human grades and adaptive evaluation as the weakest assumption and lands on CONDITIONAL with high confidence. I agree that those issues justify CONDITIONAL rather than ACCEPT, and that the open-source library, transparent cost/failure reporting, and Lean-backed Erdős-539 case study are real strengths. The sharper load-bearing concern is narrower: the 6/10 FirstProof result is the paper’s strongest claim, yet the graded proofs themselves are not inspectable. That is a stronger verification gap than “human judgment is imperfect,” because even a careful reader cannot re-check the mathematics. The researcher-problem results are similarly non-reproducible (solutions withheld as IP). This does not falsify the claim—external FirstProof referees are credible—but it keeps the central number non-auditable from the manuscript. Hence I keep CONDITIONAL (not REJECT or UNCHANGED in the sense of upgrading), with partial agreement: same verdict, different emphasis on what is least secure.","tokens_in":20878,"tokens_out":599,"duration_ms":10188,"concrete_test":"Release the six FirstProof answer.tex files (and, if permitted, anonymized referee reports) under the same license as the library, or deposit them with an independent math referee for a second full audit. If even one of P1/P2/P3/P5/P7/P9 is then judged to require major revision or to solve a weaker interpretation, the headline 6/10 claim must be revised downward.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The paper’s central empirical claim is that ProofCouncil’s autonomous submissions for 6 of 10 FirstProof problems (P1, P2, P3, P5, P7, P9) were judged by appointed expert referees “correct up to at most minor revisions,” best among teams (Abstract; Sec. 3.2.1). That claim is load-bearing for the systems contribution, yet the manuscript does not include the six accepted proofs, the referee reports, or even short technical summaries of the arguments. The only detailed mathematical artifact is the cleaned Erdős-539 case study (App. A), which is partial progress with a Lean formalization of main ingredients, not one of the six FirstProof solves. The authors correctly note human-judgment dependence and adaptive development (Sec. 4), but the stronger gap is that an external reader cannot check whether the graded solutions are actually correct, whether “minor revisions” hide substantial gaps, or whether problem interpretation (already a failure mode on the researcher set) affected any of the six. Without the artifacts, the 6/10 number is an authority citation rather than a checkable scientific result.","agreement_with_reader":"partial"},"referee_report":{"model":"grok-4.5","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.","tokens_in":21178,"tokens_out":1400,"duration_ms":28674,"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":[{"comment":"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.","section":"Sec. 3.2.1"},{"comment":"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.","section":"Sec. 3.1, Sec. 4"},{"comment":"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).","section":"Sec. 3.2.2"}],"minor_comments":[{"comment":"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.","section":"Fig. 2, Sec. 3.1"},{"comment":"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.","section":"App. A, Sec. 3"},{"comment":"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.","section":"Sec. 3.2.1, Fig. 3"},{"comment":"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.","section":"Throughout"},{"comment":"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.","section":"Sec. 2.1"}],"recommendation":"major_revision","confidential_remarks":"The FirstProof 6/10 claim is currently an authority citation to competition referees; if the journal’s bar requires checkable math artifacts for headline solve counts, the authors may need organizer permission to release redacted proofs or technical abstracts. Fit is appropriate for a short systems/AI-for-math venue; less so for a pure mathematics journal. Novelty of the author–critic idea is incremental relative to concurrent agent papers, so the open library and real open-problem evaluation are the main differentiators."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The thing to know is that this is a working author–critic math agent with external grades, not a pure methods sketch. On FirstProof it got 6/10 submissions judged correct up to minor revisions (best among teams), and on 21 researcher problems with feedback it got 5 complete solutions, 2 pending, and 8 useful partials, with no claimed full solution called mathematically false. They also ship the conditional-DAG library and a cleaned Erdős 539 case study that improves the published upper bound to n^{1/2+o(1)}, with Lean covering the main combinatorial ingredients.\n\nWhat is actually new is the concrete stack: stateful critic with periodic fresh audit, optional multi-model council, CAS compute worker, and the open library that unrolls the loop as a conditional DAG. Concurrent agent papers exist; this one is distinguished by the FirstProof result, the researcher-problem feedback table, and the released tooling. The evaluation is unusually honest for the genre: cost (~$200–350/problem), adaptive prompt/bug fixes, misinterpretation as a failure mode, one critic false positive on P8, and the P3 case where the critic kept rejecting a referee-accepted write-up. Appendix A is real math, not marketing.\n\nThe soft spot the stress-test flags is real and load-bearing: the six FirstProof proofs and referee reports are not in the paper, so the 6/10 number is an authority citation. You cannot audit “minor revisions,” interpretation, or gaps yourself. That is a genuine limit of the short-paper format and of the challenge’s IP setup, not a hidden contradiction. Secondary caveats—adaptive development on the researcher set, withheld solutions, high cost, human-judgment dependence—are already stated in Sec. 4 and should be read as such, not as fatal.\n\nThis is for people building or evaluating AI math agents, and for mathematicians who want a concrete harness plus an open library. The citation pattern is fine; the Lean and code release count as real evidence. I would send it to peer review. Engage if you care about agent systems or open-problem evaluation; treat the 6/10 as strong external signal, not as a fully checkable theorem.","headline":"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.","tokens_in":21782,"tokens_out":542,"would_cite":true,"duration_ms":6234,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68T20","03B35"],"pacs":[],"model":"grok-4.5","headline":"An author–critic LLM agent can autonomously produce solutions to open mathematical problems that expert referees and researchers judge correct or nearly correct.","keywords":["LLM agents","mathematical problem solving","author-critic architecture","open problems","proof verification","computer algebra systems","agent workflows","conditional DAGs"],"falsifier":"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.","tokens_in":21785,"feed_emoji":"🧮","tokens_out":890,"duration_ms":24511,"temperature":0.7,"pith_summary":"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.","feed_headline":"Agent solves 6 of 10 open math problems up to minor fixes","feed_subtitle":"Author–critic loop leads a ten-problem challenge and yields five complete researcher solutions.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["ProofCouncil solves 6 of 10 open math problems with minor revisions","Author-critic agent tops open math challenge with 6 accepted solutions","LLM agent ProofCouncil clears six real open math problems in challenge","ProofCouncil author-critic loop yields 6 of 10 challenge solutions","Agent solves open research math problems: 6 of 10 pass with minor fixes"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["ProofCouncil solves 6 of 10 open math problems with minor revisions","Author-critic agent tops open math challenge with 6 accepted solutions","LLM agent ProofCouncil clears six real open math problems in challenge","ProofCouncil author-critic loop yields 6 of 10 challenge solutions","Agent solves open research math problems: 6 of 10 pass with minor fixes"]},"model":"grok-4.5","effort":"low","cost_usd":0.005956,"raw_usage":{"total_tokens":1540,"prompt_tokens":725,"num_sources_used":0,"completion_tokens":78,"cost_in_usd_ticks":59560000,"prompt_tokens_details":{"text_tokens":725,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":737,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":725,"tokens_out":78,"duration_ms":8631,"temperature":1.0,"reasoning_tokens":737,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-13T02:45:18.159734+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"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.","supporting_citations":[],"review_version":1}