Kourovka 1.12 - Triviality Problem for Balanced Presentations

### What is the conjecture
The question is **Problem 1.12** in the **Kourovka Notebook** (a famous collection of unsolved problems in group theory), originally posed by **Wilhelm Magnus**.

This question is discussed extensively in research papers within the field of **combinatorial group theory**. It addresses the **decidability of the triviality problem** for a specific class of groups.

The question asks for the existence of an algorithm (a decision procedure) for the following problem:

> **"Does there exist an algorithm which, taking as input any finite presentation with $n$ generators and $n$ defining relations (where $n > 2$), determines whether the group defined by that presentation is the trivial group?"**

In technical terms, this is the **Triviality Problem for Balanced Presentations** (also known as presentations of **deficiency zero**). The problem asks if the property of being trivial is **decidable** for the class of groups having balanced presentations with more than 2 generators.

### Context and Research Discussion

**1. Meaning of the Problem:**
* **General Case:** For general finitely presented groups (where the number of relations is not restricted relative to generators), the triviality problem is known to be **undecidable** (a result of the Adian–Rabin theorem).
* **Balanced Case ($n$ generators, $n$ relations):** The condition of being "balanced" (having deficiency 0) places strong constraints on the group. However, it is unknown whether these constraints are strong enough to make the triviality problem decidable.

**2. Relation to the Andrews-Curtis Conjecture:**
This problem is deeply connected to the **Andrews-Curtis Conjecture**.
* The Andrews-Curtis conjecture states that every balanced presentation of the trivial group can be transformed into the empty presentation (trivial generators, trivial relations) using a specific set of operations called **Andrews-Curtis moves** (AC-moves) or extended Nielsen transformations.
* **If the Andrews-Curtis conjecture is true**, then the triviality problem for balanced groups is likely **decidable** (or at least the set of trivial balanced presentations is recursively enumerable in a very specific way that might lead to decidability).
* However, the Andrews-Curtis conjecture remains open and is widely suspected to be false (potential counterexamples have been proposed but not proven).

**3. Why $n > 2$?**
* **$n=1$:** A group with 1 generator and 1 relation is simply a cyclic group $\langle x \mid x^k = 1 \rangle$. It is trivial if and only if $|k|=1$. This is easily decidable.
* **$n=2$:** The case for 2 generators and 2 relations is also a major open area, but Magnus likely specified $n > 2$ to generalize the problem beyond the specific low-dimensional topological difficulties associated with $n=2$ (which relates to the geometry of 2-complexes). However, the difficulty essentially persists for all $n \geq 2$.

**4. Current Status:**
The problem remains **open**. It is listed as an unsolved problem in modern editions of the Kourovka Notebook (including recent updates like the 20th edition). There is no known algorithm to decide triviality for this class, nor is there a proof that it is undecidable.

### Summary
In research papers, this question is treated as a fundamental open problem linking **algorithmic group theory** and **low-dimensional topology**. It essentially asks: *Is the "balanced" property sufficient to make the structure of a group algorithmically knowable, or can balanced groups encode enough complexity to make checking for triviality impossible?*

### Prerequisites needed
Note: this is from Gemini, so double-check.

To state Kourovka Problem 1.12 in Lean 4, **surprisingly little is missing** from `mathlib`. The library already contains the definitions for free groups, presented groups, and the trivial group.

However, to state the question formally as a problem of **computability** (which is necessary because the problem asks for an *algorithm*, and the answer might be negative), you need to bridge the gap between "Abstract Group Theory" and "Computability Theory."

Here are the specific definitions or structures that are not "missing" in the sense of being impossible, but are **not currently bundled** in `mathlib` in a way that allows for a one-line statement of the problem.

### 1. A Bundled "Finite Presentation" Structure
`Mathlib` defines `PresentedGroup` as a type derived from a set of relations. To state the problem algorithmically, you need to treat the *presentation itself* as data.

**What is missing:** A structure that bundles the number of generators and the list of relations into a single object.
**How to define it:**
```lean
import Mathlib.GroupTheory.FreeGroup
import Mathlib.GroupTheory.PresentedGroup

-- A finite presentation is the data: number of generators 'n' and a list of words in FreeGroup n
structure FinitePresentation where
n : ℕ
rels : List (FreeGroup (Fin n))
```

### 2. A Computable Encoding of Presentations
To ask if an "algorithm" exists in the rigorous mathematical sense (Turing computable), the input data (the presentation) must be encodable into natural numbers (Gödel numbering).

**What is missing:** An instance of `Encodable` or `Countable` specifically for the `FinitePresentation` structure defined above.
**Why it's needed:** You cannot use `Mathlib.Computability` predicates on a type unless that type can be mapped to data (like `ℕ` or `List Bool`).
**Current State:** `Mathlib` has `Encodable` for Lists and Naturals, so deriving this is straightforward but manual work.

### 3. The "Triviality" Predicate for Presentations
`Mathlib` has `IsTrivial` for *Groups*, but not for *Presentations*.

**What is missing:** A definition mapping the data `FinitePresentation` to the proposition that the *Presented Group* is trivial.
**How to define it:**
```lean
def yields_trivial_group (fp : FinitePresentation) : Prop :=
-- The presented group is isomorphic to the trivial group (PUnit)
Nonempty (PresentedGroup fp.rels ≃* PUnit)
```

---

### How to State the Question in Lean 4 *Now*

You can actually state the question right now using existing `mathlib` features if you define the "glue" structures yourself.

Here is how you would state W. Magnus's question. The "missing" parts are defined explicitly in the preamble:

```lean
import Mathlib.GroupTheory.FreeGroup
import Mathlib.GroupTheory.PresentedGroup
import Mathlib.Computability.Computable -- Needed for the strict "Algorithm" definition

open Computability

-- 1. DEFINE THE DATA STRUCTURE (Missing in Mathlib)
-- A presentation with n generators and k relations
structure FinitePresentation where
n : ℕ
rels : List (FreeGroup (Fin n))

-- 2. DEFINE THE PROPERTY (Missing in Mathlib)
-- Does this presentation define the trivial group?
def is_trivial_presentation (fp : FinitePresentation) : Prop :=
Subsingleton (PresentedGroup fp.rels)

-- 3. DEFINE THE SUBSET OF INTEREST (The "Balanced" condition)
-- The set of presentations where generators = n and relations = n, with n > 2
def is_balanced_magnus_case (fp : FinitePresentation) : Prop :=
fp.rels.length = fp.n ∧ fp.n > 2

-- 4. ENCODING (Ideally Mathlib would provide this automatically)
-- We need to assert that FinitePresentation is encodable to discuss algorithms.
-- (We assume this instance exists for the statement below)
variable [Encodable FinitePresentation]

-- THE QUESTION (Kourovka 1.12)
-- "Is the set of trivial, balanced presentations (n > 2) decidable?"
-- In computable analysis terms: Is the set recursive?
def Kourovka_1_12_Open_Question : Prop :=
∃ (f : FinitePresentation → Bool),
-- The function must be Turing-Computable
Computable f ∧
-- The function must correctly identify triviality for the specific class
∀ (fp : FinitePresentation), is_balanced_magnus_case fp →
(f fp = true ↔ is_trivial_presentation fp)
```

### Summary of Missing Parts
1. **`FinitePresentation` as a Type**: Mathlib treats presentations as arguments to a constructor, not as a standalone data type.
2. **`Encodable` Instance**: Boilerplate code to map group words to natural numbers is required to connect Group Theory to Computability Theory.
3. **Algorithmic Predicates**: Concepts like `DecidablePred` are in the library, but applying them to Group Theory requires the setup above.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-20

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else