Two colours do not determine the rest
In a finite simple matrix group over GF(8), a swap on an entire involution class preserves product orders 2 and 3 but changes an edge from order 5 to order 7.
Scope
A counterexample to the universal assertion, acting on the whole involution class in a concrete nonabelian finite simple matrix group. Simplicity and the two smallest prime divisors, 2 and 3, are proved directly; no identification with a named Ree group or exact group order is assumed.
Verified against the accepted commit, not a fresh full-repository build.
Formal record
- Lean statement
- Kourovka/Problem2153/Core.lean
- Lean proof
- Kourovka/Problem2153/Final.lean
- Endpoint
- Kourovka.Problem2153.not_statement
- Source commit
- fab8915562b0b7202ae4c1c7d7765c4bd8e616ea
- Verification
- Integrity passed (verification record)
- Statement review
- Independent review
- Novelty
- No earlier complete solution located in a bounded search (report); no priority claim is made
- Human acceptance
- 17 September 2026, human statement verifier (acceptance record)
- Agent version
- Nilradical v1.0.0; execution workflow 0.4.0-draft
Protected comparison, the three-axiom audit, and checks by Lean and Nanoda passed for the frozen endpoint. The Auckland replay passed all 159 modules in its complete dependency closure. This was not a fresh full-repository build. The execution used workflow 0.4.0-draft. Independent mathematics and statement reviews passed. Final human statement acceptance was recorded on 2026-09-17 for the linked proof snapshot.
All 719 frozen source and configuration files were checked byte for byte against the accepted proof commit. The target and its complete dependency closure passed verification; this is not a fresh full-repository build.
Credit
Counterexample, proof, Lean formalization and verification by Nilradical v1.0.0. The group constructions and structural ingredients are prior mathematics credited in the proof record; reused formal foundations retain their source credits.
- Nilradical v1.0.0 — counterexample, proof, formalization and verification
- I. B. Gorshkov — original question
- R. A. Wilson and K. Coolsaet — prior matrix group constructions
- TauCeti contributors — reused abstract Tits-system and Bruhat proofs
- mathlib contributors — formal foundations
Note
Read the mathematical note, an agent-written account of the result and its proof. It is informal and not refereed.
Cite
Nilradical. Nilradical v1.0.0: solution and Lean proof of Kourovka Problem 21.53. Repository snapshot fab8915562b0.
@misc{nilradical_v1_0_0_kourovka_21_53,
author = {{Nilradical}},
title = {Nilradical v1.0.0: solution and Lean proof of Kourovka Problem 21.53},
year = {2026},
howpublished = {Mathematical result with Lean formalization},
url = {https://github.com/alunik/kourovka-lean/blob/4c13da19c50b417e48ff2431a6ea76edade3eb81/Kourovka/Problem2153/README.md},
note = {Source commit fab8915562b0b7202ae4c1c7d7765c4bd8e616ea; Nilradical v1.0.0}
}