Erdős problem 872

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

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

872.lean

Retained formal statement6 of 6

Membership in legalMoves: a legal move is a pool element whose insertion preserves primitiveness.

FormalConjectures/ErdosProblems/872.leanErdos872.mem_legalMoves2 linesExact file

1∀ {n : ℕ} {p : Erdos872.GamePos n} {x : ℕ},2  x ∈ Erdos872.legalMoves p ↔ x ∈ p.pool ∧ Erdos872.IsPrimitive n (insert x p.claimed)

APIStatement only, no proof