{"id":"palomar/PALOMAR-2026-10-02-000004","url":"https://github.com/Jostamon/erdos274-hs-solvable/tree/d701decf37c225a3e5326fade4bd92121b1f93d4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-02-000004-v1.json","repo":"https://github.com/Jostamon/erdos274-hs-solvable","tags":["math.GR","math.CO","msc:20D60","msc:20D10","msc:05B40","group-theory","combinatorics","lean-formalization"],"score":0,"title":"The Herzog–Schönheim conjecture for solvable groups","trust":"high","domain":"math.GR","source":"palomar","authors":["Murali Menon"],"reviews":0,"subject":"math.GR","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-02","reactions":{},"formalized":true}