The stable commutator length of a relator is not a one-relator group invariant
Let be sets and let , be relators with . Does this imply that ?
- Result
- Disproved(see note)
- Status
- Resolved
- AI contribution
- AI co-developed
- Method
- Computation
- Field
- Group theory, Geometric group theory
- Posed by
- Heuer and Löh
- Year posed
- 2019
- Years open
- 7y
- Solved
- 2026-08-21
- Model
- Claude Opus 5; Harmonic Aristotle (Lean formalisation)
- Vendor
- Anthropic; Harmonic
- Collaborators
- —
- Verification
- Unreviewed
- Publication
- Preprint
- Significance
- 18 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
A negative answer to Heuer and Löh's question: the isomorphism type of a one-relator group does not determine . The witnesses are and , both length 20 in , with but against .
The mechanism is what made the search finite: is an -invariant, so a pair in *different* orbits whose one-relator groups happen to be isomorphic has its two scl values unconstrained by each other. The search was for that configuration among words of length at most 20.
Scope: it settles the question as posed and nothing wider. It does not say which invariants do determine scl, and this is a single pair rather than a construction giving arbitrary gaps.
What the AI did
Two systems, and the paper is more specific in its body than in its formal statement. The AI use statement reads only: "Claude Desktop with Opus 5 assisted in designing and orchestrating the computational search for candidate counterexamples." Section 4 puts it more strongly: "Claude Desktop with Opus~5 designed and orchestrated an exhaustive search through -orbits of words of length at most 20." Candidates were then filtered by first homology of low-index subgroups, Alexander polynomials and homomorphism counts to small finite groups, with explicit isomorphisms constructed for those the invariants did not separate.
Co-developed rather than assisted on the strength of the second sentence: the author formulated the target - pairs in different -orbits whose one-relator groups are nonetheless isomorphic, which is exactly the configuration that leaves scl unconstrained - and the model designed and ran the search that found one.
A second system appears in the same paragraph and is recorded here because the submission omitted it: the Lean formalisation of the six identities "produced with the assistance of Harmonic's Aristotle". That is the artifact this entry's verification rests on.
Verification
Unreviewed, lowered from Lean-verified on inspection. A labelling correction, not a doubt about the mathematics.
The theorem has two halves - the groups are isomorphic, and the relators have different scl - and only the first is formalised. The Lean file says so itself: "(The paper computes scl r = 1 ≠ 1/2 = scl r' with scallop; see scl/.)" So the half that makes this a counterexample is a computation, not a machine-checked proof, and Lean-verified additionally requires the formal statement to be independently anchored, which an author's own repository is not.
What the Lean does establish, and it is not nothing: one file, 282 lines, with no sorry, no admit, no native_decide and no declared axiom. It builds the two homomorphisms explicitly and proves they compose to the identity in both directions, so the isomorphism is constructed rather than asserted. Not built here - no Lean toolchain on this machine, and it pins v4.28.0.
The scl values were not reproduced here either. They are reproducible in principle: scl/setup_scallop.sh fetches and patches Alden Walker's scallop, and compute_scl.py rechecks every value the paper quotes against it, exiting non-zero on disagreement. It needs a C++11 compiler with GLPK and GMP, none present on this machine.
Checked independently on 30 August 2026: both relators have exponent sum zero in both generators, so both do lie in as the question requires; both are cyclically reduced, length 20, distinct, and match the abstract exactly.
Sources
Submitted by CrimsonEgret515 on