Formalizing the Andrews-Curtis conjecture

The problem

I began working on the Andrews-Curtis conjecture through a collaboration with Sergei Gukov[1]. Sergei and his collaborators had been studying the conjecture as a test case for reinforcement learning. The rules and the goal are exact, but successful move sequences can be rare and very long.

Their paper, What makes math problems hard for reinforcement learning: a case study, asks why a problem with a small action space can still defeat search. An agent chooses from a finite set of moves, the words can grow without bound, and the standard terminal reward arrives only after a complete trivialization. The paper develops a topological measure of difficulty, proves length reducibility for all but two presentations in the Akbulut-Kirby series, and resolves several Miller-Schupp cases, including three infinite subfamilies[2].

I focused on the formalization because a search run produces a finite sequence of named moves. Lean can replay that sequence one move at a time. I wanted the formalization to cover the surrounding mathematics as well as individual certificates, including free words, presentations, rank-two computational moves, arbitrary-rank AC moves, stabilization, and the relations between those definitions.

This became a collaboration with Caroline Zhang, Aaron Zhao, Sergei, and Anima Anandkumar, and led to our NeurIPS MATH-AI 2025 paper, Mathematical Discovery and Formalization Towards the AC Conjecture[3]. Search methods proposed move sequences; Lean replayed each sequence against the precise move relation[4].

Groups and presentations

A group is a set of objects with a rule for combining them. There is an identity element \(e\), every element \(g\) has an inverse \(g^{-1}\), and parentheses do not change the result of repeated combinations. The integers form a familiar group under addition: \(0\) is the identity and \(-n\) is the inverse of \(n\).

In this problem, the elements are built from symbols called generators. The free group \(F(x,y)\) contains words made from \(x\), \(y\), \(x^{-1}\), and \(y^{-1}\), with only inverse cancellations such as \(xx^{-1}=e\). A group presentation adds further equations: \[ \langle x,y \mid r_1,r_2\rangle. \] The symbols before the bar are the generators. The words after the bar are relators, and each is declared equal to \(e\). For example, \(\langle x,y\mid xyx^{-1}y^{-1}\rangle\) imposes \(xyx^{-1}y^{-1}=e\), which is another way to say that \(x\) and \(y\) commute.

A presentation is balanced when it has the same number of generators and relators. The presentation \(\langle x,y\mid x,y\rangle\) describes the trivial group, the group containing only \(e\), because both generators are set equal to the identity.

The Andrews-Curtis question

The conjecture starts with a balanced presentation that already describes the trivial group. It asks whether its relators can always be transformed into the standard tuple \((x_1,\ldots,x_n)\) using three elementary operations: invert one relator, multiply one relator by another, or conjugate a relator. Andrews and Curtis posed the problem in 1965, and it remains open[5].

Most of our computations use two generators, so a search state is a pair \((r_1,r_2)\) of words in \(F(x,y)\). A solution is a finite list of AC moves ending at \((x,y)\). The search may use reinforcement learning, heuristics, or brute force; the final move list can be replayed independently as a certificate.

For a concrete example, the presentation \[ P_0=\langle x,y \mid xy,\;xyx^{-1}\rangle \] is AC-trivial in two moves: \[ \langle x,y \mid xy,\;xyx^{-1}\rangle \xrightarrow{\,r_2\leftarrow x^{-1}r_2x\,} \langle x,y \mid xy,\;y\rangle \xrightarrow{\,r_1\leftarrow r_1r_2^{-1}\,} \langle x,y \mid x,\;y\rangle. \] The two algebraic equalities behind the trace are \(x^{-1}(xyx^{-1})x=y\) and \((xy)y^{-1}=x\).

This tiny example has the same certificate shape as a larger search. The searcher emits two moves; Lean checks the conjugation, the cancellation, and the relation in which those moves are allowed. A trace in ACEquivalent proves an ACEquivalent statement. A trace in GeneralACEquivalent or one using stabilization proves a different statement.

The toy trace takes two moves. The conjecture asks whether every balanced presentation of the trivial group has some finite trace, even when the relators become much longer along the way. We can certify individual presentations, but the general statement remains open.

The distinction matters because knowing that a presentation defines the trivial group does not hand us an AC path. The group-theoretic fact is the hypothesis of the conjecture; the replayable move list is the missing certificate.

