{"id":"25ac1daf-8fc1-49ea-b71b-3859c52ca71a","arxiv_id":"2607.23611","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Explicit elementary-move certificates prove two MS(3) presentations AC-equivalent to AK(3) and realize the automorphism σ on the two remaining open MS(2) classes at length 14.","lead":"Four machine-checkable move certificates prove Andrews–Curtis equivalences among the six hardest length-14 Miller–Schupp presentations, including both MS(3) cases to AK(3). This makes half the length-14 collapse unconditional and ships a one-second verifier plus full archive.","discovery_kind":"extension","skeptic_critique":{"model":"moonshotai/kimi-k3","headline":"No significant objection identified. The strongest claim (Theorems 3–4 as machine-replayable AC-equivalence certificates attaching the MS(3) branch to AK(3)) rests on exactly the kind of evidence that is independently checkable, and the paper's move semantics reduce correctly to classical Andrews–C\n","rationale":"The reader correctly located the one material caveat (Theorem 6's engine-relative exhaustions) and correctly judged it scoped and non-load-bearing for the strongest claim. My independent pass over the certificate logic found the move semantics, orbit convention, and equivalence direction all sound as stated; the packaged-rotation accounting issue was already found and fixed by the authors' own adversarial process, which is evidence of functioning self-verification rather than of remaining risk. The only thing standing between the paper and full third-party certainty is independent (not same-code) replay, and the concrete test above does that at trivial cost. I therefore see no basis to move the verdict off ACCEPT; the claim \"first public certificates, MS(3) branch unconditional\" survives scrutiny, with the novelty qualifier (\"public,\" audit-scoped, and explicitly hedged against [5]'s unpublished computations) appropriately stated by the paper itself.","tokens_in":10994,"tokens_out":2314,"duration_ms":54499,"concrete_test":"Write an independent ~150-line verifier (fresh code, not importing ac_verify.py): parse cert_ms3_yinvx2yinv_equiv_ak3.json (13 moves) and bottleneck_ak_f3_cert.json (66 moves), implement free reduction, the three classical AC moves plus rotation-as-conjugation, apply the ledgers step by step, and enumerate Σ·AK(3) / Σ·MS(3,yx²y) (2·2·2·L₁·L₂ orbit members) to confirm the terminal state lies in the target orbit. If both ledgers replay under independent move semantics, condition (iii) — the only load-bearing element of the strongest claim — is settled affirmatively.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I stress-tested the strongest claim in good faith: for \"MS(3) branch collapse unconditional\" to hold, three conditions must be true: (i) the verifier's move set (inversion, multiplication, single-generator conjugation, packaged cyclic rotation) generates only genuine AC moves; (ii) the Σ-orbit convention (swap, inversion, rotation) is AC-realizable, so equivalence-to-orbit-member is genuine AC-equivalence; (iii) the ledgers actually replay. On (i): packaged rotation of a cyclically reduced relator r=uv by k equals conjugation by u^{-1}, which is a legal classical AC conjugation move (and the classical accounting, min(k, L-k) generator conjugations against move-time lengths, is conservative — classical AC allows conjugation by arbitrary w as one move). The paper itself documents that an accounting error here was caught in adversarial review and pinned by a regression test. On (ii): swap is realized by a standard elementary identity, inversion and rotation are moves; the verifier checks orbit membership explicitly rather than asserting it. On (iii): this is the only genuinely load-bearing element, and the entire architecture (dependency-free verifier, hashes, one-command repro, a second independent certificate for Theorem 3) is built to make it checkable by third parties rather than trusted. The residual risk is a subtle verifier bug (e.g., in free reduction or orbit generation) that no amount of re-running the same code would detect — but that risk is addressable by an independent re-implementation, which is cheap. The Theorem 6 exhaustion caveat the reader flags is real but scoped by the paper itself and does not bear on the strongest claim. I find no internal inconsistency and no hidden assumption in the equivalence direction (moves are reversible, so AK(3)→Σ·MS(3) certifies the stated equivalence).","agreement_with_reader":"agree"},"referee_report":{"model":"moonshotai/kimi-k3","summary":"The manuscript studies six length-14 Miller–Schupp presentations left hard by the reinforcement-learning campaign of Shehper et al. [15]. It proves four explicit AC-equivalences — Theorems 1–2 realizing the automorphism σ: y ↦ y⁻¹ on the two open MS(2) classes, and Theorems 3–4 attaching MS(3, yx²y) and MS(3, y⁻¹x²y⁻¹) to AK(3) — each witnessed by a JSON move-ledger replayable in under a second by a small dependency-free verifier that re-derives every elementary move and checks membership in the Σ-orbit of the target explicitly. Theorems 3–4 are the first public certificates for any of the four AK(3)-equivalences asserted without proof in [15], reducing the conditional length-14 collapse to the two remaining MS(2) claims (Corollary 5). The paper adds a computer-assisted exhaustive minimax analysis of the canonical GS-substitution graph (Theorem 6: d_GS = 19 exactly for the MS(3)–AK(3) pair; lower bound 27 for the searched MS(2) representatives, over 6.2M and 13.5M exhausted canonical states), a reverse-engineering analysis of the Two-Hump classification table with a 214-pair σ-merge program, negative results on saturation provers (including a genuinely useful Prover9 auto-denials pitfall), and a fully archived reproduction package including quarantined invalidated artifacts and a claims ledger.","tokens_in":11312,"tokens_out":3403,"duration_ms":100663,"significance":"If the certificates replay as claimed, this is a solid contribution at the current AC frontier: it converts two asserted-but-unwitnessed equivalences from [15] into independently checkable objects, and it certifies the σ-realization on the two remaining open classes with explicit elementary witnesses — the frontier analogue of Panteleev–Ushakov. The methodological standard is unusually high for this area: certificate-first verifier discipline, dual packaged/classical move accounting with a regression test pinning an accounting error caught in adversarial review, a second independently found certificate for Theorem 3, explicit scoping of Theorem 6 as engine-relative (with the correct observation that AC-equivalence does not transfer d_GS bounds), retention of invalidated artifacts, and one-command reproduction with pinned hashes. Theorem 6's quantified easy/hard asymmetry (19 vs ≥27) is a genuine structural datum about the benchmark, honestly fenced off from any AC-distance claim. The §6 novelty discussion is commendably candid: the authors themselves present evidence that stronger unpublished computations likely exist, and claim public replayability rather than priority.","major_comments":[{"comment":"§1, Abstract, and Corollary 5: the headline framing that Theorems 3–4 'render the MS(3) branch of the length-14 collapse unconditional' depends on the identification of the six hard presentations of [15, §3.3]. The manuscript states that this identification — in particular that the repeated MS(3) signs are correlated — 'follows from the paper's count together with its released benchmark data' rather than from an explicit list in [15]. Since this interpretive step is load-bearing for which claims Theorems 3–4 actually settle, the derivation should be shipped with the same rigor as the rest of the paper: a committed script with hard assertion gates reproducing the six-case list from the released benchmark data, and a one-line caveat at each place the 'unconditional' language appears (Abstract, §1, Corollary 5) noting the dependency on that identification.","section":"§1 / Corollary 5"},{"comment":"§2 (Certificates and verifier) and §8: every positive claim in the paper rests on a single-author verifier (ac_verify.py). The certificate-first discipline, self-tests, and regression pins are good practice, but they guard against ledger corruption and accounting drift, not against a specification-level bug in free reduction or Σ-orbit generation — the two routines whose correctness defines what is being certified. Two concrete, cheap strengthenings would materially raise confidence: (i) an independent replay of the four certificates in an established system (e.g., GAP), checking that each consecutive state pair differs by a stated elementary move and that the terminal state lies in Σ·target; (ii) property-based pinning of the orbit generator — e.g., asserting |Σ·Q| exactly against a brute-force enumeration for the certificate targets, and cross-checking free reduction against a second-t","section":"§2 / §8"},{"comment":"§5, Theorem 6: the d_GS ≥ 27 lower bounds rest on completeness of the bidirectional bottleneck-Dijkstra and on the canonicalizer/GS-move-generator emitting exactly the intended graph. The Python and C++ engines are described as a port pair, and the independent re-derivation at cap 25 explicitly shares the move generator, so bit-for-bit agreement does not exclude a shared specification error. The manuscript's scoping ('computer-assisted; engine-relative') is honest and appropriate, but one additional gate would help: validate the generator/canonicalizer against [5]'s published engine (or its released artifacts) on an overlapping family of states — the §7 cross-validation of Two-Hump greedy solutions at the elementary level shows the pipeline can interoperate, so an analogous generator-level agreement check on a sample should be feasible. Failing that, a short paragraph stating precisely什么","section":"§5, Theorem 6"}],"minor_comments":[{"comment":"§6: the inference that the Two-Hump table 'most plausibly' records unpublished computed connections is reasonable (the 354/550 shorter-label fingerprint and class 142 containing three H2-keys are suggestive), but alternatives such as a canonicalization involving length-reducing moves are not explicitly excluded. Consider tempering 'strong evidence' to 'evidence consistent with' and listing the excluded alternatives with the tests that exclude them.","section":"§6"},{"comment":"§3 table and verification table: the move-count column mixes conventions — entries read '36 (58)', i.e., packaged with classical in parentheses — but the column header says only 'Moves'. Label the columns explicitly (packaged / classical), as the distinction matters for comparison with classical AC literature.","section":"§3, verification table"},{"comment":"§2: 'elementary peak total length' (used in all four theorem statements) is never formally defined; define it as max over elementary states of |r1| + |r2| along the expanded ledger, and note it can differ from the GS-path bottleneck (as the manuscript itself observes for the 66-move certificate).","section":"§2"},{"comment":"Numbering: the σ-realization corollary after Theorem 4 is unnumbered while Corollaries 5 and 7 are numbered; make the numbering consistent.","section":"§3–§6"},{"comment":"Corollary 5: it would help the reader to state explicitly that the classical Solitar candidate P1 remains uncertified relative to AK(3) — Theorem 1 certifies P1 ∼ P6, not P1 ∼ AK(3). This is implicit but easy to misread from the table.","section":"Corollary 5"},{"comment":"The P1 notation is used both for Johnson's 1980 presentation and for MS(2, x⁻²y⁻¹x²y) 'up to rotation of its second relator'; the rotation identification is correct (y⁻¹x²yx⁻³ is a cyclic rotation of x⁻³y⁻¹x²y after inversion convention check — worth one line of detail) and should be verified by the verifier as an orbit-membership assertion rather than asserted in prose.","section":"§1 / §3"},{"comment":"§8: the reproduction banner's 'PARTIAL' behavior for third-party-dependent analyses is good practice; please also state the expected wall-clock and memory for the cap-26/27 validation re-runs so referees know what reproduction of Theorem 6's run-record checks entails versus the sub-second certificate replays.","section":"§8"}],"recommendation":"minor_revision","confidential_remarks":"The central results are machine-checkable certificates and the architecture is genuinely designed for third-party verification rather than trust; I have no correctness doubt about Theorems 1–4 conditional on the verifier being sound, which is itself auditable in an afternoon. My three major comments ask for verification-strengthening and framing precision, not new mathematics. The §6 reverse-engineering section flirts with claims about another group's unpublished computations; the authors handle it more candidly than most, but the editor may want to ensure the 'strong evidence of unpublished AC-connections' language is defensible if [5]'s authors are asked to comment. The AI-assistance disclosure is explicit and the claims-ledger practice (documenting retracted intermediate claims) is exemplary; nothing in the manuscript suggests undisclosed provenance issues."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The one thing worth knowing: this paper ships four machine-replayable elementary-move certificates at the length-14 AC frontier, two of which attach both MS(3) presentations to AK(3) and thereby make that branch of Shehper et al.’s collapse unconditional. The other two realize σ on the remaining open MS(2) classes. That is real progress on a named benchmark where the prior claims had no public move sequences.\n\nWhat is new is not the assertion that some of these are equivalent to AK(3)—Shehper et al. already said four of them were—but the first public elementary witnesses, plus the exact GS bottleneck 19 for MS(3)→AK(3) and the ≥27 lower bounds for the MS(2) side. The reproducibility setup is unusually clean for this area: dependency-free verifier written certificate-first, dual Python/C++ engines with regression gates, hashed MANIFEST, Zenodo DOI, one-command repro. Classical vs packaged accounting was caught and pinned after adversarial review. Two independent certificates exist for the harder MS(3) case. Circularity burden is near zero because the verifier re-derives every move and checks orbit membership explicitly.\n\nSoft spots, in proportion: Theorem 6’s multi-million-state exhaustions are engine-relative, not a formal graph proof. The paper scopes this correctly and does not smuggle it into the equivalence claims. The Two-Hump reverse-engineering and 214-pair σ-merge program are useful bookkeeping, not load-bearing. Residual risk is a subtle verifier bug in free reduction or orbit generation; that is addressable by independent re-implementation and is the right residual risk for this kind of work, not a hidden flaw.\n\nThis is for people who track the AC frontier, Miller–Schupp presentations, or computer-assisted combinatorial group theory. It will not resolve AK(3), and it does not claim to. Citation pattern and literature engagement look honest. I would send it to peer review without hesitation; the central theorems are supported as stated. Engage with the certificates and the bottleneck numbers; treat the GS lower bounds as strong computational evidence inside the stated generator, not as AC-distance theorems.","headline":"Solid, checkable certificates that finally make the MS(3) half of the length-14 benchmark unconditional; the remaining soft spot is only the engine-scoped GS lower bounds, which the paper already flags.","tokens_in":12826,"tokens_out":559,"would_cite":true,"duration_ms":15723,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["20F05","20-08","57M05"],"pacs":[],"model":"grok-4.5","headline":"Four machine-checkable move certificates collapse the MS(3) length-14 cases onto AK(3) and link the remaining open pairs.","keywords":["Andrews-Curtis conjecture","Akbulut-Kirby presentation","Miller-Schupp presentations","AC-equivalence certificates","balanced presentations","trivial group","substitution-move graph","machine-checkable proofs"],"falsifier":"Replay the four archived certificate files with the independent verifier; any ledger that fails to reach the claimed target orbit falsifies the corresponding equivalence. Separately, exhibiting a substitution-graph path of bottleneck below 19 (MS(3) to AK(3)) or below 27 (MS(2) pairs) would falsify the minimax claims.","tokens_in":12487,"feed_emoji":"🔗","tokens_out":1039,"duration_ms":36391,"temperature":0.7,"pith_summary":"The Andrews–Curtis conjecture asks whether every balanced presentation of the trivial group can be reduced to the standard one by elementary moves on the relators. Unconditional verification is known only up to total relator length 12; at length 13 everything reduces to the still-open Akbulut–Kirby presentation AK(3). At length 14, six hard Miller–Schupp presentations had resisted prior search, four of them asserted equivalent to AK(3) with no published move sequences. This paper supplies four explicit elementary-move certificates, each replayable in under a second by a small independent verifier: two connect the MS(3) presentations directly to AK(3), and two realize the automorphism that swaps y with y-inverse on the remaining open classes. The MS(3) branch of the length-14 collapse is thereby made unconditional, so the named six-case benchmark now hinges on exactly two still-uncertified claims.","feed_headline":"Certificates collapse two hard AC cases onto AK(3)","feed_subtitle":"First public move ledgers make the MS(3) length-14 branch unconditional; two holdouts remain","key_machinery":"Machine-checkable elementary-move certificates: JSON ledgers of inversions, multiplications, single-generator conjugations and cyclic rotations, checked by a dependency-free verifier that re-derives every step in exact arithmetic and confirms the terminal state lies in the AC-realizable symmetry orbit of the target.","core_discovery":"The paper proves four explicit AC-equivalences among the six hard length-14 Miller–Schupp presentations. MS(3, yx²y) and MS(3, y⁻¹x²y⁻¹) are each AC-equivalent to AK(3), witnessed by machine-checkable certificates of 66 and 13 packaged moves—the first public ledgers for any of the previously asserted AK(3) equivalences. Two further certificates show that the classical candidate P1 is equivalent to one holdout and that the other holdout is equivalent to its MS(2) partner, realizing the automorphism σ (y ↦ y⁻¹) on the open classes.","pith_inferences":["The eight-unit energy gap between the MS(3) and MS(2) substitution corridors suggests any future MS(2)→AK(3) certificate will pass through substantially longer intermediate presentations than the MS(3) routes.","Publishing the two missing MS(2)→AK(3) ledgers would finish the named six-case benchmark and leave AK(3) itself as the sole open obstruction in that family at lengths 13–14.","The reverse-engineered class table and σ-merge list give a finite, checkable agenda for reducing the unsolved length-≤19 pool by automorphism realization rather than fresh open-ended search."],"forward_implications":["The MS(3) branch of the length-14 Miller–Schupp collapse is now unconditional.","Full collapse of the six hard cases onto AK(3) depends on exactly two remaining uncertified claims.","The substitution-graph bottleneck from MS(3, yx²y) to AK(3) is exactly 19, while paths from the searched MS(2) representatives need total length at least 27.","A concrete 214-pair program exists for merging Two-Hump unsolved classes once the corresponding automorphisms are realized.","Every positive equivalence claim ships with one-command reproducible certificates, verifier, and membership audits."],"fun_headline_variants":["Four AC certificates collapse two MS(3) cases onto AK(3)","First public move ledgers equate MS(3) pair to AK(3)","Machine-checkable AC equivalences resolve length-14 MS(3) branch","Explicit certificates link two hard MS(3) presentations to AK(3)","AC-move ledgers make MS(3) length-14 collapse unconditional"],"cache_read_input_tokens":128,"weakest_assumption_plain":"The distance lower bounds rest on computer searches of millions of canonical states finding no connecting path below the stated energy, which assumes those searches completely enumerate the intended substitution graph.","fun_headline_variants_meta":{"raw":{"variants":["Four AC certificates collapse two MS(3) cases onto AK(3)","First public move ledgers equate MS(3) pair to AK(3)","Machine-checkable AC equivalences resolve length-14 MS(3) branch","Explicit certificates link two hard MS(3) presentations to AK(3)","AC-move ledgers make MS(3) length-14 collapse unconditional"]},"model":"grok-4.5","effort":"low","cost_usd":0.005098,"raw_usage":{"total_tokens":1602,"prompt_tokens":1074,"num_sources_used":0,"completion_tokens":87,"cost_in_usd_ticks":50984000,"prompt_tokens_details":{"text_tokens":1074,"audio_tokens":0,"image_tokens":0,"cached_tokens":128},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":441,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":1074,"tokens_out":87,"duration_ms":8491,"temperature":1.0,"reasoning_tokens":441,"cache_read_input_tokens":128,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-30T17:40:14.086305+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Replay the four archived certificate files with the independent verifier; any ledger that fails to reach the claimed target orbit falsifies the corresponding equivalence. Separately, exhibiting a substitution-graph path of bottleneck below 19 (MS(3) to AK(3)) or below 27 (MS(2) pairs) would falsify the minimax claims.","supporting_citations":[],"review_version":1}