Formal target: Corpus.WikipediaBeckFialaConjecture.beck_fiala_conjecture

**The Beck–Fiala conjecture** There exists a universal constant $C > 0$ such that every set system $S_1, \dots, S_m \subseteq [n]$ of degree at most $t$ admits a colouring $\chi \colon [n] \to \{-1, +1\}$ with $\left|\sum_{j \in S_i} \chi(j)\right| \le C \sqrt{t}$ for every $i$.

Exact formal statement

Exists.{1} fun C =>
  And (LT.lt.{0} 0 C)
    (∀ (n m t : Nat) (S : Fin m → Finset.{0} (Fin n)),
      (∀ (j : Fin n),
          LE.le.{0} (Finset.card.{0} (Finset.filter.{0} (fun i => Membership.mem.{0, 0} (S i) j) Finset.univ.{0})) t) →
        Exists.{1} fun χ =>
          And (∀ (j : Fin n), Or (Eq.{1} (χ j) 1) (Eq.{1} (χ j) (-1)))
            (∀ (i : Fin m),
              LE.le.{0} (abs.{0} (Finset.sum.{0, 0} (S i) fun j => χ j)) (HMul.hMul.{0, 0, 0} C (Nat.cast.{0} t).sqrt)))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record