Why the search is difficult

Under the standard rank-two convention, an agent has twelve elementary moves at each state[6]. Relator lengths are unbounded, so those few actions generate an infinite state graph[2].

A naive search tree contains \(12^d\) move strings at depth \(d\). Some strings cancel, and many reach the same presentation, but the exponential growth appears before the algorithm has learned which branches are useful. Breadth-first search can certify a shortest path when it finishes; its memory requirements prevent it from scaling far[6][7].

The reward is sparse. A candidate path receives the decisive success signal when it reaches \((x,y)\), which may happen only after a long sequence of moves. Word length looks like an obvious intermediate score, but useful paths can make the relators longer before they simplify. Earlier empirical work found that several hand-designed measures provided little search guidance[7]. Shehper and collaborators frame this as a long-horizon problem with rare, high-reward trajectories[2].

Some constructed presentations require extremely many moves. Bridson constructed AC-trivializable presentations, beginning in rank four, for which the number of required AC moves grows faster than every fixed-height tower of exponentials in the presentation length[8]. Lishak constructed two-generator, two-relator presentations with the same tower-type growth for the number of relation applications needed to prove a generator trivial[9]. These are superexponential lower bounds for special constructed families, and Lishak's complexity measure is not itself an AC path length. A general search method therefore cannot assume that every AC-trivialization is short.

Formalization adds a separate constraint. The rank-two computational relation, the arbitrary-rank AC relation, and stable AC use different Lean types. A certificate checked in one relation crosses into another only through an explicit theorem. Harmonic helped us find one place where that theorem was missing; we added and proved it before treating the rank-two search output as a result in the arbitrary-rank relation.

What we formalized

Aaron Zhao and I started from the basic definitions. We first had to decide how Lean should represent a free-group word, a finite presentation, and one allowed AC move. On paper, we can write \(r_i\leftarrow r_i r_j\) and continue. In Lean, we have to specify the direction of multiplication, whether inverse multiplication is primitive, which conjugating words are allowed, and which relation closes those one-step moves under symmetry and transitivity. Those choices determine the theorem.

Aristotle was part of this process while the code was still changing[10]. Aaron and I would give it the current definitions and ask focused questions: does this constructor encode the move we intended, which imports does a proof really need, and does a small example elaborate under the same relation used by the search code? We checked its answers in Lean, revised the definitions, and repeated the process. Later, once the files had grown, we used the same workflow for a broader audit.

Together, we have now fully formalized the mathematical results in Sergei and his collaborators' paper, What makes math problems hard for reinforcement learning: a case study[2]. The repository includes the definitions, the relevant AC move systems, the Akbulut-Kirby and Miller-Schupp constructions, the knot-presentation results, and the certificate machinery connecting the mathematical statements to computation. We plan to release the full repository soon.

We represented a rank-\(N\) presentation as \(\mathrm{Presentation}(\mathrm{Fin}\,N)\). The type \(\mathrm{Fin}\,N\) supplies exactly \(N\) generator names, and each relator is an element of the corresponding free group. The rank therefore stays attached to the data instead of living in a comment or a file name.

-- Problems/Core/Presentation.lean
-- Think of this as the data object for a group presentation.
-- α is the type of generator names, and relations is the list of relators.
structure Presentation (α : Type*) where
  relations : List (FreeGroup α)
deriving DecidableEq

-- Balanced means: same number of generators and relators.
-- The bracketed arguments are Lean's way of saying "α is finite"
-- and "Lean can decide equality of free-group words when needed."
def balanced {α : Type*} [Fintype α] [DecidableEq (FreeGroup α)]
    (p : Presentation α) : Prop :=
  Fintype.card α = p.relations.length

The project keeps three relations visible. ACMove is the hand-written rank-two action space used by the search environment. GeneralACMove expresses ordinary AC operations at arbitrary finite rank. StableACMove also allows the rank to change by adding or removing a generator together with a relator that kills it.

Why stable AC?

Stabilization lets a proof leave rank \(n\), simplify at rank \(n+1\), and later remove the extra generator-relator pair. That freedom can make a presentation easier to manipulate, but it proves stable AC-equivalence rather than classical AC-equivalence. The certificate type records that difference instead of hiding it in the prose around the result.

