PAIR: two maps eventually have a common hole on some $k$ -set (open)

Open

Erdos624.pair_eventual_common_hole

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

combinatoricserdos-problems

Open conjecture (PAIR). There is $K$ such that for every $k\ge K$ and every two maps $g_0,g_1:\mathcal P(U)\to U$ with $U=\mathrm{Fin}\,2^k$ , some $k$ -set $Y$ and colour $u$ satisfy $g_0(A)\ne u$ and $g_1(A)\ne u$ for all $A\subseteq Y$ , i.e. $D(Y)=n-|\bigcup_{A\subseteq Y}\{g_0(A),g_1(A)\}|>0$ .

This is the $r=2$ case of bounded-track resilience. It is OPEN, false at $k=3$ (pair_common_hole_false_k3), and by itself does not imply Erdős 624.

Preamble

import Mathlib
open Finset

Formal statement

namespace Erdos624

theorem pair_eventual_common_hole :
    ∃ K : ℕ, ∀ k ≥ K, ∀ g0 g1 : Finset (Fin (2 ^ k)) → Fin (2 ^ k),
      ∃ Y : Finset (Fin (2 ^ k)), #Y = k ∧ ∃ u : Fin (2 ^ k), ∀ A ⊆ Y, g0 A ≠ u ∧ g1 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

PAIR: two maps eventually have a common hole on some kkk-set (open)

PAIR: two maps eventually have a common hole on some $k$ -set (open)