∑math20

Group theory · Result 256

Nonsingular systems of equations over arbitrary groups

2 papersLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 2

First page of Nonsingular systems of equations over arbitrary groups

Nonsingular systems of equations over arbitrary groups

OpenAI · October 5, 2026

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.

Read PDF Download Source

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}
}
First page of The Kervaire theorem for groups

The Kervaire theorem for groups

OpenAI · September 24, 2026

We prove that no free product of a nontrivial group with an infinite cyclic group is normally generated by one element. This resolves the Kervaire conjecture positively.

Read PDF Download Source

Cite
@misc{OAI:The-Kervaire-Theorem-for-Groups-September-24-2026,
  author = {{OpenAI}},
  title = {{The Kervaire theorem for groups}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Kervaire-Theorem-for-Groups-September-24-2026/The-Kervaire-Theorem-for-Groups-September-24-2026.pdf}{OAI:The-Kervaire-Theorem-for-Groups-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

Kervaire's conjecture states that the free product of a nontrivial group with an infinite cyclic group cannot be normally generated by one element. The linked formalization proves the stronger coefficient-injectivity statement used in the paper: for any group \(A\) and any relator in \(A*\mathbb Z\) whose exponent sum in the cyclic generator is \(1\) or \(-1\), the natural map from \(A\) into the quotient by that relator is injective. This is the selected unimodular-relator result underlying the conjecture.

Comparator links

ResultComparator statement
Coefficient-group injectivity for unimodular one-relator quotientsKervaire.lean

Scope note on GitHub →