-- This turns relators into the normal subgroup they generate.
-- In group-presentation language, this is "impose these relators."
def normalClosureAny {N : Nat}
    (rels : List (FreeGroup (Fin N))) : Subgroup (FreeGroup (Fin N)) :=
  Subgroup.normalClosure (rels.toFinset : Set (FreeGroup (Fin N)))

-- The presentation is trivial exactly when those relators generate everything.
def presentsTrivialGroupAny {N : Nat} (p : Presentation (Fin N)) : Prop :=
  normalClosureAny p.relations = ⊤

-- The actual presented group: free group modulo the normal closure.
def presentedGroup {N : Nat} (p : Presentation (Fin N)) :=
  (FreeGroup (Fin N)) ⧸ (normalClosureAny p.relations)

-- The standard target presentation: each generator is killed by its own relator.
def trivialPresentationAny (N : Nat) : Presentation (Fin N) :=
  ⟨List.ofFn (fun i : Fin N => FreeGroup.of i)⟩

-- "AC-trivial" means reachable from p by the generated AC equivalence relation.
def GeneralACTrivial (N : Nat) (p : Presentation (Fin N)) : Prop :=
  GeneralACEquivalent N p (trivialPresentationAny N)

The two definitions state the classical conjecture precisely. \(\mathrm{presentsTrivialGroupAny}(p)\) says the relators normally generate the whole free group. \(\mathrm{GeneralACTrivial}(N,p)\) says there is an AC-equivalence path from \(p\) to the standard trivial presentation. The Andrews-Curtis conjecture is exactly the claim that the first condition implies the second, for balanced presentations.

-- An inductive relation is a list of allowed one-step moves.
-- Each constructor below is one allowed move in the move graph.
inductive ACMove : Presentation (Fin 2) → Presentation (Fin 2) → Prop
  | h1 (p : Presentation (Fin 2)):
    -- h1 says: replace r₂ by r₂ * r₁.
    ACMove p ⟨p.relations.set 1 ((p.relations.getD 1 1) * (p.relations.getD 0 1))⟩
  -- h2 through h11 omitted here for space.
  | h12 (p : Presentation (Fin 2)):
    -- h12 says: conjugate r₁ by x⁻¹.
    ACMove p ⟨p.relations.set 0 (x⁻¹ * (p.relations.getD 0 1) * x)⟩

-- EqvGen means "take the equivalence relation generated by those one-step moves."
-- In plain English: any finite sequence of ACMove steps, forwards or backwards.
def ACEquivalent : Presentation (Fin 2) → Presentation (Fin 2) → Prop :=
  Relation.EqvGen ACMove

-- GeneralACMove is the same idea, but for any rank N.
-- Fin N is Lean's finite type with N generator names: 0, 1, ..., N-1.
inductive GeneralACMove (N : Nat) :
    Presentation (Fin N) → Presentation (Fin N) → Prop
  | multiply (p : Presentation (Fin N)) (i j : Fin N) (s : Int)
    (h_ne : i ≠ j) (h_sign : s = 1 ∨ s = -1) :
    -- Replace rᵢ by rᵢ * rⱼ^s. The proofs say i and j are different,
    -- and that s is really one of the two allowed signs.
    GeneralACMove N p (applyMultiplicationMove N p i j s)
  | invert (p : Presentation (Fin N)) (i : Fin N) :
    -- Replace rᵢ by its inverse.
    GeneralACMove N p (applyInversionMove N p i)
  | conjugate (p : Presentation (Fin N)) (i g : Fin N) (s : Int)
    (h_sign : s = 1 ∨ s = -1) :
    -- Conjugate rᵢ by generator g or by g⁻¹.
    GeneralACMove N p (applyConjugationMove N p i g s)

-- Stable moves can change rank, so the rank N travels with the presentation.
def AnyPresentation : Type := Σ N : Nat, Presentation (Fin N)

