Kourovka 2.5

### What is the conjecture
**"According to Plotkin, a group is called an NR-group if the set of its nil-elements coincides with the locally nilpotent radical, or, which is equivalent, if every inner automorphism of it is locally stable. Can an NR-group have a nil-automorphism that is not locally stable?"**

**Terminology:**
* **NR-group:** A group where the set of nil-elements (Engel elements) is exactly the locally nilpotent radical (Hirsch-Plotkin radical). Equivalently, every inner automorphism is locally stable.
* **Nil-automorphism:** An automorphism $\phi$ of a group $G$ such that for every $g \in G$, there exists an integer $n > 0$ (depending on $g$) such that $[\dots[g, \phi], \dots, \phi] = 1$ ($n$ times).
* **Locally stable automorphism:** An automorphism $\phi$ is locally stable if for every finitely generated $\phi$-invariant subgroup $H$, $\phi$ acts as a stable automorphism (i.e., stabilizes a normal series of $H$).

The problem essentially asks if the property of "inner automorphisms being locally stable" (which characterizes NR-groups) implies that *all* nil-automorphisms are locally stable in such groups.

See also #2014.

### Prerequisites needed
To state the problem from Kourovka Notebook 2.5 in Lean 4, the following definitions and structures are currently **missing** from Mathlib and would need to be defined manually:

1. **Engel Elements (Nil-elements):**
Mathlib has `IsNilpotent`, but it does not have a bundled definition for the set of **Right Engel elements** (often denoted $R(G)$ or the set of nil-elements). You would need to define:
$$ \{ g \in G \mid \forall x \in G, \exists n \in \mathbb{N}, [x, {_n} g] = 1 \} $$
where $[x, {_n} g]$ denotes the right-normed commutator $[...[[x, g], g], ... g]$.

2. **Hirsch-Plotkin Radical (Locally Nilpotent Radical):**
While `IsNilpotent` exists, the concept of **local nilpotency** (every finitely generated subgroup is nilpotent) and the **Hirsch-Plotkin radical** (the unique maximal normal locally nilpotent subgroup) are not defined as standard objects in Mathlib. You would need to define the radical as the join (supremum) of all normal locally nilpotent subgroups.

3. **Stability of Automorphisms on Series:**
Mathlib has `Group` and `Automorphism`, but it lacks the specific definition of an automorphism being **stable** with respect to a normal series (i.e., acting trivially on the factors $H_{i+1}/H_i$ of a series $1 = H_0 \unlhd H_1 \unlhd \dots \unlhd H_k = H$).

4. **Locally Stable Automorphism:**
Consequently, the definition of a **locally stable** automorphism is missing. This requires defining that for every finitely generated, $\phi$-invariant subgroup $H$, the restriction of $\phi$ to $H$ is a stable automorphism (stabilizes some normal series of $H$).

5. **Nil-automorphism:**
The definition of a **nil-automorphism** is missing. This describes an automorphism $\phi$ that acts as a nil-element in the holomorph of the group:
$$ \forall g \in G, \exists n \in \mathbb{N}, [\dots[g, \phi], \dots, \phi] = 1 $$

**Summary of what needs to be written:**
To state the question, one must define **`IsRightEngel`**, **`HirschPlotkinRadical`**, **`IsStable`** (for a series), **`IsLocallyStable`** (for an automorphism), and **`IsNilAutomorphism`**. The core `Group` and `IsNilpotent` structures are present.

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

No repository files or tests are named. Start by reviewing the existing Group and IsNilpotent structures, then determine how the five missing definitions—IsRightEngel, HirschPlotkinRadical, IsStable, IsLocallyStable, and IsNilAutomorphism—fit the project; done means the Kourovka 2.5 conjecture is stated in Lean.

Written by the indexing model from the issue text.