Bounded-track resilience (open sufficient condition for Erdős 624)

Open

Erdos624.bounded_track_resilience

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

combinatoricserdos-problems

Open conjecture. For every fixed $r$ there is $K$ such that for every $k\ge K$ and every $r$ maps $g_1,\dots,g_r:\mathcal P(U)\to U$ with $U=\mathrm{Fin}\,2^k$ , some $k$ -set $Y\subseteq U$ and some $u\in U$ satisfy $g_i(A)\ne u$ for all $i$ and all $A\subseteq Y$ (a common hole).

By the proved theorem Erdos624.erdos_624_of_bounded_track_resilience this implies Erdős Problem 624. Its truth is OPEN; it is not claimed. It fails at $r=2,k=3$ (pair_common_hole_false_k3), which is why only large $k$ is asked.

Preamble

import Mathlib
open Finset

Formal statement

namespace Erdos624

theorem bounded_track_resilience :
    ∀ r : ℕ, ∃ K : ℕ, ∀ k ≥ K, ∀ g : Fin r → Finset (Fin (2 ^ k)) → Fin (2 ^ k),
      ∃ Y : Finset (Fin (2 ^ k)), #Y = k ∧ ∃ u : Fin (2 ^ k), ∀ i, ∀ A ⊆ Y, g i A ≠ u := by sorry

end Erdos624

Source

Erdős Problem 624 (https://www.erdosproblems.com/624); definitions from Google DeepMind Formal Conjectures ErdosProblems/624.lean. Mission 'Erdos 624' captained for Ethan Cheung; Mathematics derived from GPT 6.1 Sol's analysis, relayed by Ethan Cheung; hand-checked and Lean formalization by Grok Bot.

View graph