inductive StableACMove : AnyPresentation → AnyPresentation → Prop
  | ac (N : Nat) (p q : Presentation (Fin N)) :
      -- Ordinary fixed-rank AC moves are still allowed.
      GeneralACMove N p q →
      StableACMove ⟨N, p⟩ ⟨N, q⟩
  | stabilize (N : Nat) (p : Presentation (Fin N)) :
      -- Add a fresh generator and a fresh relator killing it.
      StableACMove
        ⟨N, p⟩
        ⟨N+1, ⟨(liftPresentationSucc N p).relations ++ [newGen N]⟩⟩
  -- destabilize, substitute_remove, substitute_remove_any,
  -- and substitute_remove_neg_any are defined in StableACMoves.lean.

A certificate only proves reachability in the relation it uses. Our searcher uses the hand-written rank-two relation ACEquivalent, while most of the mathematical library uses GeneralACEquivalent. The translation therefore has to show that every move accepted by the search checker is also a valid arbitrary-rank AC move. Harmonic's review helped us isolate that obligation, and we proved it in Basic.lean.

Some examples we formalized

We used examples throughout the development to check that the definitions matched the mathematics. A two-step certificate tests the full replay path by hand, the Akbulut-Kirby family tests a parameterized collection of difficult presentations, and the knot examples connect the formal move systems back to the paper.

A two-step AC certificate

We use \(\langle x,y \mid xy, xyx^{-1}\rangle\) as a small end-to-end check. Its two-move solution is easy to inspect: conjugate the second relator by \(x^{-1}\) to obtain \(y\), then right-multiply the first by \(y^{-1}\) to obtain \(x\). The Lean proof names those same moves and joins them with Relation.EqvGen.trans.

-- The destination state for the search game.
-- The two relators are just x and y.
def trivial_presentation : Presentation (Fin 2) :=
  ⟨[x, y]⟩

-- The toy starting state: ⟨x,y | xy, xyx⁻¹⟩.
def example_presentation : Presentation (Fin 2) :=
  ⟨[x * y, x * y * x⁻¹]⟩

-- This is a replayable certificate, not a heuristic claim.
#time theorem example_is_AC_trivial : ACEquivalent example_presentation trivial_presentation := by
  -- Step 1: Conjugate the second relation by x⁻¹
  let rels1 : List (FreeGroup (Fin 2)) := {x * y, y}
  have step1 : ACMove example_presentation (Presentation.mk rels1) := by
    -- h5 is the named move constructor we want.
    -- convert lets Lean match the concrete list representation.
    convert ACMove.h5 example_presentation
    -- decide handles the remaining finite computation.
    decide
  -- Step 2: Right multiply r₁ by r₂⁻¹
  have step2 : ACMove (Presentation.mk rels1) trivial_presentation := by
    -- h2 changes xy into xy * y⁻¹ = x.
    convert ACMove.h2 (Presentation.mk rels1)
    decide
  -- Now combine all the steps using transitivity of ACEquivalent
  have eq1 : ACEquivalent example_presentation (Presentation.mk rels1) :=
    Relation.EqvGen.rel _ _ step1
  have eq2 : ACEquivalent (Presentation.mk rels1) trivial_presentation :=
    Relation.EqvGen.rel _ _ step2
  -- Chain the two certified edges into one certified path.
  apply Relation.EqvGen.trans example_presentation (Presentation.mk rels1) trivial_presentation
  apply eq1
  apply eq2

The Akbulut-Kirby family

Selman Akbulut and Robion Kirby introduced the family now written \(AK(n)\) in 1985, while studying possible smooth counterexamples in four-dimensional topology[11]. For every \(n\geq 2\), the family gives a balanced two-generator presentation of the trivial group: \[ AK(n)=\langle x,y\mid x^n=y^{n+1},\;xyx=yxy\rangle. \] The first relation ties two neighboring powers together. The second is the braid relation. The presentation has only two relators, but the question is whether those relators can be reduced to \(x\) and \(y\) by AC moves.

These are called potential counterexamples because no one has proved that any \(AK(n)\) violates the conjecture. \(AK(2)\) has an AC trivialization. \(AK(3)\), whose first relation is \(x^3=y^4\), is the shortest presentation up to AC-equivalence that has resisted every known attempt at length reduction[2][6]. A failed search does not settle its status; the lower-bound examples discussed earlier show how long a valid trivialization can be.

