Pith. sign in

REVIEW 3 major objections 7 minor 16 references

Four machine-checkable move certificates collapse the MS(3) length-14 cases onto AK(3) and link the remaining open pairs.

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 ↗

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.

T0 review reviewed 2026-07-30 challenge →

load-bearing objection 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. the 3 major comments →

arxiv 2607.23611 v1 pith:A2FCSNN7 submitted 2026-07-26 math.GR

Machine-checkable equivalence certificates at the length-14 Andrews-Curtis frontier

Josep Carreras This is my paper
classification math.GR MSC 20F0520-0857M05
keywords Andrews-Curtis conjectureAkbulut-Kirby presentationMiller-Schupp presentationsAC-equivalence certificatesbalanced presentationstrivial groupsubstitution-move graphmachine-checkable proofs
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 reading

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.

Core claim

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.

What carries the argument

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.

Load-bearing premise

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.

What would settle it

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.

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

If this is right

  • 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.

Where Pith is reading between the lines

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

  • 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.
Share X Bluesky LinkedIn Reddit HN

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

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.

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 (3)
  1. [§1 / Corollary 5] §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.
  2. [§2 / §8] §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
  3. [§5, Theorem 6] §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什么
minor comments (7)
  1. [§6] §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.
  2. [§3, verification table] §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.
  3. [§2] §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).
  4. [§3–§6] Numbering: the σ-realization corollary after Theorem 4 is unnumbered while Corollaries 5 and 7 are numbered; make the numbering consistent.
  5. [Corollary 5] 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.
  6. [§1 / §3] 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.
  7. [§8] §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.

Circularity Check

0 steps flagged

No significant circularity: AC-equivalences rest on independently replayable move ledgers, not on fitted inputs or self-justifying definitions.

full rationale

The load-bearing claims (Theorems 1–4) are elementary-move certificates checked by a dependency-free verifier that re-derives every inversion, multiplication, conjugation, and packaged rotation in integer arithmetic and explicitly tests terminal-state membership in the Σ-orbit of the named target. Search provenance is irrelevant to acceptance; the paper states a certificate-first discipline and ships hashes plus one-command replay. Theorem 6’s GS bottleneck figures are regenerated from committed run records by a validation script and are carefully scoped as engine-relative statements about the canonical substitution graph, not smuggled AC-distance claims. Corollary 5 is explicitly conditional on two uncertified external claims. The Two-Hump table reverse-engineering and AC-19 audit are gated by hard assertions against third-party data and do not feed back into the equivalence proofs. There are no fitted parameters renamed as predictions, no uniqueness theorem imported from overlapping authors, and no definitional loop between inputs and claimed outputs. The derivation chain is self-contained and externally checkable.

Axiom & Free-Parameter Ledger

0 free parameters · 6 axioms · 2 invented entities

The paper works entirely inside the standard Andrews–Curtis rewrite system on balanced presentations of the trivial group. No numerical parameters are fitted. Background results (Miasnikov–Myasnikov length-12 theorem, Havas–Ramsay length-13 reduction to AK(3), Panteleev–Ushakov Aut(F2) realization on AK(n), Borovik–Lubotzky–Myasnikov finitary components) are cited as established domain facts. The only paper-specific modeling choices are the packaged-move accounting and the restriction of the exhaustive search to the canonical GS-substitution graph of Fagan et al.

axioms (6)
  • domain assumption Elementary AC moves (inversion, multiplication by another relator or its inverse, conjugation) generate the Andrews–Curtis equivalence relation on balanced presentations.
    Standard definition of the AC conjecture since Andrews–Curtis 1965; used throughout §§2–4 as the meaning of ~_AC.
  • domain assumption The symmetry group Σ generated by relator swap, inversion, and cyclic rotation consists entirely of AC-realizable operations (swap via a fixed 6-move identity).
    Stated in §2 Orbit convention; certificates are allowed to land in Σ·target rather than exact target.
  • domain assumption Every balanced two-generator trivial presentation of total length ≤12 is AC-trivializable (Miasnikov–Myasnikov); at length 13 every such presentation is AC-trivializable or AC-equivalent to AK(3) (Havas–Ramsay).
    Cited frontier facts that locate the paper’s length-14 contribution; Introduction.
  • standard math Left rotation of a cyclically reduced relator equals conjugation by the inverse of the rotated prefix, so packaged rotations are faithful AC moves.
    §2 elementary identity used to justify counting rotations as single packaged moves while still reporting classical single-generator conjugation cost.
  • ad hoc to paper The canonical GS-substitution graph (vertices = Σ-canonical cyclically reduced pairs; edges = cyclically aligned products with cancelling junction) is the search space for the bottleneck analysis.
    Inherited from Fagan et al. [5] and adopted in §5; Theorem 6 bounds are explicitly engine-relative to this graph, not elementary AC distance.
  • domain assumption Unimodular exponent matrices place all six benchmark presentations and AK(3) in the generating component of every finite quotient (Borovik–Lubotzky–Myasnikov), so finite quotients cannot separate them.
    Invoked in §7 to explain why the computational finite-group sieve is only illustrative.
