Pith. sign in

REVIEW 3 major objections 4 minor 13 references

Albilich, a multi-agent proof-state harness with computer-algebra support, reports completing research-level math problems and refuting an open group-theory question.

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 · deepseek-v4-flash

2026-08-01 02:56 UTC pith:B7F5K2IK

load-bearing objection Genuinely interesting proof-state orchestration system, but the headline mathematical results are not externally auditable; treat as a system paper, not a results paper. the 3 major comments →

arxiv 2607.27705 v1 pith:B7F5K2IK submitted 2026-07-30 cs.AI cs.LG

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

Ting Gong , Michael Ruofan Zeng , Yong Yang This is my paper
classification cs.AI cs.LG
keywords agentic AImathematical researchproof statecomputer algebra systemslarge language modelsinformal verificationfinite group theorytest-time scaling
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.

The paper argues that long-horizon AI mathematics is best organized as a persistent, versioned proof state rather than a linear dialogue. In Albilich, claims, proof routes, failed attempts, unresolved obligations, sources, and cost records are stored and shared among specialized agent roles, with separate verifiers controlling what counts as accepted. The authors report that this design, combined with computer-algebra tool calls, solved all ten problems in a research-level benchmark when computation was enabled (nine of ten without), produced a counterexample to one open group-theory problem and a proof of a strengthening of another, and cut gross token use by 32.0 percent on an ablation task. A second ablation indicates that the advisor role, which redirects strategy, is what assembles verified local results into a completed route. The authors explicitly state that internal informal verification is not formal verification or external grading, so the headline results stand on the trustworthiness of the internal verifier.

Core claim

The central claim is that an LLM-based research system can carry a mathematical problem from statement to accepted solution if its working memory is a database of proof objects with explicit ownership of each state change. Albilich stores the root problem, claims, routes, inferences, a debt ledger of open obligations, source and artifact records, and an event history; agents edit it only through validated patches, and only dedicated verifier roles may mark claims as verified, routes as integrated, or refutations as accepted. The paper reports 10/10 benchmark problems solved with computer algebra and 9/10 without, a counterexample giving a negative answer to an open finite-group problem 21.14

What carries the argument

The key mechanism is the persistent proof state: a versioned graph of claims, routes, and inferences with typed dependency edges, stored in a database, plus a debt ledger, an artifact store, and a history of patches and events. A deterministic scheduler selects the next obligation; each agent session receives a narrow dependency subgraph and can propose a patch, and a patch gate validates role authorization and schema before atomic application. The strict verifier checks bounded proof dossiers and archived CAS artifacts, while the integration verifier checks whether locally verified claims form a sufficient route to the immutable root; the counterexample validator checks refutations. Tool ca

Load-bearing premise

The headline results stand on the trustworthiness of Albilich's internal strict verifier, an LLM role that reads bounded proof dossiers and archived CAS transcripts without re-executing the computation, and the paper itself says internal informal verification is distinct from formal verification and external grading.

What would settle it

Independently audit the archived proof spine for the open group-theory counterexample: re-run the recorded computer-algebra computations, check the reduction from a minimal host to the subgroup chain, and check the terminal simple-factor obstruction by hand or in a formal checker. If the obstruction has a gap or the archived computations do not reproduce, the refutation claim falls; similarly, a seed-controlled replay of the CAS ablation should reproduce the 32.0 percent token reduction.

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

If this is right

  • If the reported benchmark completions hold, the full proof-state workflow can carry research-level problems from statement to internal solved status in a reproducible, auditable way.
  • A confirmed negative answer to open problem 21.142 would settle a published open question in finite group theory, with the obstruction based on alternating groups inside a subgroup chain.
  • The witness for open problem 20.2, PSL(2,7), and the follow-up family-level classification runs point toward an almost complete picture for PSL_n(q) total 3-closure, with only PSL_n(2) for n>=5 remaining.
  • The 32.0 percent token reduction in the CAS ablation suggests that routing work through archived computation instead of model context can be a direct cost lever for long reasoning runs.
  • The advisor ablation implies that raw test-time compute is not sufficient: without strategic redirection, the system verified more local mathematics yet failed to connect it to the root.

