---
id: "2026-11-07-herzog-schonheim-conjecture-solvable-groups-ai-lean"
url: "https://postcutoff.com/e/2026-11-07-herzog-schonheim-conjecture-solvable-groups-ai-lean/"
as_of: "2026-11-15T00:33:00+01:00"
date: "2026-11-07"
date_precision: day
category: science
importance: 4
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 2
editor: human editor
human_review: null
version: null
---

As of: 2026-11-15 00:33 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-11-07-herzog-schonheim-conjecture-solvable-groups-ai-lean/

# Herzog–Schönheim for solvable groups (GPT-5.6 Sol, Claude, Lean)

Full title: Herzog–Schönheim conjecture (1974) proved for all solvable groups, with key steps from GPT-5.6 Sol and Claude Opus 5 and 5.5 and a full Lean 4 formalization

arXiv 2611.11002 (7 Nov 2026), Murali Menon: the Herzog–Schönheim conjecture holds for all solvable groups, finite or infinite. The acknowledgments credit GPT-5.6 Sol with the reciprocal-sum comparison (Section 3), the cyclotomic divisibility argument and the argument for the prime 7; Claude Opus 5 and Opus 5.5 with formalizing the solvable track and completing the theorem for arbitrary solvable groups; the whole proof is formalized in Lean 4 with mathlib (repository Jostamon/erdos274-hs-solvable).

## 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

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 191 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 130 days after its cutoff
- Gemini 4 Hydrogen (training cutoff March 2026): 221 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 160 days after its cutoff

## Sources

1. [arXiv 2611.11002: The Herzog–Schönheim Conjecture for Solvable Groups (Murali Menon)](https://arxiv.org/abs/2611.11002) (arxiv.org, paper)
2. [GitHub: Jostamon/erdos274-hs-solvable (Lean 4 formalization)](https://github.com/Jostamon/erdos274-hs-solvable) (github.com, code)

## Changes

- 2026-11-14 (filed): Created (science agent; abstract and PDF acknowledgments read)

## Related

- 2026-11-14: [AI-assisted results, 14 Nov](https://postcutoff.com/e/2026-11-14-ai-assisted-results-november-14-listing/index.md)