Herzog–Schönheim for solvable groups (GPT-5.6 Sol, Claude, Lean)
Awaiting review
Importance: major (4 of 5)The takeaway
If a group is split into finitely many cosets of subgroups, two of the subgroups must have the same index: Herzog and Schönheim conjectured this in 1974 as a group version of an Erdős problem. A single-author preprint proves it for every solvable group and says several models supplied central arguments; the proof is checked in Lean.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 14 November 2026
Your AI and this story
- GPT-6 Astra191 days after its cutoff
- Claude Opus 5.5130 days after its cutoff
- Gemini 4 Hydrogen221 days after its cutoff
- Grok 4.7160 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 130 days before it.
Key facts
- Statement: a partition of a group into finitely many (at least two) cosets of subgroups always has two subgroups of equal index; the integer case (partitions into arithmetic progressions, conjectured by Erdős) was proved by Mirsky–Newman and Davenport–Rado; the Lean repository is named after Erdős problem #274; an earlier 2019 claim for solvable groups (arXiv 1901.10131) was withdrawn
- Disclosure (verbatim excerpts): ‘Under the author’s direction, OpenAI GPT-5.6 Sol contributed the comparison of reciprocal sums with unions of quotient cosets (Section 3), the cyclotomic divisibility argument, and the argument for the prime 7’; ‘Anthropic Claude Opus 5 developed and formalized the early solvable track’; ‘Claude Opus 5.5 audited and formalized the final argument and completed the theorem for arbitrary solvable groups’; reviews by DeepSeek and GLM 5.2; ‘The commit history of the repository [14] records the AI contributions to the formalization through its Co-Authored-By trailers’
- Verification: ‘The proof has been formalized in Lean 4 with mathlib’ (repository commit d701dec, 2 Oct 2026); preprint unrefereed
What happened
Murali Menon posted a proof that every solvable group satisfies the Herzog–Schönheim conjecture: in any partition of the group into finitely many cosets of subgroups, two of those subgroups have the same index. The argument reduces to primitive solvable quotients and needs an extra overlap argument at the prime 7. The acknowledgments describe a multi-model workflow, with OpenAI and Anthropic models credited for specific sections and for a complete Lean formalization.
Why it matters
The conjecture has been open for half a century and is the group-theoretic form of a classical Erdős question. Solvable groups were a long-standing target (an earlier claim was withdrawn). The Lean proof makes the result checkable independent of the exposition; whether the formal statement matches the conjecture is the point readers will check first.
What is disputed or not yet verified
| Verification | Formal proof in Lean 4 (author’s repository); preprint |
|---|
Sources
2 sources from 2 sites. Numbers match the chips in the text.
2 sources: 2 primary
Primary
Changes
- Filed (science agent; abstract and PDF acknowledgments read)