Where Pith is reading between the lines

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

  • A natural next step the paper leaves implicit is to funnel the informally verified dossiers through a formal proof checker or an independent executor; if such translation succeeds, the same architecture would produce machine-checkable certificates from its archived artifacts.
  • If the CAS cost reduction generalizes beyond the single ablation, tool-mediated computation may become the primary scaling axis for agentic research systems, shifting spending away from model context and toward small, auditable artifacts.
  • The advisor-on/off contrast suggests a testable hypothesis about long-horizon reasoning in general: performance may be bounded less by the generation of true local statements and more by the assembly of a coherent proof spine, so interventions in route selection and dependency reconciliation could outperform added inference.
  • A direct audit experiment would be to take the internally accepted solutions, re-run the archived CAS transcripts, and trace each dependency closure by hand; surviving audits would be the strongest evidence that the verification design transfers beyond the reported runs.

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 / 4 minor

Summary. The paper presents Albilich, an open-source multi-agent harness for informal mathematical research built around a persistent SQLite proof state. It separates research, advising, adversarial, and verification roles; integrates CAS and literature-retrieval tools via MCP; and uses a strict verifier plus an integration verifier to mark claims and routes. The authors report 10/10 solved_final on RealMath with CAS (and 9/10 without CAS in the abstract), a counterexample to Kourovka Problem 21.142, a witness/proof for Problem 20.2, and ablations showing that CAS reduces token usage and that the advisor aids root-level proof assembly. The paper explicitly classifies its verification as informal and defers formal verification to a later version.

Significance. If the mathematical claims were substantiated, the paper would be significant as a demonstration that a steerable, CAS-integrated multi-agent harness can complete research-level problems and reduce cost; the persistent proof-state design and role separation are genuinely useful engineering contributions. The 32.0% token reduction in the matched CAS ablation and the careful advisor-ablation design are concrete strengths. However, as submitted, the headline results are not independently auditable: the acceptance authority is Albilich's own LLM strict verifier, CAS computations are not re-executed, no proof texts or expert attestations are supplied, and the RealMath no-CAS claim is absent from the experimental section. The engineering ideas are credible, but the central 'solved' and 'proof' claims are unverified.

major comments (3)
  1. [Verification and Integration; Limitations] The central acceptance criterion is an internal loop. The 'strict verifier' is an LLM role checking bounded dossiers, and the paper states 'The strict verifier reads that artifact and does not re-execute the computation' and 'Internal informal verification remains distinct from formal verification, independent peer review, and external benchmark grading.' For Kourovka Problems 21.142 and 20.2 no proof text, GAP/Sage transcript, or independent certification is included; only internal statuses ('exact solution', 'explicit witness') are reported. Because the generating and checking agents are of the same model family and no external artifact is available, the acceptance loop is self-consistent but not auditable. The 'solved' and 'counterexample/proof' claims therefore do not meet the evidentiary standard for research-level mathematical results.
  2. [RealMath Benchmark; Table 3] The abstract's 'solved 10/10 with CAS and 9/10 with no CAS' is not supported by the experimental section. Table 3 reports only the CAS-enabled RealMath run, with outcome '10 final'; no no-CAS RealMath row or table appears. Moreover, the text concedes that 'for Problem 08, the equivalence between Albilich's convolution formula and the reference expression remained unresolved,' and 'Final' denotes Albilich's internal solved_final state. Thus the externally matched count is nine, not ten, and the no-CAS claim is unreported.
  3. [Introduction; Case Studies] The statement 'We have used Albilich to resolve two problems in group theory, verified by human experts' is a core credibility claim, but no names, dates, attestations, or external reports are provided. The case-study section gives only a high-level sketch of a reduction for 21.142 (without the explicit m(p,q)) and the answer G=PSL_2(7) for 20.2, relying on internal certification and GAP transcripts that are neither quoted nor rerun. Without the proof artifacts or an independent mathematician's confirmation, the claim cannot be checked; it should either be removed or fully documented.