I like this family as a formalization test because one definition gives infinitely many concrete instances. We can prove structural facts for a symbolic \(n\), generate a particular presentation for computation, and check a discovered move sequence in the same framework. The reinforcement-learning study proves a uniform length reduction for \(AK(n)\) when \(n\geq 5\). Since \(AK(2)\) is already AC-trivial, \(AK(3)\) and \(AK(4)\) are the two small cases not covered by that reduction[2].

-- AK is a whole family of presentations, one for each natural number n.
def AK (n : Nat) : Presentation (Fin 2) :=
  let x := FreeGroup.of (0 : Fin 2)
  let y := FreeGroup.of (1 : Fin 2)
  -- The first relator encodes x^n = y^(n+1).
  let rel1 := x^n * (y^(n+1))⁻¹
  -- The second relator is the fixed braid-like word in the family.
  let rel2 := x * y * x * (y * x * y)⁻¹
  ⟨[rel1, rel2]⟩

-- This proof is just bookkeeping: AK n has two generators and two relators.
lemma balanced_AK (n : Nat) : balanced (AK n) := by
  unfold balanced AK
  simp

-- This theorem says AK n is equivalent to the Miller-Schupp presentation
-- in the general move system. It is not automatically a Basic.lean ACMove proof.
theorem AK_equiv_MS_w₁ (n : Nat) (_hn : 2 ≤ n) :
    GeneralACEquivalent 2 (AK n) (MS n w₁ w₁_exp_sum) := by
  classical
  -- The proof in AK.lean continues as an explicit chain of GeneralACMove steps.

Encoding \(AK\) as a function of \(n\) lets Lean prove once that every member is balanced. The second theorem connects \(AK(n)\) to a Miller-Schupp presentation. That connection is useful because it lives in the same general relation to which we lift checked rank-two search certificates. Once a search trace has been proved as ACEquivalent, ACEquivalent.toGeneral transports it to GeneralACEquivalent 2, where it can be combined with this theorem.

What stable AC means

Ordinary AC moves keep the number of generators fixed. A rank-two proof starts with two generators and two relators, and every intermediate presentation has that same rank. Stable AC allows one additional operation called stabilization: introduce a new generator \(z\) together with the relator \(z\).

The new relator says \(z=e\), so this operation does not change the group being presented. It gives the move sequence a temporary generator. Subsequent AC moves may use \(z\) inside the relators, and a destabilization removes the extra generator-relator pair after \(z\) has been isolated again. At the level of presentation complexes, this is the algebraic form of adding and later removing a cancelling cell pair, which connects stable AC to 3-deformations of contractible two-complexes[12].

Stable AC is therefore a weaker target than ordinary AC: it permits every ordinary move plus temporary changes of rank. A stable trivialization proves that the presentation can be reduced after allowing this extra workspace. It does not by itself provide a fixed-rank AC trivialization. Keeping the two claims separate matters when a search result is turned into a theorem.

The rank change also matters to Lean. A presentation over \(\mathrm{Fin}\,N\) and one over \(\mathrm{Fin}(N+1)\) have different types. We store the rank together with the presentation in AnyPresentation, so a stable move can change both pieces without erasing which generators are available.

The constructors below record four situations. ac performs an ordinary move at a fixed rank. stabilize adds the new generator and its defining relator. destabilize removes an isolated generator only after proving that the other relators do not mention it. The substitution constructors cover the common case in which one relator explicitly solves for a generator, allowing Lean to substitute that word before lowering the rank.

-- A stable presentation is a pair:
--   rank N, plus a presentation over Fin N.
def AnyPresentation : Type := Σ N : Nat, Presentation (Fin N)

