FormalConjectures.Wikipedia.AndrewsCurtis

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

The Andrews-Curtis conjecture

The conjecture says that every normally generating n-tuple in the free group on n generators is Andrews-Curtis equivalent to the standard free basis.

References:

Wikipedia, Andrews-Curtis conjecture

A. D. Myasnikov, A. G. Myasnikov and V. Shpilrain, On the Andrews-Curtis equivalence

namespace AndrewsCurtis

An n-tuple of relators in the free group on n generators.

abbrev RelatorTuple (n : ℕ) := Fin n → FreeGroup (Fin n)

The standard relator tuple, consisting of the free generators themselves.

def standardRelators (n : ℕ) : RelatorTuple n :=
  fun i ↦ FreeGroup.of i

The elementary Andrews-Curtis moves: inversion or multiplication of relators, interchange of two relators, and conjugation of one relator by an arbitrary word.

inductive Move {n : ℕ} : RelatorTuple n → RelatorTuple n → Prop
  | invert (r : RelatorTuple n) (i : Fin n) :
      Move r (Function.update r i (r i)⁻¹)
  | multiply (r : RelatorTuple n) (i j : Fin n) (hij : i ≠ j) :
      Move r (Function.update r i (r i * r j))
  | swap (r : RelatorTuple n) (i j : Fin n) :
      Move r (fun k ↦ r (Equiv.swap i j k))
  | conjugate (r : RelatorTuple n) (i : Fin n) (w : FreeGroup (Fin n)) :
      Move r (Function.update r i (w * r i * w⁻¹))

Andrews-Curtis equivalence is the equivalence relation generated by elementary moves.

def Equivalent {n : ℕ} : RelatorTuple n → RelatorTuple n → Prop :=
  Relation.EqvGen Move

A relator tuple normally generates the free group when the normal closure of its range is the whole free group. Equivalently, the associated balanced presentation presents the trivial group.

def NormallyGenerates {n : ℕ} (r : RelatorTuple n) : Prop :=
  Subgroup.normalClosure (Set.range r) = ⊤

The Andrews-Curtis conjecture.

Every normally generating n-tuple in the free group of rank n is Andrews-Curtis equivalent to the standard tuple of free generators.

@[category research open, AMS 20]
theorem andrews_curtis_conjecture (n : ℕ) (r : RelatorTuple n)
    (hr : NormallyGenerates r) :
    Equivalent r (standardRelators n) := byn:ℕr:RelatorTuple nhr:NormallyGenerates r⊢ Equivalent r (standardRelators n)
  sorryAll goals completed! 🐙

end AndrewsCurtis