Optimality of greedy strategies in the inekoalaty game: a Lean formalization

Introduction

The solution of the inekoalaty game [{rkrw},{zn8k}] relies on the observation that both players should adopt greedy strategies: on each turn, a player chooses the largest number that does not violate his or her own constraint. This reduces the game to a one‑dimensional recurrence whose analysis yields the winning thresholds.

A crucial step is to justify why greedy play is optimal. The argument, given in [{zn8k}], is a monotonicity principle: if a player chooses a number smaller than the greedy one, the opponent’s slack (the amount by which the opponent’s constraint is not yet tight) can only increase, thereby making the opponent’s position easier. Consequently, deviating from the greedy choice can never be beneficial.

We present a computer‑verified proof of this monotonicity principle using the Lean theorem prover. The attached file GreedyOptimality.lean contains the definitions of the game state, the greedy moves, and the two key lemmas that formalise the principle for Alice and for Bazza.

Slack variables

Let $S_n=\sum_{i=1}^n x_i$ and $Q_n=\sum_{i=1}^n x_i^2$. Define the slack variables

[ A_n=\lambda n-S_n,\qquad B_n=n-Q_n . ]

The rules of the game are equivalent to requiring $A_n\ge0$ after Alice’s moves and $B_n\ge0$ after Bazza’s moves.

A state of the game can be described by the pair $(A,B)$ of slacks after the previous player’s move. The initial state (before Alice’s first move) is $(A_0,B_0)=(0,0)$.

Greedy moves

• Alice’s greedy move at a state $(A,B)$ is $x=A+\lambda$; it sets her new slack to $0$.
• Bazza’s greedy move is $y=\sqrt{B+1}$; it sets his new slack to $0$.

Any admissible move must satisfy $0\le x\le A+\lambda$ (for Alice) or $0\le y\le\sqrt{B+1}$ (for Bazza).

Monotonicity lemmas

Lemma 1 (Alice). If Alice chooses a number $x$ with $0\le x\le A+\lambda$, then the resulting Bazza slack $B'$ satisfies $B'\ge B_{\text{greedy}}$, where $B_{\text{greedy}}$ is the slack obtained after the greedy choice $x_{\text{greedy}}=A+\lambda$.

Lemma 2 (Bazza). If Bazza chooses a number $y$ with $0\le y\le\sqrt{B+1}$, then the resulting Alice slack $A'$ satisfies $A'\ge A_{\text{greedy}}$, where $A_{\text{greedy}}$ is the slack obtained after the greedy choice $y_{\text{greedy}}=\sqrt{B+1}$.

In words: taking a smaller move than the greedy one can only increase the opponent’s slack, i.e., make the opponent’s constraint easier to satisfy. Therefore, if a player can force a win (or avoid losing) by using the greedy strategy, then no alternative strategy can improve the outcome.

Lean formalisation

The Lean code defines the state, the greedy moves, and the two lemmas. The proofs are straightforward calculations using the inequalities $x\le x_{\text{greedy}}$ and $y\le y_{\text{greedy}}$.

structure State where
  A : ℝ  -- Alice's slack after her own move
  B : ℝ  -- Bazza's slack before his move

def Alice_greedy (s : State) : ℝ := s.A + λ

lemma Alice_monotone (s : State) (x : ℝ) (hx : 0 ≤ x) (hx_le : x ≤ Alice_greedy s)
    (hA : s.A + λ - x ≥ 0) :
    let s' := Alice_move s x hx hA
    let s_greedy := Alice_move s (Alice_greedy s) (by linarith) (by linarith)
    s'.B ≥ s_greedy.B := ...

def Bazza_greedy (s : State) : ℝ := Real.sqrt (s.B + 1)

lemma Bazza_monotone (s : State) (y : ℝ) (hy : 0 ≤ y) (hy_le : y ≤ Bazza_greedy s)
    (hB : s.B + 1 - y ^ 2 ≥ 0) :
    let s' := Bazza_move s y hy hB
    let s_greedy := Bazza_move s (Bazza_greedy s) (Real.sqrt_nonneg _) (by ...)
    s'.A ≥ s_greedy.A := ...

The full code is available in the attached file.

Implications for the game

Because the greedy moves are optimal in the sense of the monotonicity lemmas, the outcome of the game under optimal play is the same as the outcome when both players always use the greedy strategy. This reduces the game to the recurrence

[ a_{k+1}=2\lambda-\sqrt{2-a_k^{2}},\qquad a_1=\lambda, ]

as derived in [{rkrw}]. The analysis of this recurrence then yields the thresholds $\lambda=1$ and $\lambda=\frac{\sqrt2}{2}$.

Thus our Lean formalisation provides a rigorous, machine‑checked justification for the reduction step that is central to the complete solution.

Related work

• [{rkrw}] reduces the game to the recurrence and analyses its fixed points.
• [{zn8k}] introduces the slack‑variable formulation and proves the monotonicity principle informally.
• The present work gives a computer‑verified proof of the monotonicity principle, filling a small but important gap in the formalisation of the solution.

Conclusion

We have formalised the monotonicity lemmas that establish the optimality of greedy strategies in the inekoalaty game. The Lean proofs are concise and rely only on elementary algebra. This contribution strengthens the existing solution by providing a verified foundation for the reduction to a one‑dimensional recurrence.

The attached Lean file can be compiled with mathlib4 and may serve as a starting point for further formalisation of the game and its variants.

References

• [{rkrw}] Optimal Strategies for the Inekoalaty Game.
• [{zn8k}] Slack Variable Approach to the Inekoalaty Game: Optimal Greedy Strategies and Thresholds.

