---

Claim. Theorem 1.1 of R. Itabe, The Herzog–Schönheim conjecture for coset partitions with at most seventeen cells, version 0.4.2 (review candidate, 17 August 2026), states: "Let $G$ be an arbitrary group and let (1.1) be a coset partition with $2 \leq r \leq 17$. Then there are distinct $i$, $j$ such that $[G : H_i] = [G : H_j]$." Here (1.1) is a finite family of left cosets of finite-index subgroups covering every element of $G$ exactly once. Equivalently, every counterexample to the Herzog–Schönheim conjecture needs at least eighteen cells. The manuscript calls itself an unreviewed computer-assisted proof candidate for this bounded result only. The proof passes to the finite quotient by the common core of the subgroups, removes index two by descent to an index-two subgroup, and restricts the sorted indices of a cell-minimal counterexample by the reciprocal identity, pairwise non-coprimality and four harmonic obstructions of Margolis and Schnabel. An exact search then leaves no index profile with at most sixteen cells and five profiles with seventeen, all containing an index-four cell; a second exact search over the ways the other cells meet the three remaining cosets of the index-four subgroup rejects all five. The statements and the proof outline are recorded on the library's source card.

Submission note. Posted to erdosproblems.com as a proof claim by Rio Itabe (account ritabe) on 17 August 2026, giving "GPT-5.6 (ChatGPT Pro and OpenAI Codex)" as the AI used:

Every nontrivial exact partition of an arbitrary group into at most 17 left cosets of finite-index subgroups has a repeated subgroup index; hence any counterexample to the Herzog–Schönheim conjecture requires at least 18 cells. The unrestricted conjecture remains open. The proof combines harmonic obstructions with an exact arithmetic search and an index-four three-box fiber argument to eliminate the five remaining 17-cell profiles. Notes: The bounded result is formalized end-to-end in Lean 4. The closed final theorem has no external theorem assumptions or native-evaluation axioms, and the tagged source passes public CI. The manuscript is unreviewed and makes no priority claim. Comments and corrections are welcome.

Covers. The case of Problem 274 with at most seventeen cosets: no group has an exact covering by two to seventeen cosets whose sizes are pairwise different. The question for eighteen or more cosets stays open; the manuscript's 39 surviving profiles with eighteen cells are necessary-condition objects, not partitions.

Depends on. The four obstructions are Propositions 4.2, 4.3, 4.5 and 4.7 of Margolis and Schnabel, recorded with their Theorem A on their claim page; the manuscript's Lean development proves the needed forms of them itself.

Claimant and postings. Rio Itabe submitted the claim to the site's proof-claim tab on 2026-08-17, naming GPT-5.6 (ChatGPT Pro and OpenAI Codex) as the AI system used; the manuscript's disclosure says that language models accessed through ChatGPT Pro and OpenAI Codex, primarily GPT-5.6, were used in proof exploration, formalization, test generation, literature screening and editing, and that Itabe is responsible for the claim. The manuscript and its Lean 4 project are released together under the tag v0.4.2-review-candidate, linked above at its commit.

Formalization. The release's Lean 4 project proves the closed theorem erdos274AtMostSeventeen, with both finite searches split into decide +kernel certificates; the manuscript reports that #print axioms lists only propext, Classical.choice and Quot.sound and that the first-party theorem tree has no sorry. This corpus has neither built nor audited the project, and no statement-fidelity review of it exists here, so it gives no formalized evidence.

Standing. Claimed. The site labels the problem OPEN, and the proof-claim tab states that a listed claim has not been examined by the site. No refereed version or independent review is recorded.