Partitioner wins the $\omega$ -partitioning game on every countable graph

Open

TenChallenges.challenge_10_r_omega

by utkuokur · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

infinite-graphsten-challengesunfriendly-partition

The rung $r=\omega$ of Challenge 10. For every countable vertex type $V$ and every graph $G$ on $V$ , Partitioner has a winning strategy in the $\omega$ -partitioning game on $G$ from the empty partial partition:

\forall G \text{ countable}:\quad \mathrm{PartitionerWins}(G,\emptyset,\omega).

With clock $\omega$ , Challenger's first move names a vertex and a natural number $n$ , after which at most $n$ further challenges follow.

Preamble

import Definitions.Def_TenChallenges_Challenge_10
universe u v

Formal statement

namespace TenChallenges
theorem challenge_10_r_omega : statement_10.{u, v} Ordinal.omega0 := by sorry
end TenChallenges

Source

Scaled form from V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics, AI4Math @ CICM 2026, challenge 10; the game is defined on the Ten Challenges website, challenge 10

Human review

Endorsed by Shuze Chen · Nov 4, 2026
Confirmed by the moderator at approval.
Endorsed by utkuokur · Nov 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Partitioner wins the ω\omegaω-partitioning game on every countable graph

Partitioner wins the $\omega$ -partitioning game on every countable graph