invented entities (2)
  • Packaged-move accounting (rotation-by-k counted as one move; classical cost = min(k,L-k) single-generator conjugations at move-time length) independent evidence
    purpose: Compress certificates and report both human-readable and classical lengths consistently.
    Defined in §2; verifier tracks state lengths so classical counts are not computed against initial lengths. Not a physical entity; a bookkeeping convention with a regression test.
  • σ-merge program of 214 cross-label pairs from the Two-Hump 261-class table no independent evidence
    purpose: Turn the public classification table into an explicit list of candidate AC class mergers under the automorphism σ.
    Derived in §6 by pairing the 550 unsolved presentations under σ and counting cross-boundary pairs; conditional Corollary 7 follows if all 214 are AC-realized.

reviewed 2026-07-30 · how reviews work

0 comments
Cite this review

Pith. "Pith review of Machine-checkable equivalence certificates at the length-14 Andrews-Curtis frontier." pith.science (2026). https://pith.science/paper/A2FCSNN7

@misc{pith2026260723611,
  author       = {Pith},
  title        = {Pith review of: Machine-checkable equivalence certificates at the length-14 Andrews-Curtis frontier},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/A2FCSNN7}},
  note         = {Machine review of arXiv:2607.23611}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

In rank 2, unconditional verification of the Andrews-Curtis conjecture stands at total relator length 12; at length 13 every balanced trivial-group presentation is AC-trivializable or AC-equivalent to the Akbulut-Kirby presentation AK(3), itself open. At length 14, Shehper et al. reduced the Miller-Schupp family to six hard presentations: four stated AC-equivalent to AK(3) with no published move sequences, and two unresolved. We prove four explicit AC-equivalences among these six as machine-checkable elementary-move certificates, replayable in under a second by a small dependency-free verifier: the classical candidate <x,y | x^-1 y^2 x = y^3, y^-1 x^2 y = x^3> (= MS(2, x^-2 y^-1 x^2 y) up to rotation) is equivalent to the unresolved MS(2, y x^2 y^-1 x^-2) (36 moves); MS(2, y x^2 y x^-2) to MS(2, x^-2 y^-1 x^2 y^-1) (85 moves); and MS(3, y x^2 y) and MS(3, y^-1 x^2 y^-1) each to AK(3) (66 and 13 moves). The latter two are, to our knowledge, the first public explicit certificates for any of the four AK(3)-equivalences asserted without proof by Shehper et al., making the MS(3) branch of the length-14 collapse unconditional. The first two realize the automorphism sigma: x -> x, y -> y^-1 on the remaining open classes. We complement the certificates with a computer-assisted exhaustive minimax analysis of the substitution-move graph: the bottleneck distance from MS(3, y x^2 y) to AK(3) is exactly 19, while any such path from either MS(2) representative to AK(3), or between them, must reach total length at least 27. We further analyze the public classification table of the "Two-Hump" campaign, derive a 214-pair class-merger program, and commit an AC-19 membership audit. All certificates, search engines, verifier, and one-command reproduction are archived.

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

