{"id":"6327f8dc-e514-494b-ba5d-749e0603ce68","arxiv_id":"2607.27705","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":4,"one_line_summary":"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.","lead":"Albilich is a software system that keeps an LLM's long math proof attempts in a database, adds computer-algebra tools, and uses separate agents to steer and check the work. The authors report it solved all ten RealMath problems and two open group-theory questions, but code, proofs, and independent verification are not yet public.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Headline 'solved/counterexample/proof' claims rest solely on Albilich's internal LLM verifier, which checks CAS transcripts without re-execution and has no formal backend; no proof texts or artifacts are supplied.","rationale":"The concern is load-bearing because all headline claims pass through an internal LLM-based verifier with no external check and no supplied proof artifacts. Even if the architecture is coherent and potentially useful, the empirical claims cannot be accepted as research-level solutions without independent audit. The reader's weakest assumption correctly identifies this gap. The engineering contributions (SQLite proof state, role separation, MCP tool calls) are clearly described, but they do not establish the mathematical results. Verdict remains REJECT; it could become conditional if artifacts were released and independently verified.","tokens_in":9746,"tokens_out":2865,"duration_ms":31195,"concrete_test":"Obtain from the authors (or from the released repository) the archived proof dossiers, CAS transcripts, and integration reports for Problems 21.142 and 20.2. Independently re-execute every CAS script under the recorded backend versions, and formalize the two proof routes in Lean 4 or Isabelle/HOL, or obtain signed expert attestations with the full proof texts. If any CAS output cannot be reproduced, or any step fails formalization, the solved/counterexample statuses are unsupported. Additionally, rerun RealMath without CAS and grade all ten outputs against the reference equivalence, resolving Problem 08.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central results — 10/10 on RealMath, the counterexample to Problem 21.142, and the proof of a strengthening of Problem 20.2 — are accepted by an internal 'strict verifier' that is an LLM role checking bounded dossiers. The CAS artifacts are not re-executed: 'The strict verifier reads that artifact and does not re-execute the computation.' Formal verification is explicitly deferred: 'Internal informal verification remains distinct from formal verification, independent peer review, and external benchmark grading.' Since this verifier is the only acceptance authority, any LLM hallucination in verification or in a fabricated CAS transcript propagates into the solved status. The RealMath 10/10 is further undercut by the unresolved equivalence for Problem 08, and the advertised 9/10 without CAS is not reported in any experiment table. For the Kourovka problems, no full proof texts, CAS logs, or external expert reports are included — only internal statuses ('exact solution,' 'explicit witness'). The introduction claims 'We have used Albilich to resolve two problems in group theory, verified by human experts,' but provides no names, dates, or attestations. Therefore the abstract's mathematical successes are currently not independently auditable.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":10031,"tokens_out":7174,"duration_ms":80873,"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":[{"comment":"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.","section":"Verification and Integration; Limitations"},{"comment":"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.","section":"RealMath Benchmark; Table 3"},{"comment":"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.","section":"Introduction; Case Studies"}],"minor_comments":[{"comment":"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.","section":"Abstract; Experiments"},{"comment":"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.","section":"Case Studies: Open Problems in Group Theory"},{"comment":"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.","section":"Case Studies: Open Problems in Group Theory"},{"comment":"Reference formatting is inconsistent: several entries (e.g., QED, Danus, TheoremSearch) lack arXiv identifiers or complete venue information. The acknowledgements section also misspells 'Acknowledgements.'","section":"References"}],"recommendation":"reject","confidential_remarks":"The paper contains useful system-design ideas and the ablations are thoughtfully scoped, but the headline mathematical achievements are not independently verifiable from the manuscript. The self-referential acceptance loop and the explicit decision not to re-execute CAS artifacts mean the 'solved' and 'proof' claims rest entirely on the system's internal verifier. I would not rule out a future version that supplies proof artifacts, CAS logs, external expert confirmation, and an honest revision of the abstract; without those, the central claims cannot be accepted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Let me give you the short version. Albilich is a proof-state orchestration system for LLM-based math research. The architecture is genuinely new in its combination: persistent SQLite proof state, explicit debt ledger, role-authorized patches, separation of local verification from root integration, reconciliation when dependencies change, and a PhD-advisor role that redirects strategy. The paper describes these mechanisms clearly enough that someone could build on them. That is the real contribution.\n\nWhat the paper does less well is quantify success. The abstract claims 10/10 on RealMath with CAS and 9/10 without, but the no-CAS result appears in no table. The 10/10 is undercut by the paper's own statement that Problem 08's equivalence with the reference remained unresolved. The two Kourovka results---a counterexample to 21.142 and a witness for 20.2---are asserted without proof texts, CAS logs, artifacts, or named human verifiers, despite the introduction claiming human verification. Internal 'solved_final' status depends on an LLM strict verifier that reads CAS transcripts without re-executing them and has no formal backend. The limitations section says exactly that, so the paper is honest about its own epistemic limits, but that honesty does not make the headline claims auditable.\n\nThe ablations are honestly framed. The CAS ablation is a paired one-hour run showing 32% token reduction but solving nothing. The advisor ablation stopped the advisor-off arm before its full allowance, so it only shows that arm had not solved by stopping point, not that it could not have. The paper says this explicitly. The engineering ideas are coherent, the narrative is readable, and the citations to related systems are fair. But the central mathematical claims are load-bearing and unverifiable from the manuscript.\n\nMy recommendation: send this to peer review, but as a systems paper, not as a paper establishing the open-problem resolutions. The referee should demand external verification or full artifacts for the Kourovka claims, a corrected RealMath count, and a table for the no-CAS condition. With those, this could be a strong contribution to the agentic-math-systems literature. Worth citing for the architecture; worth discussing in reading group as a cautionary example of the gap between system design and verified results.","headline":"Genuinely interesting proof-state orchestration system, but the headline mathematical results are not externally auditable; treat as a system paper, not a results paper.","tokens_in":735,"tokens_out":1460,"would_cite":true,"duration_ms":30464,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Albilich, a multi-agent proof-state harness with computer-algebra support, reports completing research-level math problems and refuting an open group-theory question.","keywords":["agentic AI","mathematical research","proof state","computer algebra systems","large language models","informal verification","finite group theory","test-time scaling"],"falsifier":"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.","tokens_in":9609,"feed_emoji":"🧮","tokens_out":11351,"duration_ms":104573,"temperature":0.7,"pith_summary":"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.","feed_headline":"AI with persistent proof memory refutes open group-theory problem","feed_subtitle":"The harness also solved 10 of 10 benchmark problems and cut token use by 32 percent when computation tools were enabled.","key_machinery":"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","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["AI refutes open group-theory problem using proof-memory orchestration","LLM+CAS harness aces math benchmark, solves open problem","CAS cuts AI math token use 32% while solving open problems","Proof-state database lets LLM steer long mathematical proofs","AI counterexample settles open problem in group theory"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["AI refutes open group-theory problem using proof-memory orchestration","LLM+CAS harness aces math benchmark, solves open problem","CAS cuts AI math token use 32% while solving open problems","Proof-state database lets LLM steer long mathematical proofs","AI counterexample settles open problem in group theory"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000839,"raw_usage":{"total_tokens":3496,"prompt_tokens":749,"completion_tokens":2747,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":493,"completion_tokens_details":{"reasoning_tokens":2662}},"tokens_in":493,"tokens_out":2747,"duration_ms":20211,"temperature":1.0,"reasoning_tokens":2662,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T02:56:38.679118+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}