Erdős problem 872 · problems.science

Each move claims exactly one pool element, so the minimax value never exceeds the number of already claimed elements plus the number of still unclaimed elements.

Sources

Browse retained paths and inspect the exact material available for this Problem.

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

872.lean

Retained formal statement5 of 6

Each move claims exactly one pool element, so the minimax value never exceeds the number of already claimed elements plus the number of still unclaimed elements.

FormalConjectures/ErdosProblems/872.leanErdos872.gameValueAux_le2 linesExact file

1∀ {n : ℕ} (fuel : ℕ) (turn : Bool) (p : Erdos872.GamePos n),2  Erdos872.gameValueAux fuel turn p ≤ p.claimed.card + p.pool.card

APIStatement only, no proof

Sources

Search problems.science