---
title: "Nonsingular systems of equations over arbitrary groups"
authors:
  - "OpenAI (internal model)"
year: 2026
venue: "openai/math manuscript collection (GitHub), result family 256; unreviewed"
arxiv: null
doi: null
source: "https://github.com/openai/math/blob/main/preprints/Nonsingular-systems-of-equations-over-arbitrary-groups-October-5-2026/nonsingular-systems-over-arbitrary-groups.pdf"
topics:
  - "openai-math"
  - "ai-generated-math"
  - "group-theory"
  - "lean4"
  - "formalized"
seed_rank: 2111
seed_batch: "openai-math-2026-10-07"
reviewed: "2026-10-07"
pool: "maths-foundations"
relevance_score: 8
lineage: ai-mathematical-reasoning
cites:
  - title: "Nonsingular systems of equations over arbitrary groups"
    url: "https://github.com/openai/math/blob/main/preprints/Nonsingular-systems-of-equations-over-arbitrary-groups-October-5-2026/nonsingular-systems-over-arbitrary-groups.pdf"
    year: 2026
    arxiv: null
    doi: null
  - title: "The Kervaire theorem for groups"
    url: "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"
    year: 2026
    arxiv: null
    doi: null
---

# Nonsingular systems of equations over arbitrary groups

## One-sentence takeaway

OpenAI's result family 256 (Group theory) claims: 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.

## Why it matters here

Pure mathematics with no direct engine use; it is in the library as part of the openai/math corpus, which records what an AI research model claims to have proved. More broadly, every card in this batch is evidence for the `ai-mathematical-reasoning` thread: per the repo README, an unreleased internal OpenAI model produced it, using about three hours of ChatGPT Pro thinking compute per result on average, across roughly 4,000 posed problems. The Lean development makes the claim machine-checkable, which is the pattern Broadside cares about for agentic verification loops.

## Key ideas

- Family summary (repo): 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.
- *Nonsingular systems of equations over arbitrary groups*: 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.
- *The Kervaire theorem for groups*: 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.
- Lean scope (lean/docs/256.md): 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.

## Caveats

- Unreviewed: these are AI-generated manuscripts posted to GitHub with no peer review or arXiv deposit. The repo README says results are "at different stages of verification" and that "some of the unformalized results could have issues."
- This card restates the repo's family summary, manuscript abstracts and Lean scope notes. It is not an independent check of the proofs, and the scope of each theorem is exactly as stated there.
- Lean: formalized in part. The repo has a scope note listing 1 Comparator challenge statement(s), and that note defines which statements are covered. Do not read the Lean coverage as the full content of every manuscript in the family.
- A grep of the repo's `lean/OAI` tree found no `sorry` and no top-level `axiom` declarations. The library was not compiled for this card, and Comparator was not run.

## Links

- Manuscript: [Nonsingular systems of equations over arbitrary groups](https://github.com/openai/math/blob/main/preprints/Nonsingular-systems-of-equations-over-arbitrary-groups-October-5-2026/nonsingular-systems-over-arbitrary-groups.pdf)
- Manuscript: [The Kervaire theorem for groups](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)
- Lean scope: https://github.com/openai/math/blob/main/lean/docs/256.md
- Comparator statement (Coefficient-group injectivity for unimodular one-relator quotients): https://github.com/openai/math/blob/main/lean/ComparatorChallenges/Kervaire.lean
- Family entry: https://github.com/openai/math/blob/main/CONTENTS.md
- Overview PDF: https://github.com/openai/math/blob/main/overview.pdf
- Repo: https://github.com/openai/math