Kourovka 1.28 - Axiomatization

### What is the conjecture
Does a finite axiomatization exist for a free nilpotent group?

Kourovka Notebook Problem **1.28**, posed by **M. I. Kargapolov**, is a well-known open problem in group theory and mathematical logic.

A **free nilpotent group** $N_{r,c}$ (of rank $r$ and class $c$) is the "most general" group generated by $r$ elements that satisfies the condition that all commutators of length $c+1$ are the identity.
The **universal theory** consists of all logical statements of the form "For all $x, y, z...$ [some equation holds]" that are true in that group.
Kargapolov's problem asks for a list of these true statements (axioms) that implies all the others.

While the problem dates back to the 1960s (appearing in the 1st or 2nd issue of the Kourovka Notebook), it remains a subject of investigation. Significant progress has been made, particularly regarding specific ranks and nilpotency classes, but a complete description for the general case is still a topic of study.

* **Recent Work:** A notable recent paper is *"The Universal Theory of a Free Nilpotent Group: A Progress Report"* by **Anthony M. Gaglione and Dennis Spellman** (published in the *Far East Journal of Mathematical Sciences*, 2023). This paper explicitly addresses Problem 1.28, reviewing previous results and offering new partial solutions.
* **Related Results:**
* **Class 2:** The universal theory of free nilpotent groups of class 2 (where commutators commute) is better understood. For example, research has shown links between the decidability of these theories and the universal theory of the rationals $\mathbb{Q}$.
* **Axiomatization:** Researchers like **A. G. Myasnikov** and **V. N. Remeslennikov** have done foundational work on the universal theories of free groups (Problem 1.27) and have proposed candidate axiom systems (quasi-identities) for the nilpotent case.

* **"Describe":** In model theory, asking to "describe" a theory usually means one of two things:
1. **Axiomatization:** Find a specific, explicit set of axioms (usually universal sentences or quasi-identities) that completely generate the theory. (e.g., "The theory is axiomatized by the group axioms plus these specific identities...").
2. **Decidability:** Determine if there exists an algorithm that can decide whether any given universal sentence is true in the group.

However, the solution often turns into an existence question in practice:
* **Does a finite axiomatization exist?** (The problem might be resolved by proving no finite set of axioms can describe the theory).
* **Does a decision algorithm exist?** (The problem might be resolved by proving the theory is undecidable).

**Current Status:**
* For **free nilpotent groups** (Problem 1.28), the answer depends heavily on the nilpotency class $c$. For high classes, the theory can be extremely complex, and complete "descriptions" (like explicit axioms) are still the subject of papers like the 2023 Gaglione & Spellman report.

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

To state Kourovka Problem 1.28 in Lean 4, you do not need any new fundamental mathematical structures (like new types of logic or algebra). **Mathlib4 already contains all the necessary building blocks** (Free Groups, Nilpotency, First-Order Logic, and Model Theory).

However, to "state" the question, you would need to write several **"glue" definitions** that are currently missing as pre-bundled objects in the library. You cannot simply `import` a file and immediately reference `FreeNilpotentGroup` or `UniversalTheory`.

Here are the specific definitions and structures that are "missing" (i.e., you would have to define them yourself using existing components) to state the problem.

### 1. The Explicit Definition of a Free Nilpotent Group
Mathlib has `FreeGroup` and the concept of the `lowerCentralSeries`, but it does not have a standalone definition for the **Free Nilpotent Group** of rank $r$ and class $c$ ($N_{r,c}$).

You would need to define this by constructing the quotient of the free group by the $(c+1)$-th term of its lower central series.

* **Existing components:**
* `GroupTheory.FreeGroup`: To create $F_r$.
* `GroupTheory.Nilpotent`: To access `lowerCentralSeries`.
* `GroupTheory.QuotientGroup`: To take the quotient $F_r / \gamma_{c+1}(F_r)$.
* **Missing Definition (You must write):**
* A type `FreeNilpotentGroup (r : Type) (c : ℕ)` which is defined as the quotient instance.

### 2. The Definition of "Universal Sentence" (The $\Pi_1$ Hierarchy)
Mathlib's model theory library is robust, but it handles formula complexity via the arithmetic hierarchy ($\Sigma_n$ and $\Pi_n$). It does not have a simple predicate named `IsUniversal`.