inductive StableACMove : AnyPresentation → AnyPresentation → Prop
  | ac (N : Nat) (p q : Presentation (Fin N)) :
      -- A normal general AC move, without changing rank.
      GeneralACMove N p q →
      StableACMove ⟨N, p⟩ ⟨N, q⟩

  | stabilize (N : Nat) (p : Presentation (Fin N)) :
      -- Add one new generator and one new relator saying it is trivial.
      StableACMove
        ⟨N, p⟩
        ⟨N+1, ⟨(liftPresentationSucc N p).relations ++ [newGen N]⟩⟩

  | destabilize (N : Nat) (p : Presentation (Fin (N+1)))
      (h_split : ∃ rs : List (FreeGroup (Fin (N+1))),
        p.relations = rs ++ [newGen N] ∧ (∀ r ∈ rs, DoesNotMentionLast N r)) :
      -- Remove the last generator again, but only if the other relators
      -- do not mention it. The proof h_split is that safety check.
      StableACMove
        ⟨N+1, p⟩
        ⟨N,
          let rs := Classical.choose h_split
          let hrs := (Classical.choose_spec h_split).2
          dropLastPresentation N ⟨rs⟩ hrs⟩

  | substitute_remove (N : Nat) (rs : List (FreeGroup (Fin (N+1)))) (w : FreeGroup (Fin N)) :
      -- If the new generator is defined by y = w, substitute w everywhere
      -- and then remove y.
      StableACMove
        ⟨N+1, ⟨rs ++ [ (newGen N)⁻¹ * liftWordSucc w ]⟩⟩
        ⟨N, substituteAndRemovePresentation N rs w⟩

  -- The full file also contains variants that remove any chosen generator
  -- and handle a negatively oriented defining relator.

-- A stable certificate is any finite chain of these stable moves.
def StableACEquivalent : AnyPresentation → AnyPresentation → Prop :=
  Relation.EqvGen StableACMove

From a knot diagram to a presentation

Some relator lists in the search code come directly from knot diagrams through a Wirtinger presentation: a presentation of the knot group read from the arcs and crossings in the diagram.

Take an oriented knot diagram and break it into arcs at the undercrossings. Assign one group generator to each arc. At a crossing, let \(x\) denote the over-passing arc and let \(y,z\) denote the incoming and outgoing under-passing pieces. The crossing says that the outgoing generator is a conjugate of the incoming generator by the over-passing generator. The sign is determined by the orientation:

Moving either equation to one side gives a relator, for example \(y^{-1}x^{-1}zx=1\). Repeating this at every crossing produces the Wirtinger presentation of the knot group. A diagram with \(n\) crossings has \(n\) arc generators and \(n\) crossing relators, so the presentation is balanced. The crossing relators also satisfy a product identity, which is why one of them can be deleted without losing the knot group.

For an unknot, the group after deleting that redundant relator is infinite cyclic. We then append a word \(w\) whose total exponent sum is \(1\) or \(-1\). The total exponent sum is what remains after replacing every generator by \(+1\) and every inverse by \(-1\); for example, \(xy^{-1}x\) has exponent sum \(1-1+1=1\). In the cyclic quotient, such a word kills the remaining generator and gives a balanced presentation of the trivial group.

The Lean hypothesis IsUnknotWirtinger K packages the unknot group facts and the supporting data used by the paper. Under that hypothesis, theorem16_paper proves ordinary AC-triviality at rank \(K.n\) for the modified presentation, and proposition12_paper derives stable AC-triviality. The construction gives the search problem a geometric source and a precise theorem explaining how that source becomes an AC instance.

-- One oriented crossing contributes one conjugation relator.
def Crossing.relator {n : Nat} (c : Crossing n) : FreeGroup (Fin n) :=
  let x := FreeGroup.of c.x
  let y := FreeGroup.of c.y
  let z := FreeGroup.of c.z
  match c.kind with
  | .left  => y⁻¹ * x⁻¹ * z * x
  | .right => y⁻¹ * x * z * x⁻¹

-- From an unknot diagram, delete one relator,
-- add a word with exponent sum ±1, and get general AC-triviality.
theorem theorem16_paper (K : KnotDiagram)
    (h_unknot : IsUnknotWirtinger K)
    (k : Fin K.n) (w : FreeGroup (Fin K.n)) (hw : HasExponentSumPM1 w) :
    GeneralACTrivial K.n (deleteRelatorAddWord K k w) := by
  -- Proof continues in KnotTheory.lean.

-- The stable version of the same paper-facing construction.
theorem proposition12_paper (K : KnotDiagram)
    (h_unknot : IsUnknotWirtinger K)
    (k : Fin K.n) (w : FreeGroup (Fin K.n)) (hw : HasExponentSumPM1 w) :
    StablyACTrivialAny K.n (deleteRelatorAddWord K k w) := by
  -- Proof continues in KnotTheory.lean.

We record the open conjectures as propositions beside the proved statements. This keeps the mathematical claim available as a hypothesis without inserting an unproved theorem or a sorry into the checked development.

