Browse › Group theory › 256 Nonsingular systems of equations over arbitrary groups
Nonsingular systems of equations over arbitrary groups
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
Every finite nonsingular system of equations over an arbitrary group has a simultaneous solution in an overgroup. This proves Howie's conjecture on nonsingular systems.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Comments and discussion
- Kourovka Notebook (eds. E. I. Khukhro, V. D. Mazurov), Unsolved Problems in Group Theory, 21st edition: updates file, Problem 18.87 (Kourovka Notebook update, 2026). Problem 18.87(a) (V. A. Roman'kov), the Kervaire–Laudenbach conjecture for independent systems over an arbitrary group, is marked "The conjecture is proved (AI solution confirmed by N. V. Bogachev: OpenAI, Preprint, 2026)". The entry links a copy of this paper; the nilpotent and solvable versions 18.87(b),(c) carry no solution mark.
Formalization
- OpenAI math release, Lean scope notes for family 256 (
lean/docs/256.md) (release Lean documentation, 6 Oct 2026). The notes describe a formalization of coefficient injectivity for a single unimodular relator in $A*\mathbb Z$, the companion Kervaire paper's theorem and a special case of this paper's claim; they list no formalization of the multi-relator nonsingular-system theorem. [family-level] - OpenAI, lean/OAI/GroupTheory/Kervaire/Main.lean (github.com/openai/math, 2026). Proves
Kervaire.coefficient_injective(one unimodular word) andKervaire.quotient_nontrivial, i.e. the $m=n=1$ unimodular case that this paper extends. [family-level]
Possibly relevant literature (found by the agent, not checked)
- A. Klyachko and A. Thom, New topological methods to solve equations over groups (arXiv:1509.01376; Algebr. Geom. Topol. 17 (2017), 331–353). Extends the Gerstenhaber–Rothaus compact-Lie-group method for equations over hyperlinear groups, which the paper's history section discusses via Pestov and Nitsche–Thom.
- M. A. Mikheenko, Infinite systems of equations in abelian and nilpotent groups (arXiv:2410.20729, 2024–2025). Studies infinite unimodular/nonsingular systems; may be relevant to the paper's Remark extending Theorem 1 to arbitrary sets of equations with independent exponent rows.
Digests and expositions
- Open Mathematics Courses, Nonsingular systems of equations over groups (undated). Five-lesson exposition of the manuscript covering rational cohomology, simultaneous fixed spaces and the planar boundary obstruction; it identifies its author and self-checker as Claude Opus 5.5, with independent review incomplete. [AI-generated per source]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 256
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:Nonsingular-systems-of-equations-over-arbitrary-groups-October-5-2026,
author = {{OpenAI}},
title = {{Nonsingular systems of equations over arbitrary groups}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/Nonsingular-systems-of-equations-over-arbitrary-groups-October-5-2026/nonsingular-systems-over-arbitrary-groups.pdf}{OAI:Nonsingular-systems-of-equations-over-arbitrary-groups-October-5-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/256.md. The Lean statements have not been checked by people against the paper's claims.
Family 256: Nonsingular systems of equations over arbitrary groups
Proves that every finite system of equations over an arbitrary group whose exponent-sum matrix has full row rank over ℚ has a simultaneous solution in an overgroup, resolving Howie's conjecture. The coefficient group embeds in the presented quotient. A companion proves Kervaire's conjecture: adjoining one generator and one relation cannot trivialize a nontrivial group.
Other papers in this family:
- The Kervaire theorem for groups · September 24, 2026