Kourovka 1.5

### What is the conjecture
The question "Does there exist a group whose group ring does not contain zero divisors and is not embeddable into a skew field?" is a well-known open problem in algebra found in the **Kourovka Notebook** (a famous collection of unsolved problems in group theory).

Here are the specific details regarding its authorship and status:

### 1. Source and Authorship
* **Problem Number:** It is **Problem 1.5** in the Kourovka Notebook (appearing in the **1st Issue**, published in **1965**).
* **Associated Author:** The problem is attributed to **L. A. Bokut'** (Lev Arkad'evich Bokut'). In the notebook, it is often labeled as a "(Well-known problem)" followed by Bokut's name, indicating he submitted it to the collection.
* **Context:** This problem is a variation of **Malcev's Problem**. Anatoly Malcev (A. I. Mal'cev) had previously proved in 1937 and 1948 that not every associative ring without zero divisors (domain) can be embedded into a skew field (division ring). Problem 1.5 asks specifically if this pathology can occur in **group rings** of torsion-free groups.

### 2. Discussion in Research Papers
The problem is actively discussed in research papers under the umbrella of **Kaplansky's Conjectures** and the theory of **group rings**.
* **Kaplansky's Zero Divisor Conjecture (Kourovka 1.3):** States that the group ring of a torsion-free group has no zero divisors. If this conjecture is false, then the condition "does not contain zero divisors" in Problem 1.5 might rarely or never be met.
* **The Embedding Conjecture:** Often linked with Problem 1.5, it conjectures that *every* group ring of a torsion-free group (which is a domain) *is* embeddable in a skew field. If this conjecture is true, the answer to Problem 1.5 is "No."
* **Partial Results:**
* **Malcev (1948):** Constructed a semigroup ring that is a domain but not embeddable in a skew field.
* **Kropholler, Linnell, and Moody (1988):** Proved that for **elementary amenable groups** (a large class of groups), if the group is torsion-free, its group ring *is* embeddable in a skew field.
* **Recent Work:** The problem remains open for general torsion-free groups (e.g., hyperbolic groups). Recent papers (such as those by **Linnell**, **Lück**, and **Baykalov**) continue to cite Problem 1.5 as an unsolved question when discussing divisibility and embedding properties of group algebras.

### 3. Current Status
**The problem is Open.**
It is unknown whether such a group exists. Finding such a group would provide a counterexample to the conjecture that all group ring domains are embeddable in skew fields. Conversely, proving no such group exists would establish the Embedding Conjecture for group rings.

### Prerequisites needed
Gemini says the problem can be fully stated. Verify:
```
import Mathlib.Algebra.MonoidAlgebra.Basic
import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.Ring.Defs

/-- Kourovka Notebook Problem 1.5 (Bokut') -/
def kourovka_problem_1_5 : Prop :=
∃ (G : Type) [Group G],
let R := MonoidAlgebra ℤ G
(NoZeroDivisors R) ∧
(∀ (D : Type) [DivisionRing D], ∀ (f : R →+* D), ¬ Function.Injective f)
```

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

* ams-16

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