Add Kourovka Problem 2.24 on orderability of torsion-free Engel groups #2184

vikasprajapati-01 · 2026-02-06T17:40:11Z

Summary

add a Lean statement for Kourovka Notebook Problem 2.24 on orderability of torsion-free Engel groups.
define iterated commutator, Engel, torsion-free, and orderable predicates.
tag the open problem with category and AMS codes.

Tested using lake build and it was successfull.

Solves #2017

felixpernegger · 2026-02-06T20:16:50Z

FormalConjectures/Kourovka/2_24.lean

+
+variable (G : Type*) [Group G]
+
+/-- The `n`-fold iterated commutator `[x,_n y]`. -/


Use LaTeX formatting for docstrings

felixpernegger · 2026-02-07T12:40:29Z

FormalConjectures/Kourovka/2_24.lean

+variable (G : Type*) [Group G]
+
+/-- The $n$-fold iterated commutator $[x,_n y]$. -/
+def commutator_n (x y : G) : ℕ → G


This, as well as Torsion free groups (and most likely orderable groups) is in mathlib, dont define it yourself.

felixpernegger · 2026-02-07T12:41:29Z

FormalConjectures/Kourovka/2_24.lean

+*Reference:* Kourovka Notebook, Problem 2.24.
+
+Does every torsion-free Engel group admit a bi-invariant linear order? The question is intertwined
+with Plotkin's conjecture on the local nilpotence of Engel groups: a positive answer to Plotkin's


Formaluse the connection with research solved tag

vikasprajapati-01 · 2026-02-07T14:11:17Z

Thanks for the review @felixpernegger
I switched the torsion-free assumption to mathlib’s Monoid.IsTorsionFree (refered : https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Torsion.html ) and marked the problem with @[category research solved, AMS 20] as requested. I couldn’t find mathlib predicates for Engel groups or bi-invariant orderable groups. If you can point me to them, I’ll swap those in too.

felixpernegger · 2026-02-07T14:47:24Z

Another thing, do you (you!) understand what the problem is about and not just copy fron some LLM?

vikasprajapati-01 · 2026-02-07T17:04:47Z

Another thing, do you (you!) understand what the problem is about and not just copy fron some LLM?

What i have understood is that the goal here is to formalize the statement, and in this particular issue we have to check if a group has no torsion and whether we can get identity element by repeated commutators of any 2 elements.

Actually i am new to lean, so i am referring the documentations to learn more and solve the issue not LLM.

But If you still think the PR needs a lot of work, then i would be happy to close this PR for now. So that i can learn more about formal conjectures and lean and raise the PR later.

felixpernegger · 2026-02-07T17:06:47Z

nice, this is just a very common occurence in this repo, so I asked

felixpernegger · 2026-02-07T17:09:13Z

FormalConjectures/Kourovka/2_24.lean

+
+Does every torsion-free Engel group admit a bi-invariant linear order?
+-/
+@[category research solved, AMS 20]


What I actually meant: The conjecture should be under research open, but there should be a sperate statemnt (with sorry as proof), that the conjecture implies the other one (as you write on top of the file). This should be tagged with research solved.
There are many examples for this in the repository, maybe take a look at a few of them to get a sense for this

felixpernegger · 2026-02-07T17:09:28Z

FormalConjectures/Kourovka/2_24.lean

+@[category research solved, AMS 20]
+theorem kourovka_problem_2_24 :
+    answer(sorry) ↔
+      ∀ (H : Type*) [Group H], IsEngel H → Monoid.IsTorsionFree H → IsOrderable H := by


Suggested change

∀ (H : Type*) [Group H], IsEngel H → Monoid.IsTorsionFree H → IsOrderable H := by

∀ (H : Type) [Group H], IsEngel H → Monoid.IsTorsionFree H → IsOrderable H := by

felixpernegger · 2026-02-07T17:11:21Z

FormalConjectures/Kourovka/2_24.lean

+variable (G : Type*) [Group G]
+
+/-- The $n$-fold iterated commutator $[x,_n y]$. -/
+def commutator_n (x y : G) : ℕ → G


Commutator also exists in mathlib, under commutator. For the beginning, I recommend you to use the website leansearch.net (there are also some alternatives, say if you wanna know more) to find definitions and theorems in mathlib.

Thank you for the website (leansearch.net), this is really great. Now i am able to easily find the theorems in Mathlilb4.

felixpernegger · 2026-02-07T17:13:31Z

FormalConjectures/Kourovka/2_24.lean

+      z * y * z⁻¹ * y⁻¹
+
+/-- An Engel group: every pair of elements has some iterated commutator equal to the identity. -/
+def IsEngel : Prop :=


There is also LieAlgebra.IsEngelian in mathlib, but I doubt this is applicable here, so this is likely fine

felixpernegger · 2026-02-07T17:16:10Z

FormalConjectures/Kourovka/2_24.lean

+  ∀ x y : G, ∃ n : ℕ, commutator_n (G := G) x y n = 1
+
+/-- A group is orderable if it admits a bi-invariant strict total order. -/
+def IsOrderable : Prop :=


MulRightStrictMono and MulLeftStrictMono make this redundant.

vikasprajapati-01 · 2026-02-08T03:46:33Z

Changes are :

Main statement is tagged research open.
The implication “Plotkin ⇒ orderability” is a separate research solved lemma.
commutator_n now uses mathlib’s element commutator notation ⁅·, ·⁆ (open scoped Group).
Orderability uses MulLeftStrictMono/MulRightStrictMono.
torsion-free uses IsMulTorsionFree.
IsLocallyNilpotent is still a placeholder True (I can strengthen it to “every finitely generated subgroup is nilpotent” if you prefer).
I also kept PlotkinConjecture as a named def (happy to inline that assumption instead).

Add Kourovka Problem 2.24 statement

f71d09b

felixpernegger reviewed Feb 6, 2026

View reviewed changes

vikasprajapati-01 and others added 2 commits February 7, 2026 12:51

Use latex formatting for docstring

ea06166

Merge branch 'main' into kourovka-2-24

1c8a54a

felixpernegger reviewed Feb 7, 2026

View reviewed changes

Use mathlib torsion-free predicate and mark Kourovka 2.24 solved

5d9f110

felixpernegger reviewed Feb 7, 2026

View reviewed changes

Kourovka 2.24: use commutator notation and defining Plotkin's conjecture

93399ab


		variable (G : Type*) [Group G]

		/-- The `n`-fold iterated commutator `[x,_n y]`. -/

	∀ (H : Type*) [Group H], IsEngel H → Monoid.IsTorsionFree H → IsOrderable H := by
	∀ (H : Type) [Group H], IsEngel H → Monoid.IsTorsionFree H → IsOrderable H := by

Add Kourovka Problem 2.24 on orderability of torsion-free Engel groups #2184

Are you sure you want to change the base?

Add Kourovka Problem 2.24 on orderability of torsion-free Engel groups #2184

Uh oh!

Conversation

vikasprajapati-01 commented Feb 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

vikasprajapati-01 commented Feb 7, 2026

Uh oh!

felixpernegger commented Feb 7, 2026

Uh oh!

vikasprajapati-01 commented Feb 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

felixpernegger commented Feb 7, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

vikasprajapati-01 commented Feb 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

vikasprajapati-01 commented Feb 6, 2026 •

edited

Loading

vikasprajapati-01 commented Feb 7, 2026 •

edited

Loading