CatchUpConjecture.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

8 declarations, 1 contain sorry, 0 declared as axioms

The Catch-Up game and conjecture

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).

Imports (1)

FormalConjecturesUtil

inductive CatchUp.Player An arbitrary two elements type indexing the players in the Catch-Up game line 59 source
Source documentation
An arbitrary two elements type indexing the players in the Catch-Up game.

no axioms what this means
```
inductive Player
  | p1
  | p2
deriving DecidableEq, Repr

/-- Returns the other player. -/
```
def CatchUp.Player.other Returns the other player line 65 source
Source documentation
Returns the other player.

no axioms what this means
Statement uses: CatchUp.Player
Proof uses: CatchUp.Player.other.match_1, Unit, CatchUp.Player.p2, CatchUp.Player.p1
```
def Player.other : Player → Player
  | p1 => p2
  | p2 => p1

/-- The possible outcomes of a Catch-Up game. -/
```
Mentions: CatchUp.Player

inductive CatchUp.Outcome The possible outcomes of a Catch-Up game line 70 source

Source documentation

The possible outcomes of a Catch-Up game.

no axioms what this means

inductive Outcome
  | win
  | loss
  | draw
deriving DecidableEq, Repr

/-- Negates an outcome, swapping win and loss. Used when switching player perspectives. -/

def CatchUp.Outcome.neg Negates an outcome, swapping win and loss line 77 source
Source documentation
Negates an outcome, swapping win and loss. Used when switching player perspectives.

no axioms what this means
Statement uses: CatchUp.Outcome
Proof uses: CatchUp.Outcome.neg.match_1, Unit, CatchUp.Outcome.loss, CatchUp.Outcome.win, CatchUp.Outcome.draw
```
def Outcome.neg : Outcome → Outcome
  | win => loss
  | loss => win
  | draw => draw

/--
Computes the best outcome for the current player from a list of possible outcomes.
Win > Draw > Loss.
-/
```
Mentions: CatchUp.Outcome, CatchUp.Outcome.best
def CatchUp.Outcome.best Computes the best outcome for the current player from a list of possible outcomes line 86 source
Source documentation
Computes the best outcome for the current player from a list of possible outcomes. Win > Draw > Loss.

standard axioms: propext what this means
Statement uses: List, CatchUp.Outcome
Proof uses: List.foldl, CatchUp.Outcome.best.match_1, CatchUp.Outcome.win, CatchUp.Outcome.draw, CatchUp.Outcome.loss
```
def Outcome.best (os : List Outcome) : Outcome :=
…
```
Mentions: CatchUp.Outcome
def CatchUp.valueAux value remaining s_me s_opp isFirstMove evaluates the position where: * remaining is the set S' of numbers not yet taken line 116 source
Source documentation
value remaining s_me s_opp isFirstMove evaluates the position where:
- remaining is the set S' of numbers not yet taken.
- s_me is the current score of the player who is about to act (the “current player”).
- s_opp is the opponent’s current score.
- isFirstMove indicates whether we are in the special very first move of the whole game, where the rules force exactly one pick and then the turn passes.
The result is the game-theoretic value from the current player’s point of view: .win / .loss / .draw, assuming optimal play from both sides.
We model a single turn (which may consist of several picks $x_1,...,x_k$ ) by recursion: the current player chooses one number x; if they are still strictly behind after taking it, they must continue the same turn (so the recursive call keeps the same “current player”); once they catch up (score ≥ opponent), the turn ends and we swap players.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Bool, CatchUp.Outcome
Proof uses: PSigma.mk, PSigma
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def valueAux (remaining : Finset ℕ) (s_me s_opp : ℕ) (isFirstMove : Bool) : Outcome :=
…
```
Mentions: CatchUp.Outcome
def CatchUp.value Public API: The game-theoretic value of Catch-Up on the set S, assuming optimal play line 173 source
Source documentation
Public API: The game-theoretic value of Catch-Up on the set S, assuming optimal play. Returns .win if player 1 wins, .loss if player 2 wins, .draw if the game is tied.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, CatchUp.Outcome
Proof uses: CatchUp.valueAux, OfNat.ofNat, Bool.true
1 instances, coercions and auxiliary constants left out.
```
noncomputable def value (S : Finset ℕ) : Outcome :=
…
```
Mentions: CatchUp.Outcome
theorem CatchUp.value_of_even_mul_succ_self_div_two Let $T_N = \sum_{k=1}^{N} k = \frac{N(N+1)}{2}$ sorry line 182 source
Source documentation
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.

depends on sorry what this means
Statement uses: Nat, Even, HDiv.hDiv, HMul.hMul, HAdd.hAdd, OfNat.ofNat, Eq, CatchUp.Outcome, CatchUp.value, Finset.Icc, CatchUp.Outcome.draw
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem value_of_even_mul_succ_self_div_two
    (N : ℕ) (h_even : Even (N * (N + 1) / 2)) :
    value (.Icc 1 N) = .draw := by
…
```
Mentions: CatchUp.value