minor comments (4)
  1. [Abstract; Experiments] The abstract states '9/10 with no CAS' but no such run is reported in Table 3 or elsewhere; if the run exists, it should be added, including the per-problem outcomes and token counts.
  2. [Case Studies: Open Problems in Group Theory] For Problem 21.142 the paper says 'for some m≥9, depending on p and q' but never gives an explicit m(p,q). As written, this is not a concrete counterexample; the exact construction should be stated.
  3. [Case Studies: Open Problems in Group Theory] There is a typo: 'toward a an almost complete family-level classification' should read 'toward an almost complete family-level classification.' Similar language issues appear in the MCP tool-call section, where 'The literature researcher role as MCP tool calls' is incomplete.
  4. [References] Reference formatting is inconsistent: several entries (e.g., QED, Danus, TheoremSearch) lack arXiv identifiers or complete venue information. The acknowledgements section also misspells 'Acknowledgements.'

Circularity Check

3 steps flagged

Headline 'solved/counterexample/proof' claims are accepted by Albilich's own internal verifier; the 10/10 RealMath count is the internal solved_final state rather than the paper's own 9/10 external match, and CAS transcripts are trusted without re-execution.

specific steps
  1. self definitional [Abstract; Experiments — RealMath Benchmark; Table 3 caption]
    ""It solved 10/10 problems on RealMath with CAS and 9/10 with no CAS." ... "All ten attempts reached solved_final. Human comparison with the supplied references found nine clear matches; for Problem 08, the equivalence between Albilich's convolution formula and the reference expression remained unresolved." ... "'Final' denotes Albilich's internal solved_final state.""

    The abstract's 'solved 10/10' is the count of Albilich's internal solved_final states, not the external benchmark-match count. The paper's own human comparison yields nine clear matches, with Problem 08 unresolved. Thus the headline success count is a restatement of the system's self-assigned acceptance state for the tenth problem, rather than an externally derived result.

  2. other [Verification and Integration; MCP Tool Calls: Literature Search and Computer Algebra; Limitations]
    ""The strict verifier reads that artifact and does not re-execute the computation, so a CAS-supported claim carries the trust level of its transcript." ... "Internal informal verification remains distinct from formal verification, independent peer review, and external benchmark grading.""

    CAS-derived claims are accepted without independent re-execution; the verifier's check reduces to reading a model-produced transcript. Consequently any CAS-backed 'verified' claim is equivalent to the LLM verifier's acceptance of the supplied text, not to a reproduced computation. The open-problem proofs and counterexample rely on this trust model, so the central mathematical claims inherit the transcript's trust level as their only computational grounding.

  3. other [Introduction; Experiments — Case Studies: Open Problems in Group Theory]
    ""We have used Albilich to resolve two problems in group theory, verified by human experts." ... "Albilich reported and internally certified a negative answer..." ... "The archived run certified the explicit answer G= PSL 2(7).""

    The word 'certified' refers to certification by Albilich's own strict and integration verifier roles; no proof text, CAS logs, or independent external attestation is supplied beyond the authors' statement. Since formal verification is explicitly deferred, the claimed counterexample and proof of a strengthening are the system's internal informally_verified status. The conclusion is accepted because the same system's verifier accepted it, forming a self-consistent acceptance loop rather than an externally anchored derivation.

full rationale

The paper has some genuinely non-circular content: the RealMath runs were compared by humans against supplied references (nine clear matches), the CAS ablation reports token counts and run conditions that are independently measurable, and the PhD-advisor ablation compares matched conditions with verifier-rejection statistics. There are no load-bearing self-citations: the references to TheoremSearch, Matlas, Danus, QED, Archon, etc. are external prior work, not the present authors' own papers. However, the central headline claims — 'solved 10/10 on RealMath', 'produced a counterexample to Problem 21.142', 'proof of a strengthening of Problem 20.2' — reduce in part to Albilich's internal solved_final / informally_verified states. The paper itself flags the key limitation: internal informal verification is distinct from formal verification, independent peer review, and external benchmark grading, and CAS artifacts are not re-executed. That transparency is commendable, but it does not remove the self-referential acceptance loop for the open-problem resolutions. The RealMath count is especially concrete: the paper's own external comparison supports 9/10, while the abstract claims 10/10 by counting internal solved_final states. Weighing the external anchors for most of the RealMath runs and the independent ablation metrics against the self-certified open-problem claims, a score of 5 reflects partial circularity: some headline results are internally defined acceptance states, while parts of the evaluation retain independent content.

Axiom & Free-Parameter Ledger

4 free parameters · 4 axioms · 0 invented entities