-- The open rank-two conjecture, recorded as a proposition.
def AC_conjecture (p : Presentation (Fin 2)) : Prop :=
  balanced p →
  AndrewCurtisConjecture.presentsTrivialGroupAny p →
  ACEquivalent p trivial_presentation

-- The stable conjecture, also recorded as an open proposition.
def stable_AC_conjecture (N : Nat) (p : Presentation (Fin N)) : Prop :=
  balanced p →
  AndrewCurtisConjecture.presentsTrivialGroupAny p →
  StablyACTrivialAny N p

A closer audit with Aristotle

Aristotle had already helped us test definitions and small proofs during development. Once the project contained three move systems, examples, and results spread across several files, I also used it as a second reader for the full theorem graph.

I asked concrete questions: which relation does this inductive type generate, which results still depend on sorry, does this theorem prove classical or stable AC-equivalence, and can a rank-two ACEquivalent search certificate be lifted into GeneralACEquivalent 2? I checked each answer against the Lean source and the mathematics.

Each answer had to point to a constructor, theorem, or missing implication that could be inspected directly.

An early stress test

One early prompt was blunt: prove or disprove the Andrews-Curtis conjecture. Aristotle formalized the statement, proved the small ranks, and stopped at the open rank-two case.

The generated project handled the supporting facts first. It proved that the standard presentation is trivial and that one AC move preserves the normal closure of the relators. A finite checked move chain therefore preserves the presented group. Those are the supporting lemmas a certificate checker needs before discussing the open conjecture.

The \(n=1\) result is fully transparent. The free group on one generator is \(\mathbb Z\). A relator normally generates it only when its exponent is \(1\) or \(-1\), so the presentation is already standard or needs one inversion. Aristotle proved that case and stopped before rank two.

-- Rank zero: there are no generators and no relators.
-- The only tuple is already the standard tuple.
theorem andrewsCurtis_n0 (r : RelatorTuple 0) (h : r.presentsTriv) :
    ACEquiv r (RelatorTuple.standard 0) := by
  convert ACEquiv.refl _
  exact funext fun i => Fin.elim0 i

-- Rank one: FreeGroup (Fin 1) behaves like ℤ.
-- A relator that normally generates everything has exponent ±1.
-- So either it is already the generator, or one inversion move is enough.
theorem andrewsCurtis_n1 (r : RelatorTuple 1) (h : r.presentsTriv) :
    ACEquiv r (RelatorTuple.standard 1) := by
  -- The generated proof is longer, but the mathematical reason is this:
  -- in rank one, the only normal generators are x and x⁻¹.

In later sessions, Aristotle traced the generated relations, found remaining assumptions, and suggested changes to imports and theorem statements. I checked each suggestion against the source. Accepted suggestions ended in a smaller, explicit Lean obligation.

A concrete interaction

In one session, we asked Aristotle to compare ACMove with GeneralACMove. It noticed that GeneralACMove listed inversion as an explicit constructor, while ACMove did not. It then asked whether the files contained a lemma proving that a certificate from the rank-two search relation was valid in the general relation. They did not. Aaron and I checked the issue, matched each of the twelve computational moves to a constructor of GeneralACMove, and proved the translation.

What the review checked

Aristotle compared the constructors literally. The phrase "AC moves" in the prose referred to two different inductive relations in Lean. This gave us a precise question: is every move emitted by the rank-two searcher accepted by the general mathematical relation? We turned that question into two Lean theorems and proved both.

The mismatch we fixed

Harmonic found a real mismatch between our rank-two search relation and the general mathematical relation. We fixed it and proved that every certificate produced by the search checker is valid in the general system.

The hand-written rank-two ACMove type had four multiplication moves and eight conjugation moves. Inversion, replacing \(r_i\) by \(r_i^{-1}\), was not a constructor. The general GeneralACMove type did include inversion as a primitive move.

For our certificate pipeline, the required direction is from the smaller computational action set into the general relation. We proved ACMove.toGeneral by checking all twelve constructors. We then lifted finite chains with ACEquivalent.toGeneral. This means a search certificate can now be used in the arbitrary-rank formalization without identifying the two relations.

