The Andrews-Curtis conjecture

/-
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](https://en.wikipedia.org/wiki/Andrews%E2%80%93Curtis_conjecture)
* [A. D. Myasnikov, A. G. Myasnikov and V. Shpilrain,
  *On the Andrews-Curtis equivalence*](https://arxiv.org/abs/math/0302080)
-/

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) := by
  sorry

end AndrewsCurtis

• Formalization source ↗

On-site verification needs an executable Lean target. None is attached yet.

A source attachment or link is not a verified proof. The statement’s correspondence with the original question needs human review.