Can one equation kill a group?
Two AI preprints claim Kervaire’s conjecture and Howie’s conjecture on equations over groups
Covers result 256 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.
5:16. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
To solve x² = −1 you enlarge the real numbers. Groups have equations too, mixing an unknown x with fixed elements of the group, and the question is whether some bigger group, containing the original one unchanged, has a solution. Over the six symmetries of a triangle, 36 of the 216 equations x g₁ x g₂ x⁻¹ g₃ = 1 have no solution among those six. None of them can be solved by shuffling fewer than nine points; with nine points, every one can (our computation).
Some equations can never be solved: x a x⁻¹ = b fails whenever a and b have different orders. The rule of thumb is to count the x’s, with inverses counting minus one. In 1962 Gerstenhaber and Rothaus showed that in the unit quaternions the solutions, counted with signs, number exactly that exponent sum (in bigger compact groups, a power of it), so groups that fit inside such matrix groups were handled. Kervaire asked, from his work on knots in the 1960s, whether adding one generator and one relation can ever kill a nontrivial group. Howie conjectured in 1981 that every system whose exponent-sum matrix has full rank has a solution in some overgroup. Klyachko proved Kervaire’s case for torsion-free groups in 1993, and a 2026 paper by Chen saw no significant breakthrough since.
Result 256 is two OpenAI preprints. The first, 13 pages, dated September 24, 2026, claims that for every group, adding one generator t and one relation whose t-exponent sum is ±1 keeps the group embedded, and so Kervaire’s conjecture. The second, 16 pages, dated October 5, claims Howie’s conjecture: every system whose exponent-sum matrix has full rank over the rationals has a solution in an overgroup.
What it doesn’t claim
Overgroups that are nilpotent or solvable, which a related problem asks for; any control over what the overgroup looks like; or anything about singular systems, which can genuinely fail. Our singular example: over the triangle’s symmetries, x a x⁻¹ = b, with a a flip and b a rotation, collapses the whole group.
Where it stands
- Posted as preprints
- OpenAI, two papers, 13 and 16 pages, dated September 24 and October 5, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- In part: the first paper’s main theorem (docs)
Last checked October 19, 2026. Neither preprint has been revised. In Lean, the first paper’s main theorem is formalized: about 11,300 lines with no unproved steps, which we did not build. Howie’s theorem is not formalized, and neither paper is in the repository’s formalization list. OSVerify has not reviewed them. The Kourovka Notebook’s website hosts both papers as proposed solutions, with a warning that AI preprints there may be unverified, and the Notebook itself does not mark the problems solved. Lvzhou Chen, who has worked on these problems, wrote of mixed feelings about the profession and said he had read only parts of the release. An earlier claimed proof, by Kawauchi, has not won acceptance.
How the proofs go
- Never exactly one. Glue disks, each spelling the relation, with bands into a surface without handles; its boundary circles spell words in the group. The papers show that such a surface never has exactly one nontrivial boundary word: if all the others are trivial, so is the last.
- Counting turns. The proof measures an operator by the total angle of its eigenvalues, a spectral phase. A fixed-space lemma, proved by counting solutions modulo two, together with subadditivity, bounds that phase from above. Computed circle by circle, each trivial boundary adds a full turn, and the Euler characteristic makes these fill the whole bound, so the last word has zero phase and is trivial.
- No matrices needed. The operator acts on the group’s own space of square-summable functions, so the group never has to be approximated by matrices, which was the barrier for the old method. The second paper extends the fixed-space step to several unitary blocks, using the cohomology of the unitary group and nested nonzero minors of the exponent matrix.
The numbers in the video
- Ours: on the unit quaternions, x a x b x⁻¹ c had three solutions with signs +, +, −, net 1.
- Ours: with exponent sum 1, the number of good angles in the fixed-space lemma was odd in 40 of 40 random trials; with exponent sum 0 it was even, and zero in 17 of 40.
- Ours: about 8.7 million labelled surfaces without handles over the triangle’s symmetries had no exception; surfaces with handles gave 124,416 exceptions.
Read the source
- The Kervaire Theorem for Groups (PDF), 13 pages.
- Nonsingular Systems of Equations over Arbitrary Groups (PDF), 16 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 256.
The 2 papers in this result
OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.
- Nonsingular systems of equations over arbitrary groups main paper
- The Kervaire theorem for groups companion
Transcript
Read the full script
0:00The question
To solve x² = −1, you enlarge the real numbers. Groups have equations too, mixing an unknown x with fixed elements of the group, and the question is whether a bigger group, containing the original one unchanged, has a solution. Our computer looked at a group of 6 elements, the symmetries of a triangle: of 216 equations of the form x g₁ x g₂ x⁻¹ g₃, 36 have no solution among those 6. None can be solved by shuffling fewer than 9 points; with 9 points, every one of them can. Some equations can never be solved: x a x⁻¹ = b fails whenever a and b have different orders. The rule of thumb is to count the x’s, with inverses counting minus one. In 1962 Gerstenhaber and Rothaus showed that in the unit quaternions, the solutions counted with signs number exactly that exponent sum; in bigger compact groups, a power of it. Our check: x a x b x⁻¹ c had three solutions with signs +, +, −: net 1. So groups that fit inside such matrix groups were handled, but not every group. Kervaire’s conjecture, from his work on knots in the 1960s, asks whether adding one generator and one relation can ever kill a nontrivial group. Howie, in 1981, conjectured more generally that any system whose exponent-sum matrix has full rank has a solution in some overgroup. Klyachko proved Kervaire’s case for torsion-free groups in 1993, and a 2026 paper by Chen saw no significant breakthrough since.
1:39The claims
Result 256 is two OpenAI preprints. The first, 13 pages, dated September 24, 2026, claims that for every group, adding one generator t and one relation whose t-exponent sum is ±1 keeps the group embedded, and so Kervaire’s conjecture: other exponent sums give a quotient onto a nontrivial cyclic group anyway. The second, 16 pages, dated October 5, claims Howie’s conjecture: every system whose exponent-sum matrix has full rank over the rationals has a solution in an overgroup. Not claimed: overgroups that are nilpotent or solvable, which a related problem asks for; any control over what the overgroup looks like; or anything about singular systems, which can genuinely fail. Our singular example: over the triangle’s symmetries, x a x⁻¹ = b, with a a flip and b a rotation, collapses the whole group.
2:38How the proofs go
The heart of both papers is a statement about surfaces. Glue disks, each spelling the relation, with bands into a surface without handles; its boundary circles spell words in the group. The claim is that such a surface never has exactly one nontrivial boundary word: if all the others are trivial, so is the last. Our computer checked about 8.7 million labelled surfaces of this kind over the triangle’s symmetries and found no exception, while surfaces with handles gave 124,416 exceptions. The proof measures an operator by the total angle of its eigenvalues, a spectral phase. A fixed-space lemma, proved by counting solutions modulo two, together with subadditivity, bounds that phase from above; our check: with exponent sum 1, the number of good angles was odd in 40 of 40 random trials, and with exponent sum 0 it was even, often zero. Computing the phase circle by circle, each trivial boundary adds a full turn, the Euler characteristic makes these fill the whole bound, so the last word has zero phase and is trivial. The decisive point is that the operator acts on the group’s own space of square-summable functions, so the argument never needs the group to be approximated by matrices, which was the barrier for the old method. The second paper extends the fixed-space step to several unitary blocks, using the cohomology of the unitary group and nested nonzero minors of the exponent matrix.
4:12Where it stands
Both preprints are unrefereed and unchanged since release. In Lean, the first paper’s main theorem is formalized, about 11,300 lines with no unproved steps; Howie’s theorem is not formalized, and neither is in the repository’s formalization list; we did not build it. OSVerify has not reviewed them. The Kourovka Notebook’s website hosts the papers as proposed solutions, with a warning that AI preprints there may be unverified, and the Notebook itself does not mark the problems solved. Lvzhou Chen, who has worked on these problems, wrote of rather mixed feelings about the profession, and said he had read only parts of the release. An earlier claimed proof, by Kawauchi, has not won acceptance. If they hold, adding new generators and as many relations, with independent exponent sums, can never collapse a group: every nonsingular system over every group has a solution somewhere, about 60 years after Kervaire’s question.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.