/-- Every move in the rank-two computational action set is a general AC move. -/
theorem ACMove.toGeneral {p q : Presentation (Fin 2)} (h : ACMove p q) :
    GeneralACMove 2 p q := by
  cases h with
  | h1 =>
      simpa [applyMultiplicationMove] using
        (GeneralACMove.multiply p
          (⟨1, by decide⟩ : Fin 2) (⟨0, by decide⟩ : Fin 2)
          1 (by decide) (by left; rfl))
  -- The remaining eleven constructors are checked in the same way.

/-- A certificate in the computational relation is valid in the general AC relation. -/
theorem ACEquivalent.toGeneral {p q : Presentation (Fin 2)}
    (h : ACEquivalent p q) : GeneralACEquivalent 2 p q := by
  induction h with
  | refl => exact Relation.EqvGen.refl (r := GeneralACMove 2) _
  | rel _ _ hmove => exact Relation.EqvGen.rel _ _ hmove.toGeneral
  | trans _ _ _ _ _ ih₁ ih₂ => exact Relation.EqvGen.trans _ _ _ ih₁ ih₂
  | symm _ _ _ ih => exact Relation.EqvGen.symm _ _ ih

The proof makes the interface explicit. The search code can keep its compact twelve-move action space, while the rest of the development works with the general definition. Lean checks every step when a computational certificate crosses that boundary.

Where this leaves us

Aristotle was most useful when the questions were concrete. It traced theorem dependencies across several files, stopped at the open cases, and found a mismatch between two move systems. Aaron and I repaired that interface and proved the search-to-general translation in Lean. I still checked every suggestion against the source and the mathematics, but Aristotle made that review faster and more disciplined.

Next, we want to replay more certificates from search, release the repository, and keep extending the formal library around rank-two computational, arbitrary-rank, and stable AC. For each computational result, the theorem type should state the exact move relation that was checked.

We are grateful to Harmonic for supporting this work and for giving us access to Aristotle while the formalization was still evolving. Their team has been generous with its time and feedback, and we thank them for helping us test the system on a real mathematical development. We are very happy with the collaboration so far and look forward to continuing it.

References and related work

1. Sergei Gukov. Official homepage. Research in mathematical physics, topology, and machine learning at Caltech.
2. Ali Shehper, Anibal M. Medina-Mardones, Lucas Fagan, Bartłomiej Lewandowski, Angus Gruen, Yang Qiu, Piotr Kucharski, Zhenghan Wang, and Sergei Gukov. What makes math problems hard for reinforcement learning: a case study. arXiv:2408.15332, 2024.
3. Caroline Zhang, Aaron Zhao, Robert Joseph George, Sergei Gukov, and Anima Anandkumar. Mathematical Discovery and Formalization Towards the AC Conjecture. NeurIPS MATH-AI 2025. Project listing.
4. Lean theorem prover. Lean 4 documentation and theorem proving ecosystem. The final certificate checker for the formalized move systems discussed above.
5. J. J. Andrews and M. L. Curtis. Free groups and handlebodies. Proceedings of the American Mathematical Society 16, 192-195, 1965. The classical source of the Andrews-Curtis conjecture.
6. George Havas and Colin Ramsay. Breadth-first search and the Andrews-Curtis conjecture. International Journal of Algebra and Computation 13(1), 61-68, 2003.
7. Krzysztof Krawiec and Jerry Swan. Distance Metric Ensemble Learning and the Andrews-Curtis Conjecture. arXiv:1606.01412, 2016.
8. Martin R. Bridson. The complexity of balanced presentations and the Andrews-Curtis conjecture. arXiv:1504.04187, 2015.
9. Boris Lishak. Balanced finite presentations of the trivial group. Journal of Topology and Analysis 9(2), 363-378, 2017.
10. Harmonic. Aristotle and AI-assisted formalization tools. Used here as an audit layer for Lean definitions, theorem dependencies, and formalization boundaries.
11. Selman Akbulut and Robion Kirby. A potential smooth counterexample in dimension 4 to the Poincaré conjecture, the Schoenflies conjecture, and the Andrews-Curtis conjecture. Topology 24(4), 375-390, 1985.
12. Lucas Fagan. The Stable Andrews-Curtis Conjecture and Generic 2-Polyhedra. Doctoral dissertation, University of California, Santa Barbara, 2025.