The Kervaire conjecture

The Kervaire conjecture in group theory asserts that adding one generator and one relator to a nontrivial group never gives the trivial group: if A ≠ 1, then (A ∗ ⟨t⟩)/⟨⟨w⟩⟩ ≠ 1 for every w ∈ A ∗ ⟨t⟩. (It is unrelated to the Kervaire invariant problem of homotopy theory.) Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math) make claims on this question. The first, dated 24 September 2026, claims a proof of the conjecture through coefficient injectivity for unimodular relators. The second, dated 5 October 2026, claims the solvability of every finite nonsingular system of equations over every group. This page summarizes the published claims and lists publicly available follow-up work.

Background

• As recounted in the introductions of both manuscripts:
  • Kervaire's characterization of high-dimensional knot groups (1965) includes normal generation by a single element. Chen traces the group-theoretic Kervaire problem to this setting.
  • Solvability. An equation w(t) = 1 over A is solvable if A embeds in a group containing a solution. This is equivalent to the injectivity of the coefficient map A → (A ∗ ⟨t⟩)/⟨⟨w⟩⟩.
  • Exponent sums. The word w is called unimodular when the exponent sum of t in w is ±1, and nonsingular when that exponent sum is nonzero.
  • The stronger forms. The Kervaire–Laudenbach conjecture asks for coefficient injectivity for every nonsingular equation in one variable. Howie's conjecture asks for a simultaneous solution of every finite system whose exponent-sum matrix has full row rank over Q; the October manuscript cites Klyachko, Mikheenko and Roman'kov (2024) for this formulation.
  • For statements about all groups, the nontriviality assertion is equivalent to unimodular coefficient injectivity, by a standard reduction through an embedding into a simple group recorded by Klyachko (2005).
• Known cases recalled in the manuscripts:
  • Gerstenhaber and Rothaus (1962): nonsingular systems over finite groups (and square systems over compact connected Lie groups), hence the injectivity for residually finite coefficient groups;
  • Pestov (2008), Nitsche and Thom: the hyperlinear case;
  • Howie (1981): finite independent systems over locally indicable groups;
  • Klyachko (1993): one unimodular equation over a torsion-free group, with a new proof by Chen through the complexity of surfaces;
  • Klyachko and Lurye (2012): injectivity for arbitrary coefficient groups after imposing w^m = 1 with m ≥ 2.
• The September manuscript notes that Kawauchi (2024) has published a proposed resolution of the nontriviality assertion through ribbon sphere-link groups. It states that its own argument takes a different route, in which neither the collapse construction nor the ribbon-asphericity assertions enter.

The original results

• Kervaire conjecture (24 September 2026). Theorem 1.1: for every group A and every unimodular word w ∈ A ∗ ⟨t⟩, the canonical homomorphism A → (A ∗ ⟨t⟩)/⟨⟨w⟩⟩ is injective. No restriction on torsion, cardinality or presentation of A is imposed.
  • Corollary: the Kervaire conjecture. For an exponent sum d ≠ ±1, the quotient maps onto a nontrivial cyclic group of order |d|, or onto Z when d = 0.
  • The manuscript describes Theorem 1.1 as the unimodular case of the Kervaire–Laudenbach form. Its conclusion concerns solvability in an overgroup, not a solution inside A.
• Method, as described in that manuscript. A coefficient killed by w = 1 yields a planar diagram of word disks joined by bands. The central assertion is that on a connected planar surface of this kind, one boundary word cannot be the only nontrivial one.
  • Travel along the boundaries is encoded by a permutation weighted by the left regular representation of A. This representation supplies a faithful finite trace for every group, with no approximation hypothesis.
  • It is measured by the trace of the fractional spectral phase of a unitary, which the manuscript proves subadditive.
  • A fixed-space lemma is proved by a degree calculation: given signs s₁, …, s_n with sum ±1 and P ∈ U(nk), some X ∈ U(k) makes diag(X^s₁, …, X^s_n)P have at least k fixed directions.
  • Euler characteristic identifies the common term of the resulting upper bound and of a direct boundary-by-boundary calculation. The exceptional word is therefore trivial.
• Nonsingular systems (5 October 2026). Theorem 1.1: let G be any group and let w₁, …, w_m ∈ G ∗ F_n, with 1 ≤ m ≤ n. If their exponent-sum matrix has row rank m over Q, then G → (G ∗ F_n)/⟨⟨w₁, …, w_m⟩⟩ is injective. Equivalently, the system has a simultaneous solution in an overgroup of G.
  • The manuscript presents this as the finite case of Howie's conjecture. A remark extends it to arbitrary sets of equations and variables with independent exponent rows. The one-equation case includes the Kervaire–Laudenbach conjecture.
  • The proof follows the same plan as in September, with a fixed-space estimate for systems: full row rank forces equal numbers of positive and negative disks of each relator type.
• Sources. Commit 1581d4c of the openai/math repository:
  • The Kervaire theorem for groups;
  • Nonsingular systems of equations over arbitrary groups.
• Formalization, as described by the repository.
  • The scope note lean/docs/256.md links the September manuscript. It states that the formalization proves "the stronger coefficient-injectivity statement used in the paper", for any group and any relator with exponent sum 1 or −1.
  • The Comparator challenge Kervaire.lean states coefficient_injective. For every group A (in any universe) and every w in Monoid.Coprod A (Multiplicative ℤ) with exponent sum 1 or −1, the composite of the inclusion of A with the quotient map by the normal closure of w is injective. This is Theorem 1.1 of the September manuscript. The October system theorem is not among the selected statements.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 16 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates the family "partial" against its summary of Howie's conjecture. Only the Kervaire special case is stated: one equation in one unknown with exponent sum ±1. The finite-system headline is not stated, while "the Kervaire companion claim is covered (coefficient injectivity implies nontriviality)". Records a sandboxed Comparator pass for Kervaire.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, fuel, memory, errors) does not list Kervaire. The challenge was therefore accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-10	cert-machine, openai/math lane K, run 38019899278	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the Kervaire solution (464 s). The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.

Notes

• The kernel checks above concern the formal statement coefficient_injective as written. The October system theorem has no formal statement in the collection.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.