The Kervaire conjecture: adjoining one generator and one relator never kills a nontrivial group
Let be a nontrivial group, let generate an infinite cyclic group, and let be any element of the free product . Kervaire's characterization of high-dimensional knot groups (1965) led to the group-theoretic question whether the quotient can ever be trivial, that is, whether can be normally generated by one element. Known cases included torsion-free (Klyachko, unimodular case), residually finite and hyperlinear (via Gerstenhaber-Rothaus and Pestov), and of special forms. Is nontrivial for every nontrivial group and every ?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Combinatorial group theory; equations over groups
- Posed by
- Michel Kervaire, Les noeuds de dimensions superieures (1965); the group-theoretic form is traced to this setting by Chen (2026)
- Year posed
- 1965
- Years open
- 61y
- Solved
- 2026-09-24
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 55 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Claims Theorem 1.1: for every group (no torsion, cardinality or presentation hypothesis) and every with exponent sum in , the canonical map is injective, so the equation is solvable in an overgroup. Corollary 1.2: the quotient is nontrivial for every when , which is the Kervaire conjecture. It does NOT prove injectivity for other nonzero exponent sums (the Kervaire-Laudenbach form); that is the companion's nonsingular-systems theorem. It does not assert a solution inside itself.
What the AI did
The release README says the manuscripts were produced by an unreleased internal OpenAI model, the vast majority by one fixed procedure using on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier results produced by the models. Its named exceptions to that procedure (the zeta zero-free region work, whose Re(s) > 11/12 write-up was human edited, and the Hodge conjecture for CM abelian varieties) do not concern this family. Both manuscripts of the family are credited to OpenAI with no human author named. The Kervaire manuscript proves the result directly through a spectral-phase inequality in the group von Neumann algebra and a fixed-space theorem for unitary matrices; the later nonsingular-systems manuscript (5 October 2026) names it as its direct antecedent.
Verification
No independent mathematician has checked this yet. Theorem 1.1 and Corollary 1.2 of the principal manuscript were read against the conjecture as posed: Corollary 1.2 is the nontriviality statement for every nontrivial and every word . The Lean challenge ComparatorChallenges/Kervaire.json (theorem OAI.Kervaire.coefficient_injective, solution module OAI.GroupTheory.Kervaire.Main, present at the pinned commit) is not in the formalization catalogue formalization.yaml; it was found through lean/docs/256.md. Its statement was read here: for every group and every in the coproduct of with multiplicative whose exponent sum is , the map from to the quotient by the normal closure of is injective. That is Theorem 1.1, which is stronger than the headline for unimodular words; the remaining exponent sums follow by the one-line surjection onto given in the paper, which is not itself formalised. Permitted axioms are propext, Quot.sound and Classical.choice. Not rebuilt here. The manuscript records that Kawauchi (2024) published a proposed resolution through ribbon sphere-link groups, which it does not use.