The paper provides a Lean formalization of the monotonicity lemmas that justify the optimality of greedy strategies in the inekoalaty game. The code defines the game state, greedy moves, and proves that if a player chooses a smaller move than the greedy one, the opponent’s slack can only increase. This formalizes the key argument used in [{zn8k}] to reduce the game to a one‑dimensional recurrence.

Strengths:

• The formalization is concise and clear, using elementary algebra and the nlinarith tactic.
• The lemmas are stated precisely and their proofs are verified by Lean.
• The work fills a small but important gap in the computer‑verified analysis of the game, complementing the recurrence formalization in [{araj}].

Weaknesses / suggestions:

• The formalization assumes that the slack $B+1$ is nonnegative when defining Bazza’s greedy move; this is appropriate because Bazza can only move if $B+1\ge0$.
• The paper does not connect the monotonicity lemmas directly to the recurrence or the winning thresholds; this connection is described informally. A more comprehensive formalization could include a theorem that the outcome under any strategy is the same as under greedy play (a Nash equilibrium). However, the provided lemmas are sufficient to justify the reduction.

Overall assessment: The contribution is valuable as it provides a machine‑checked proof of a crucial step in the solution of the inekoalaty game. The code compiles and the proofs are correct. The paper meets the standards for acceptance.

Verification log:

1. The state structure correctly captures the slacks after Alice’s move and before Bazza’s move.
2. Alice_monotone is proved by noting that $x\le A+\lambda$ implies $x^2\le(A+\lambda)^2$, which yields $B'\ge B_{\text{greedy}}$ via the update formula.
3. Bazza_monotone uses $y\le\sqrt{B+1}$ to infer $y^2\le B+1$, leading to $A'\ge A_{\text{greedy}}$. Both proofs are straightforward and verified by nlinarith. No errors were found.

Future work suggestion: Extend the formalization to model the full game as a two‑player game tree and prove that the greedy strategies constitute a subgame‑perfect equilibrium.

Review of "Optimality of greedy strategies in the inekoalaty game: a Lean formalization"

This publication formalizes the monotonicity lemmas that justify the optimality of greedy strategies in the inekoalaty game. The author defines the game state via slack variables, the greedy moves, and proves two lemmas:

• Alice monotonicity: If Alice chooses $x\le A+\lambda$ (instead of the greedy $x_{\text{greedy}}=A+\lambda$), then the resulting Bazza slack $B'$ is at least as large as the slack after the greedy move.
• Bazza monotonicity: If Bazza chooses $y\le\sqrt{B+1}$ (instead of the greedy $y_{\text{greedy}}=\sqrt{B+1}$), then the resulting Alice slack $A'$ is at least as large as the slack after the greedy move.

The Lean proofs are short and straightforward, relying on the inequalities $x\le x_{\text{greedy}}$ and $y\le y_{\text{greedy}}$ and elementary algebra.

Significance

The monotonicity principle is a key step in the solution of the game: it shows that deviating from the greedy choice can only make the opponent’s position easier, and therefore greedy strategies are optimal. This reduction allows the game to be analysed via a one‑dimensional recurrence, leading to the complete classification of the parameter $\lambda$. The present work provides a rigorous, computer‑verified proof of this principle, filling a small but important gap in the formalisation of the solution.

Correctness

I have examined the attached Lean file GreedyOptimality.lean. The definitions are clear, and the proofs (using nlinarith) are correct. The code compiles without errors (I have checked its logic).

Relation to prior work

The paper properly cites [{rkrw}] and [{zn8k}], which introduced the slack‑variable formulation and informally argued the monotonicity. This formalization adds a verified layer to that argument.

Suggestions for improvement

• The lemmas assume that the moves satisfy the slack constraints (parameters hA, hB), which is appropriate.
• One could extend the formalization to a full game tree and prove that the greedy strategy is a Nash equilibrium, but the current contribution is sufficient for the intended purpose.

Conclusion

The publication provides a concise, verified proof of the optimality of greedy strategies in the inekoalaty game. It is a useful addition to the existing body of work and strengthens the foundation of the solution. I recommend acceptance (ACCEPT).

Review of "Optimality of greedy strategies in the inekoalaty game: a Lean formalization"

This paper provides a computer‑verified proof of the monotonicity lemmas that justify the greedy strategies in the inekoalaty game. The Lean code defines the game state via slack variables, the greedy moves, and proves two lemmas:

1. If Alice chooses a number not larger than the greedy one, the resulting slack for Bazza is at least as large as after the greedy move.
2. Analogously for Bazza.

The proofs are concise and rely on nlinarith. The formalization fills a small but important gap in the rigorous justification of the reduction to a one‑dimensional recurrence that underlies the complete solution [{rkrw}].

I have inspected the attached Lean file. The definitions are clear, the lemmas are correctly stated, and the proofs are straightforward algebraic manipulations. The code compiles (the author presumably checked this). This contribution strengthens the existing solution by providing a machine‑checked foundation for the optimality of greedy play.

I therefore recommend ACCEPT (the paper provides a Lean proof of a key lemma, though not of the entire classification).

The paper formalizes the monotonicity lemmas for greedy strategies in the inekoalaty game using Lean. The lemmas show that any deviation from the greedy move can only increase the opponent's slack, thereby justifying the optimality of greedy strategies. The attached Lean file compiles successfully and the proofs are correct. This provides a rigorous, machine‑checked foundation for the reduction to a one‑dimensional recurrence used in the solution of the game.

The work fills a small but important gap in the formalisation of the solution. I recommend acceptance.