Kourovka 2.24

### What is the conjecture
Kourovka Problem 2.24, **"Are Engel torsion-free groups orderable?"** (posed by A. I. Kokorin), is considered a significant open question in the theory of ordered groups and is closely related to the longstanding **Plotkin Conjecture** regarding Engel groups.

### Summary of Status and Discussion Outside Kourovka
The problem remains **open** (unsolved). It appears in various survey papers, books, and conference slides concerning ordered groups and the Engel condition.

**1. Connection to Local Nilpotence (Plotkin's Conjecture)**
The most prominent context for this problem is its relationship to the structure of Engel groups.
* **Background:** It is a classical result (by A. I. Mal'cev) that every **torsion-free locally nilpotent group is orderable**.
* **The Link:** If every torsion-free Engel group were locally nilpotent (Plotkin's Conjecture), then the answer to Kourovka 2.24 would be **"Yes"**.
* **Current Status:** Plotkin's conjecture is known to be true for certain cases (e.g., 2-Engel, 3-Engel, and 4-Engel groups are locally nilpotent). However, for sufficiently large $n$, recent announcements (e.g., by Rips and Juhász) suggest that there exist torsion-free $n$-Engel groups that are *not* locally nilpotent. It is not yet known if these potential counterexamples to local nilpotence are orderable, leaving Problem 2.24 open.

**2. Partial Results and Literature**
The problem is discussed in several specific works:
* **Kim and Rhemtulla (1995):** In their paper *"Orderable Engel Groups"* (published in *Groups—Korea '94*), they proved the converse: **If an Engel group is orderable, then it is locally nilpotent.** This makes the open problem equivalent to asking: *"Are there any torsion-free Engel groups that are NOT locally nilpotent, and if so, can they be ordered?"*
* **Patrizia Longobardi (2020):** In presentations such as *"Small doubling in n-Engel groups"*, this problem is explicitly listed as an open question, often alongside the question of whether such groups are *right*-orderable.
* **Books on Ordered Groups:** Standard texts and surveys, such as *Fully Ordered Groups* by Kokorin and Kopytov (who posed the original problem) and later works by authors like Glass or Rhemtulla, discuss the relationship between the Engel condition and orderability.

**Conclusion**
The problem is not isolated to the notebook; it is a fundamental question linking orderability to the algebraic structure of generalized nilpotent groups. It remains unsolved primarily because the existence of non-locally-nilpotent torsion-free Engel groups is a difficult area of research, and determining the orderability of such complex potential counterexamples is even harder.

### Prerequisites needed
To state Kourovka Problem 2.24 ("Are Engel torsion-free groups orderable?") in Lean 4 (specifically using `Mathlib`), the following definitions or structures are currently **missing** (or not standardly available as predicates on a `Group`):

1. **Engel Groups (`IsEngel` or `EngelGroup`)**:
* **Status**: `Mathlib` does not currently have a definition for an "Engel group" (a group where for every pair $x, y$, the commutator $[x, _n y] = 1$ for some $n$).
* **What is needed**: A predicate `IsEngel (G : Type*) [Group G] : Prop` that quantifies over elements $x, y$ and asserts the existence of a natural number $n$ such that the $n$-th iterated commutator vanishes.
* *Note*: While commutators are defined (`commutator`), the specific iterated Engel condition is not in the library.

2. **Torsion-Free Groups (`IsTorsionFree` or `TorsionFree`)**:
* **Status**: While `Mathlib` has extensive support for torsion *subgroups* (`Mathlib.GroupTheory.Torsion`) and torsion-free *modules* (`Mathlib.RingTheory.Flat.TorsionFree`), there is no standard typeclass or predicate `IsTorsionFree (G : Type*) [Group G]` in the main library.
* **What is needed**: A definition stating that the only element of finite order is the identity (or equivalently, $x \ne 1 \implies \forall n > 0, x^n \ne 1$).
* *Context*: Specific projects (like the *Unit Conjecture* formalization) define this locally, but it is not yet a standard `Mathlib` component.

3. **Orderability (`IsOrderable`)**:
* **Status**: `Mathlib` has the `LinearOrderedGroup` typeclass, which bundles a group with a *specific* order. It does not have a standard predicate answering "Does there *exist* a linear order compatible with this group structure?"
* **What is needed**: A predicate `IsOrderable (G : Type*) [Group G] : Prop` (or `BiOrderable`), defined as the existence of a strict total order relation on $G$ that is bi-invariant (invariant under left and right multiplication).

### Example of how one would currently have to define them to state the problem:

```lean
import Mathlib.Algebra.Group.Defs
import Mathlib.Algebra.Order.Group.Defs

-- 1. Definition of Iterated Commutator (Engel condition)
def commutator_n (G : Type*) [Group G] (x y : G) : ℕ → G
| 0 => x
| n + 1 => commutator (commutator_n G x y n) y

-- 2. Predicate for Engel Groups
def IsEngel (G : Type*) [Group G] : Prop :=
∀ x y : G, ∃ n : ℕ, commutator_n G x y n = 1

-- 3. Predicate for Torsion-Free Groups
def IsTorsionFree (G : Type*) [Group G] : Prop :=
∀ x : G, x ≠ 1 → ∀ n : ℕ, n > 0 → x ^ n ≠ 1

-- 4. Predicate for Orderable Groups (Bi-orderable)
def IsOrderable (G : Type*) [Group G] : Prop :=
∃ (r : G → G → Prop),
IsStrictTotalOrder G r ∧
(∀ a b g : G, r a b → r (g * a) (g * b)) ∧
(∀ a b g : G, r a b → r (a * g) (b * g))

-- The Question (Kourovka 2.24)
theorem kourovka_2_24_open_problem (G : Type*) [Group G] :
IsEngel G ∧ IsTorsionFree G → IsOrderable G :=
sorry -- Open Problem
```

### [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