Formal target: Corpus.WikipediaAndrewsCurtis.andrews_curtis_conjecture

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

Exact formal statement

∀ (n : Nat) (r : Corpus.WikipediaAndrewsCurtis.RelatorTuple n),
  Corpus.WikipediaAndrewsCurtis.NormallyGenerates r →
    Corpus.WikipediaAndrewsCurtis.Equivalent r (Corpus.WikipediaAndrewsCurtis.standardRelators n)

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record