---

Claim. A Lean 4 development by Murali Menon, "The Herzog–Schönheim conjecture for solvable groups", proves that if a solvable group, finite or infinite, is partitioned into finitely many left cosets of subgroups, at least two of them, then two of the subgroups have the same index, and so the same cardinality. Its theorems Erdos274.herzog_schonheim.variants.solvable and Erdos274.erdos_274.variants.solvable state the index and cardinality forms with the hypothesis that $G$ is solvable added to the formal-conjectures statements, using Mathlib's derived-series notion of solvability. By the registry entry's abstract, the infinite case reduces to a finite solvable quotient by the common core of the subgroups, and the finite case treats a least counterexample through its largest prime divisor $p$, divisibility restrictions on local indices from fixed-point counts in a primitive solvable quotient, and a separate argument at $p=7$. No informal write-up is public. This is a different work from Menon's [[../library/group_theory/menon_2026_two_questions_g_harmonic_tuples/_index|note on $G$-harmonic tuples]] and its coset partition of $A_5$.

Submission note. The Palomar registry's description of entry PALOMAR-2026-10-02-000004:

A Lean 4 formalization of the Herzog–Schönheim conjecture (the index form, which implies the cardinality form asked in Erdős problem 274) for every solvable group, finite or infinite: if a solvable group is partitioned into finitely many, and at least two, left cosets of subgroups, then two of the subgroups have the same index (hence, in the cardinality form, the same cardinality). The conjecture for arbitrary groups is open and is not claimed. The infinite case reduces to a finite solvable quotient by the common core of the parts; the finite case is proved for a least counterexample by considering its largest prime divisor p, using the subgroup generated by the p-prime-part elements, divisibility restrictions on local indices obtained from fixed-point counts in a primitive solvable quotient, and an extra closure argument at p = 7. The statements use the same exact covering structure as the formal-conjectures file for Erdős problem 274.

Covers. The case of Problem 274 for solvable groups: no solvable group has an exact covering by two or more cosets of pairwise different sizes. The question for nonsolvable groups stays open. The only earlier claim of the solvable case, arXiv:1901.10131, was withdrawn in 2019.

Depends on. Nothing in this wiki; the development proves its reductions itself.

Claimant and postings. Menon registered the development with the Palomar registry as entry PALOMAR-2026-10-02-000004, registered 2026-10-02T07:53Z, from the source repository linked above at the pinned commit (Apache 2.0). The repository's README says that the code was developed with AI assistance from Claude and OpenAI Codex models, that no human expert has reviewed the proof, and that novelty has not been confirmed by a specialist.

Formalization. The registry replays a submitted proof in the Lean kernel and compares it with a challenge statement. Its entry records Lean v4.35.0-rc2, the Mathlib revision it pins, the permitted axioms propext, Quot.sound and Classical.choice, an 85-line challenge file importing only Mathlib, checks by two further kernels, and an automated review by a language model with a neutral outcome and no warnings; the registry's own description says that it certifies neither novelty nor the match between the formal and informal statements and is not peer review. This corpus has neither built nor audited the development, and no statement-fidelity review of its challenge file exists here, so it gives no formalized evidence.

Standing. Claimed. The site labels the problem OPEN, and the site's page and proof-claim tab do not mention the registration. No refereed version or independent review is recorded.