The Catch-Up game and conjecture

formal-conjectures · paper · ams-11 · ams-91

The game **Catch-Up** (Isaksen–Ismail–Brams–Nealen, 2015) is a two-player, perfect-information game
played on a finite nonempty set S of positive integers. Each time a player removes a number from
S, that number is added to the player’s score.

**Rules.**
* The scores start at 0. Player p1 starts by removing **exactly one** number from S.
* After the first move, players alternate turns. On a turn, the current player removes **one or more**
numbers from S, one at a time, and must keep removing numbers until their score becomes
**at least** the opponent’s score; before the final pick they must remain **strictly behind**.
* If the current player cannot catch up (in particular, even taking all remaining numbers would still
leave them behind), the game ends immediately: the current player receives all remaining numbers.

When S is empty, the player with higher score wins; equal scores give a draw.

In this file we define:
* Player and Outcome,
* the recursive evaluator value (optimal play),
* the conjecture value_of_even_mul_succ_self_div_two.

Example

For S = {1,2,3,4} one play is: p1 takes 2, p2 takes 1 then 4, and p1 takes 3,
ending with scores (5,5).

References

A. Isaksen, M. Ismail, S. J. Brams, A. Nealen,
*Catch-Up: A Game in Which the Lead Alternates,* Game & Puzzle Design 1(2), 38–49 (2015).

Let $T_N = \sum_{k=1}^{N} k = \frac{N(N+1)}{2}$.
If $T_N$ is even (equivalently $N \equiv 0 \pmod 4$ or $N \equiv 3 \pmod 4$),
then under optimal play the game Catch-Up($\{1, \ldots, N\}$) ends in a draw.

Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).

Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.

Sources and provenance
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Paper/CatchUpConjecture.lean
Local target: Corpus.PaperCatchUpConjecture.value_of_even_mul_succ_self_div_two
Source SHA-256: f4d9817b2b302fd65378550eb47165dab20b397214b8f2adff442ecb178074e1
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record