Kourovka 1.31

### What is the conjecture
The problem **"Is a residually finite group with the maximum condition for subgroups almost polycyclic?"** (Kourovka Notebook Problem 1.31) is a well-known open problem in group theory that is discussed in various research papers and survey articles.

### 1. Status of the Problem
The problem remains **unsolved**. It appears as Problem 1.31 in the **Kourovka Notebook** (a famous collection of unsolved problems in group theory), proposed by **M. I. Kargapolov** in the 1960s. It continues to be listed as an open question in the most recent editions (e.g., the 20th edition published in 2023).

### 2. Context and Definitions
* **Maximum condition for subgroups (Max):** A group satisfies this condition if every strictly ascending chain of subgroups terminates. Such groups are often called **Noetherian groups**. An equivalent definition is that every subgroup of the group is finitely generated.
* **Almost polycyclic:** This typically means **polycyclic-by-finite** (or virtually polycyclic), i.e., the group contains a polycyclic subgroup of finite index.
* **The Question:** It is a standard theorem (due to P. Hall) that every polycyclic-by-finite group satisfies the maximum condition for subgroups and is residually finite. The problem asks if the converse is true: **If a group is Noetherian and residually finite, must it be polycyclic-by-finite?**

### 3. Discussion in Research
The problem is significant because the condition of "residual finiteness" is the only thing preventing known counterexamples:
* **Without Residual Finiteness:** The answer is **negative**. In 1979, **A. Y. Ol'shanskii** constructed "Tarski monsters"—infinite simple groups where every proper non-trivial subgroup is cyclic of prime order. These groups are Noetherian (satisfy Max) but are not polycyclic-by-finite. However, being infinite simple groups, they are **not** residually finite.
* **With Residual Finiteness:** The problem asks if the "pathological" structure of groups like Tarski monsters is impossible in the presence of residual finiteness.

### 4. Relevant Literature
While no paper has solved it, the problem is frequently cited in papers discussing:
* **Finiteness conditions:** Papers investigating groups with the Max condition (Noetherian groups).
* **Equationally Noetherian groups:** Recent work (e.g., by **M. Valiunas** in *Journal of Algebra*, 2021) compares residually finite groups and equationally Noetherian groups, often citing this problem as a boundary of current knowledge for finitely generated groups.
* **Growth of residual finiteness:** Papers studying the rate of growth of finite quotients often reference the structure of residually finite Noetherian groups.

In summary, the problem is a "classic" open question. It highlights the gap in understanding between the class of groups defined by the Max condition and the more tractable class of polycyclic groups.

### Prerequisites needed
Based on the current state of **Lean 4 Mathlib** (as of early 2026), the following definitions and structures are likely missing or not yet "bundled" in a way that allows for a direct, single-line statement of Kourovka 1.31.

To state the problem **"Is a residually finite group with the maximum condition for subgroups almost polycyclic?"**, you would need to define or assume the following structures which are not standard in Mathlib's main `GroupTheory` library:

### 1. `ResiduallyFinite`
While Mathlib has extensive libraries for finite groups and topological groups (including profinite completions), there is **no single typeclass** `ResiduallyFinite G` currently in the core library.
* **How to state it (if defining it yourself):** You would need to define it as: "The intersection of all subgroups of finite index is trivial" or "For every non-identity element $g$, there exists a homomorphism to a finite group mapping $g$ to a non-identity element."

### 2. `PolycyclicGroup`
Mathlib contains `Cyclic` groups and `Solvable` groups, but the specific definition for a **Polycyclic Group** (a group with a subnormal series where factors are cyclic) is **missing** from the main library.
* This is a significant gap for this specific problem, as "Polycyclic" is the core property in the conclusion.

### 3. `Virtually` / `Almost` (Polycyclic)
There is no generic `Virtually P` predicate in Mathlib that applies a property `P` to a subgroup of finite index.
* **Missing structure:** A definition for `AlmostPolycyclic` or `VirtuallyPolycyclic`. This would formally mean: "There exists a subgroup $H \le G$ such that $[G:H] < \infty$ and $H$ is Polycyclic."

### 4. `IsNoetherianGroup` (Max Condition)
While Mathlib has `IsNoetherian` for **modules** and rings, there is no direct `IsNoetherianGroup` class.
* **Available workaround:** You *can* state this using existing Mathlib structures by saying the lattice of subgroups is well-founded: `WellFoundedGT (Subgroup G)`. Alternatively, you can state that every subgroup is finitely generated (`∀ (H : Subgroup G), H.FG`).
* **Missing:** A bundled name like `HasMaxCondition` specifically for groups.

---

### Hypothesized Lean 4 Statement
If you were to state the problem, you would first need to provide these missing definitions. The code would look something like this:

```lean
import Mathlib.Algebra.Group.Subgroup.Basic
import Mathlib.Order.WellFounded
import Mathlib.GroupTheory.Finiteness

-- MISSING DEFINITIONS
def ResiduallyFinite (G : Type*) [Group G] : Prop :=
∀ g : G, g ≠ 1 → ∃ (H : Subgroup G), H.Normal ∧ H.index ≠ 0 ∧ g ∉ H

def IsPolycyclic (G : Type*) [Group G] : Prop :=
sorry -- Definition involves existence of a specific subnormal series

def VirtuallyPolycyclic (G : Type*) [Group G] : Prop :=
∃ (H : Subgroup G), H.index ≠ 0 ∧ IsPolycyclic H

-- THE STATEMENT (Kourovka 1.31)
theorem kourovka_1_31_open_problem (G : Type*) [Group G] :
(ResiduallyFinite G ∧ WellFoundedGT (Subgroup G)) → VirtuallyPolycyclic G :=
sorry
```

**Summary of Missing Components:**
* `IsPolycyclic` (Critical)
* `ResiduallyFinite` (Needs definition)
* `Virtually` / `Almost` modifier (Needs definition)

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