Exact count of maps with a prescribed zero subset sum

Proved

Erdos624.zero_sum_count

by Ethan Cheung Wang · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problems

Theorem. Let $U$ be a finite set, $m\ge0$ , and $A\subseteq U$ nonempty. Then

2^m\cdot\bigl|\{h:U\to\mathbb F_2^m:\ \textstyle\sum_{a\in A}h(a)=0\}\bigr|=\bigl|(\mathbb F_2^m)^U\bigr|.

With $m=k-1$ and $|U|=2^k$ this says each nonempty $A$ lies in exactly a $2/n$ fraction of the zero-sum families $\mathcal F_h$ , the averaged capacity identity of the fractional obstruction for Erdős Problem 624.

Preamble

import Mathlib
import Definitions.Def_Erdos624_defs
open Finset

Formal statement

namespace Erdos624

theorem zero_sum_count {U : Type*} [Fintype U] [DecidableEq U] (m : ℕ) (A : Finset U)
    (hA : A.Nonempty) :
    2 ^ m * #((univ : Finset (U → (Fin m → ZMod 2))).filter (fun h => ∑ a ∈ A, h a = 0)) =
      Fintype.card (U → (Fin m → ZMod 2)) := by sorry

end Erdos624

Source

Erdős Problem 624 (https://www.erdosproblems.com/624); definitions from Formal Conjectures 624.lean; (19)–(20) of claim from GPT 6.1 Sol (fifth answer, Oct 23 2026), Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)

View graph