16 extracted references · 5 canonical work pages

  1. [1]

    J. J. Andrews, M. L. Curtis,Free groups and handlebodies, Proc. Amer. Math. Soc.16(2) (1965), 192–195. doi:10.1090/S0002-9939-1965-0173241-8

    work page doi:10.1090/s0002-9939-1965-0173241-8 1965

  2. [2]

    Akbulut, R

    S. Akbulut, R. Kirby,A potential smooth counterexample in dimension 4 to the Poincar´ e conjecture, the Schoenflies conjecture, and the Andrews–Curtis conjecture, Topology24(4) (1985), 375–390. doi:10.1016/0040-9383(85)90010-2 9

    work page doi:10.1016/0040-9383(85)90010-2 1985

  3. [3]

    Borovik, A

    A. Borovik, A. Lubotzky, A. Myasnikov,The finitary Andrews–Curtis conjecture, arXiv:1103.1295

    Pith/arXiv arXiv

  4. [4]

    R. G. Burns, O. Macedo´ nska,Balanced presentations of the trivial group, Bull. London Math. Soc.25(6) (1993), 513–526. doi:10.1112/blms/25.6.513

    work page doi:10.1112/blms/25.6.513 1993

  5. [5]

    Fagan, M

    L. Fagan, M. Tarquini, A. Shehper, M. Manko, A. Gruen, C. Huang, G. Butbaia, D. Passaro, S. Gukov,The Two-Hump Problem: Bridging the Difficulty Gap in Mathematical Reinforcement Learning, ICML 2026, arXiv:2606.21611

    Pith/arXiv arXiv 2026

  6. [6]

    Havas, C

    G. Havas, C. Ramsay,Breadth-first search and the Andrews-Curtis conjecture, Internat. J. Algebra Comput.13(1) (2003), 61–68. doi:10.1142/S0218196703001365

    work page doi:10.1142/s0218196703001365 2003

  7. [7]

    D. L. Johnson,Topics in the Theory of Group Presentations, London Math. Soc. Lecture Note Ser. 42, Cambridge Univ. Press, 1980

    1980

  8. [8]

    Lisitsa,The Andrews–Curtis conjecture, term rewriting and first-order proofs, ICMS 2018, LNCS 10931, Springer, 343–351

    A. Lisitsa,The Andrews–Curtis conjecture, term rewriting and first-order proofs, ICMS 2018, LNCS 10931, Springer, 343–351. doi:10.1007/978-3-319-96418-8 41

    doi:10.1007/978-3-319-96418-8 2018

  9. [9]

    Lisitsa,New Andrews–Curtis trivializations for Miller–Schupp group presentations, Ex- amples and Counterexamples6(2024), 100168

    A. Lisitsa,New Andrews–Curtis trivializations for Miller–Schupp group presentations, Ex- amples and Counterexamples6(2024), 100168. doi:10.1016/j.exco.2024.100168

    arXiv 2024

  10. [10]

    Lisitsa,Stable Andrews-Curtis trivialization of AK(3) revisited

    A. Lisitsa,Stable Andrews-Curtis trivialization of AK(3) revisited. A case study using automated deduction, J. Computational Algebra16(2025), 100041. doi:10.1016/j.jaca.2025.100041 (arXiv:2501.18601)

    arXiv 2025

  11. [11]

    A. D. Miasnikov, A. G. Myasnikov,Balanced presentations of the trivial group on two generators and the Andrews-Curtis conjecture, arXiv:math/0304305

    Pith/arXiv arXiv

  12. [12]

    C. F. Miller III, P. E. Schupp,Some presentations of the trivial group, in Groups, Languages and Geometry, Contemp. Math. 250, Amer. Math. Soc., 1999, 113–115. doi:10.1090/conm/250/03848

    work page doi:10.1090/conm/250/03848 1999

  13. [13]

    Panteleev, A

    D. Panteleev, A. Ushakov,Conjugacy search problem and the Andrews–Curtis conjecture, arXiv:1609.00325

    Pith/arXiv arXiv

  14. [14]

    Schulz, S

    S. Schulz, S. Cruanes, P. Vukmirovi´ c,Faster, Higher, Stronger: E 2.3, CADE-27, LNCS 11716, Springer, 2019, 495–507. doi:10.1007/978-3-030-29436-6 29

    doi:10.1007/978-3-030-29436-6 2019

  15. [15]

    Shehper, A

    A. Shehper, A. Medina-Mardones, L. Fagan, B. Lewandowski, A. Gruen, Y. Qiu, P. Kucharski, Z. Wang, S. Gukov,What makes math problems hard for reinforcement learning: a case study, arXiv:2408.15332

    Pith/arXiv arXiv

  16. [16]

    McCune,Prover9 and Mace4,http://www.cs.unm.edu/ ~mccune/prover9/, 2005– 2010

    W. McCune,Prover9 and Mace4,http://www.cs.unm.edu/ ~mccune/prover9/, 2005– 2010. 10

    2005

This paper was first reviewed by grok-4.5 on July 30, 2026.