Kourovka 2.28

### What is the conjecture
Can every orderable group be embedded in a pro-orderable group?

In the Kourovka Notebook (Problem 1.35 and 2.28), a **pro-orderable group** is defined as a group in which **every partial ordering can be extended to a linear (total) ordering**.

Outside of the Kourovka Notebook, this specific class of groups is more commonly referred to as **O*-groups** (read as "O-star groups").
* **O*-group**: A group $G$ is an O*-group if every partial order on $G$ can be extended to a total order on $G$.

### Discussion in Literature
The problem and the class of groups it concerns have been studied by several authors. Key discussions outside Kourovka include:

* **V. M. Kopytov**: A Russian mathematician who solved related problems (e.g., Kourovka 1.35b). He showed that **subgroups of pro-orderable groups are not always pro-orderable** (published in *Algebra i Logika*, 1966). This negative result makes the embedding problem (2.28) particularly non-trivial because you cannot simply embed a group into a "larger" pro-orderable structure and expect the property to hold for the subgroup.
* **Colin D. Fox**: In his work in the 1970s (e.g., *"An Embedding Theorem for Ordered Groups"*, *Canadian Journal of Mathematics*, 1972), he explicitly discusses this property. He proves that certain classes of groups (e.g., groups with a specific normal chain structure where factors are locally nilpotent and torsion-free) can be embedded into divisible O*-groups.
* **H. A. Hollister**: In his Ph.D. thesis (University of Michigan, 1965) and subsequent papers (e.g., *Proc. Amer. Math. Soc.*, 1968), he studied groups with extension properties for partial orders.
* **Torsion-Free Abelian Groups**: It is a known result (attributed to Simbireva) that every torsion-free abelian group is an O*-group.

### Status of the Problem
The general question—"Can **every** orderable group be embedded in a pro-orderable (O*-) group?"—remains **unsolved** as of the latest editions of the Kourovka Notebook (including the 20th edition, 2022).

While it is known that many common orderable groups (like torsion-free abelian groups) *are* pro-orderable, and that certain extensions work, the general embedding conjecture has not been proven true or false. The difficulty lies in the fact that the "pro-orderable" condition is very strong (requiring *every* partial order to extend), and as Kopytov showed, this property is not hereditary (it doesn't pass to subgroups), which prevents standard embedding techniques from easily working.

### Prerequisites needed
To state Kourovka Problem 2.28 ("Can every orderable group be embedded in a pro-orderable group?") in Lean 4, you do not need new logical foundations, but you must define specific predicates that are not standardly bundled in `Mathlib`.

`Mathlib` is primarily designed around **typeclasses** (where a group `G` has a single, canonical order `[OrderedGroup G]`). However, this problem requires treating orders as **variables** (quantifying over *all possible* orders on a group).

Here are the specific definitions and structures missing from `Mathlib` that you would need to define to state the question:

### 1. Missing Definition: `IsBiInvariant` (for a Relation)
`Mathlib` handles invariance via typeclasses like `CovariantClass`, but for this problem, you need a predicate that applies to an arbitrary relation `r : G → G → Prop`.

```lean
/-- A relation r is bi-invariant if it is preserved by multiplication on both sides. -/
def IsBiInvariant (G : Type*) [Group G] (r : G → G → Prop) : Prop :=
(∀ a b k : G, r a b → r (k * a) (k * b)) ∧
(∀ a b k : G, r a b → r (a * k) (b * k))
```

### 2. Missing Structure: `IsOrderableGroup` (Existence Predicate)
`Mathlib` has `LinearOrderedGroup` (a group *equipped* with an order), but it lacks the predicate "this group *admits* a linear order."

```lean
/-- A group is orderable if there exists a linear order compatible with the group structure. -/
def IsOrderableGroup (G : Type*) [Group G] : Prop :=
∃ r : G → G → Prop, IsLinearOrder G r ∧ IsBiInvariant G r
```

### 3. Missing Structure: `IsProOrderableGroup` (The "O*-group" Property)
This is the core concept of the problem. It is not in `Mathlib`. A group is pro-orderable (often called an **O*-group** in literature) if every compatible *partial* order extends to a compatible *total* (linear) order.

```lean
/-- A group is pro-orderable if every bi-invariant partial order extends to a bi-invariant linear order. -/
def IsProOrderableGroup (G : Type*) [Group G] : Prop :=
∀ r : G → G → Prop,
(IsPartialOrder G r ∧ IsBiInvariant G r) →
∃ s : G → G → Prop,
IsLinearOrder G s ∧
IsBiInvariant G s ∧
∀ a b, r a b → s a b
```

### 4. The Formal Statement
With those definitions added, the question can be stated as:

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

open Function

-- [Insert the definitions above here]

/-- Kourovka 2.28: Can every orderable group be embedded in a pro-orderable group? -/
def Kourovka_2_28 : Prop :=
∀ (G : Type*) [Group G],
IsOrderableGroup G →
∃ (H : Type*) [Group H],
IsProOrderableGroup H ∧
Nonempty (G ↪* H) -- G embeds into H
```

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