Free-parameter list is minimal: the system has no fitted numerical constants, but the listed configuration choices and trust policy are hand-selected inputs that all headline numbers depend on. The central assumptions are LLM verifier reliability, trust in CAS transcripts without rerun, and internal solved_final as evidence. Albilich and its agent roles are software components, not theoretical entities, so invented_entities is empty.

free parameters (4)
  • Model and reasoning effort = gpt-5.6-sol with xhigh reasoning
    All reported runs use this proprietary model; results are not reproducible without it and all outcomes depend on this choice.
  • Research and verification budgets = 80M research tokens, 12M verification reserve, max reduction depth 4, full_proof_first
    Hand-selected settings; the advisor ablation compares runs under these exact budgets.
  • CAS ablation stopping conditions = 1-hour limit, 20 child sessions per arm
    Neither arm solved the root problem, so the 32% token reduction reflects cost at a chosen stopping point.
  • Verifier trust policy = informal LLM checks; no CAS rerun; no formal backend
    Hand-chosen acceptance criteria that determine which claims count as verified.
axioms (4)
  • domain assumption The internal strict verifier's LLM-based informal checks reliably certify local claims and citations.
    Central acceptance of every result in Albilich depends on this verifier; §Verification and Integration says formal verification is deferred and CAS artifacts are not re-executed.
  • domain assumption A CAS transcript is trustworthy evidence without independent re-execution.
    The strict verifier reads the artifact and does not rerun the computation (§MCP Tool Calls: Computer algebra systems), so the proof chain inherits any CAS error.
  • domain assumption The internal solved_final state is a valid indicator that a problem is solved.
    The 10/10 RealMath and Kourovka 'solved' outcomes are the system's own final states; no external grading or proof text is given.
  • ad hoc to paper The claimed Kourovka results were checked by human experts.
    Introduction states 'verified by human experts' but provides no names, reports, or details, and Limitations say there is no independent peer review.

pith-pipeline@v1.3.0-daily-deepseek · 9387 in / 13539 out tokens · 137452 ms · 2026-08-01T02:56:38.679118+00:00 · methodology

0 comments
read the original abstract

Large language models can contribute useful ideas to mathematical research, yet long-horizon proof attempts remain difficult to coordinate, evaluate, and reproduce. We present Albilich, an open-source agentic harness for autoresearch in mathematics that combines long-horizon reasoning, computer algebra systems (CAS), literature retrieval, and persistent SQLite-based context management. We evaluate Albilich on the RealMath benchmark (Zhang et al. 2025) and on open problems in group theory from the Kourovka Notebook (Khukhro and Mazurov 2026). It solved 10/10 problems on RealMath with CAS and 9/10 with no CAS. On the Kourovka problems, Albilich produced a counterexample to Problem 21.142 and a proof of a strengthening of Problem20.2. Anablation on Problem 17.91 demonstrates 32.0% token reduction when CAS is enabled. An ablation on Problem 21.142 demonstrates higher verifier-rejection rate and failure to synthesize proof routes in the absence of the advisor agent. These results support Albilich as a human-steerable, CAS-boosted environment for scalable AI-assisted mathematical research.

Figures

Figures reproduced from arXiv: 2607.27705 by Michael Ruofan Zeng, Ting Gong, Yong Yang.

Figure 1
Figure 1. Figure 1: The Albilich workflow. of this state. They may modify it only by submitting validated patches. Proof-State Representation Let q⋆ denote the immutable root statement. At revision t, the proof state consists of St = (q⋆, Gt, Dt,Lt, At,Pt, Ht,Mt), Gt = (Ct ∪˙ Rt ∪˙ It, Γt). (1) Here, Ct, Rt, and It are the sets of claims, proof routes, and inferences. The typed edges Γt record logical dependencies among them.… view at source ↗

discussion (0)

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

Reference graph

Works this paper leans on