To state the problem, you need to filter the set of all sentences to find the "Universal" ones.

* **Existing components:**
* `ModelTheory.Syntax`: Defines `Sentence` and `Formula`.
* `ModelTheory.Order.Complexity`: Defines `IsPi` and `IsSigma`.
* **Missing Definition (You must write):**
* A helper `def IsUniversal (φ : Sentence L) : Prop := φ.IsPi 1`.
* (Alternatively, you might need to handle the distinction between "Universal" and "Universal-Existential" depending on exactly how strict you want the definition, but usually $\Pi_1$ suffices).

### 3. The Definition of "The Universal Theory" of a Structure
Mathlib has the concept of the *complete* theory of a structure (`ModelTheory.Theory`), which is the set of *all* sentences true in that structure. It does not have a pre-defined function that extracts only the *universal* subset.

* **Existing components:**
* `FirstOrder.Language.Theory`: The type for a set of sentences.
* `FirstOrder.Language.Structure.realize`: The relation $\models$ (truth).
* **Missing Definition (You must write):**
* A definition `UniversalTheory (M : Type*) [Structure L M] : Theory L` which equals `{ φ | M ⊨ φ ∧ IsUniversal φ }`.

### 4. Finite Axiomatizability (Relative to Universal Theory)
Mathlib defines what it means for a theory to be satisfiable, but stating "Finite Axiomatizability" for a specific *subset* of logic requires careful assembly. You are asking if there exists a *finite* set of universal axioms that entails the rest.

* **Existing components:**
* `FinSet`: For finite sets.
* `models`: Semantic entailment ($\Gamma \models \phi$).
* **Missing Definition (You must write):**
* A predicate `IsFinitelyAxiomatizable (T : Theory L)`:
$\exists (A : \text{FinSet (Sentence L)}), (A \subseteq T) \wedge (\forall \phi \in T, A \models \phi)$.

---

### Summary: How to State it in Lean 4
If you were to write this in Lean 4 today, the code would look roughly like this (pseudo-code):

```lean
import Mathlib.ModelTheory.Syntax
import Mathlib.ModelTheory.Satisfiability
import Mathlib.GroupTheory.FreeGroup
import Mathlib.GroupTheory.LowerCentralSeries

open FirstOrder Language ModelTheory Group

-- 1. DEFINE THE GROUP (The Missing Object)
-- Define N_{r,c} as FreeGroup(r) / lowerCentralSeries(c+1)
def FreeNilpotentGroup (r : Type) (c : ℕ) : Type :=
QuotientGroup.Quotient (lowerCentralSeries (FreeGroup r) (c + 1))

-- 2. DEFINE UNIVERSAL SENTENCES (The Missing Predicate)
-- A universal sentence is a Π_1 sentence in the arithmetic hierarchy
def IsUniversal (φ : Sentence Language.group) : Prop :=
φ.IsPi 1

-- 3. DEFINE THE UNIVERSAL THEORY (The Missing Collection)
-- All universal sentences true in M
def UniversalTheory (M : Type) [Group M] : Set (Sentence Language.group) :=
{ φ | (M ⊨ φ) ∧ IsUniversal φ }

-- 4. STATE THE PROBLEM
-- Does there exist a finite set of universal sentences Γ such that
-- Γ entails every other sentence in the Universal Theory of N_{r,c}?
theorem Kourovka_1_28_Existence (r : Type) [Fintype r] (c : ℕ) :
∃ (Γ : FinSet (Sentence Language.group)),
(∀ ψ ∈ Γ, IsUniversal ψ) ∧
(∀ φ ∈ UniversalTheory (FreeNilpotentGroup r c), (Γ : Set _) ⊨ φ) :=
sorry
```

**Conclusion:**
There are **no missing definitions** in the sense of "mathematical concepts not supported by Lean." The only things missing are the specific **convenience definitions** (glue code) shown above to link Model Theory and Group Theory together for this specific 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

Start by checking the proposed imports for FreeGroup, lowerCentralSeries, quotient groups, and ModelTheory.Syntax against the current Mathlib APIs. Verify the definitions and statement for FreeNilpotentGroup, universal sentences, UniversalTheory, and finite axiomatizability, then ensure the resulting Lean conjecture compiles and faithfully states Kourovka Problem 1.28.

Written by the indexing model from the issue text.