13 extracted references · 7 linked inside Pith

  1. [1]

    The GAP Group

    2026.GAP – Groups, Algorithms, and Programming. The GAP Group. https://www.gap-system.org. 2026.SageMath, the Sage Mathematics Software System. The Sage Developers. https://www.sagemath.org. Alexander, L.; Leonen, E.; Szeto, S.; Remizov, A.; Tejeda, I.; Inchiostro, G.; and Ilin, V

    2026

  2. [3]

    arXiv:2604.24021

    QED: An Open-SourceMulti-AgentSystemforGeneratingMathemat- ical Proofs on Open Problems. arXiv:2604.24021. Anthropic

    Pith/arXiv arXiv

  3. [6]

    arXiv:2602.10177

    Towards Autonomous Mathematics Research. arXiv:2602.10177. Grayson, D. R.; and Stillman, M. E

    arXiv

  4. [7]

    http: //www2.macaulay2.com

    Macaulay2, a software system for research in algebraic geometry. http: //www2.macaulay2.com. Ju, H.; Chen, L.; Wu, P.; Dai, B.; and Dong, B. 2026a. Matlas: A Semantic Search Engine for Mathematics. arXiv:2604.17484. Ju, H.; Gao, G.; Jiang, J.; Wu, B.; Sun, Z.; Liu, S.; Chen, L.; Wang, Y.; Wang, Y.; Wang, Z.; He, W.; Wu, P.; Xiao, L.; Liu,R.;Dai,B.;andDong...

    Pith/arXiv arXiv 2026

  5. [9]

    Romera-Paredes, B.; Barekatain, M.; Novikov, A.; Balog, M.; Kumar, M

    Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory.arXiv preprint arXiv:2607.06447. Romera-Paredes, B.; Barekatain, M.; Novikov, A.; Balog, M.; Kumar, M. P.; et al

    Pith/arXiv arXiv

  6. [10]

    arXiv:2607.09474

    ProofCouncil: An LLM Agent for Solving Open Mathematical Problems. arXiv:2607.09474. Xin, H.; Ren, Z. Z.; Song, J.; Shao, Z.; Zhao, W.; Wang, H.; Liu, B.; Zhang, L.; Lu, X.; Du, Q.; Gao, W.; Zhu, Q.; Yang, D.; Gou, Z.; Wu, Z. F.; Luo, F.; and Ruan, C

    Pith/arXiv arXiv

  7. [13]

    arXiv:2605.06651

    AI Co-Mathematician: Accelerating Mathematicians with Agentic AI. arXiv:2605.06651

    Pith/arXiv arXiv

  8. [21]

    July 2026 update

    Novosibirsk:SobolevInstituteofMathematics,21stedition. July 2026 update. Liu, J.; Gao, G.; Sun, Z.; Wu, B.; Liu, S.; Jiang, J.; Ju, H.; Chen, L.; Cheng, R.; Zhang, X.; and Dong, B

    2026

  9. [2021]

    InAutomated Deduc- tion–CADE28,volume12699ofLectureNotesinComputer Science, 625–635

    The Lean 4 Theorem Prover and Programming Language. InAutomated Deduc- tion–CADE28,volume12699ofLectureNotesinComputer Science, 625–635. Springer. Decker, W.; Greuel, G.-M.; Pfister, G.; and Schönemann, H. 2024.Singular— A computer algebra system for polyno- mial computations. http://www.singular.uni-kl.de. Feng, T.; Trinh, T. H.; Bingham, G.; Hwang, D.; ...

    2024

  10. [2023]

    arXiv:2306.15626

    Le- anDojo: Theorem Proving with Retrieval-Augmented Lan- guage Models. arXiv:2306.15626. Zhang,J.;Petrui,C.;Nikolić,K.;andTramèr,F.2025. Real- Math: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics. InAdvances in Neural Information Processing Systems, volume

    Pith/arXiv arXiv 2025

  11. [2024]

    arXiv:2408.08152

    DeepSeek-Prover-V1.5: Harnessing Proof Assistant FeedbackforReinforcementLearningandMonte-CarloTree Search. arXiv:2408.08152. Yang,K.;Swope,A.M.;Gu,A.;Chalamala,R.;Song,P.;Yu, S.; Godil, S.; Prenger, R.; and Anandkumar, A

    Pith/arXiv arXiv

  12. [2025]

    https://modelcontextprotocol.io/specification

    Model Context Protocol Specifica- tion. https://modelcontextprotocol.io/specification. Revision 2025-11-25. de Moura, L.; and Ullrich, S

    2025

  13. [2026]

    An, C.; Ye, Q.; Pan, M.; and Zhang, J

    Semantic Search over 9 Million Mathematical Theorems.arXiv preprint arXiv:2602.05216. An, C.; Ye, Q.; Pan, M.; and Zhang, J

    arXiv