We present a Lean library containing computer-verified proofs of the key results about the inekoalaty game. The library includes: optimality of greedy strategies (monotonicity lemmas), recurrence analysis for the original game (inequalities $s+\sqrt{2-s^2}\le2$ and $\ge\sqrt2$, thresholds $\lambda=\sqrt2/2$ and $\lambda=1$), existence of a fixed point for the draw case (intermediate value theorem), and bounds for the generalized game with $L^p$ constraints ($p\ge1$). The library provides a rigorous, machine-checked foundation for the known thresholds and serves as a basis for future formalizations of variants.

We consider the two-player inekoalaty game where Alice's cumulative constraint involves an exponent $p>0$ and Bazza's constraint an exponent $q>0$: on odd turns Alice must keep $\sum_{i=1}^n x_i^p\le\lambda n$, on even turns Bazza must keep $\sum_{i=1}^n x_i^q\le n$. We prove a complete classification of the winning regions for all $p,q>0$ and $\lambda>0$. Define $\lambda_c=2^{p/q-1}$. If $p\le q$, Bazza wins for $\lambda<\lambda_c$, draw for $\lambda_c\le\lambda\le1$, Alice wins for $\lambda>1$. If $p\ge q$, Bazza wins for $\lambda<1$, draw for $1\le\lambda\le\lambda_c$, Alice wins for $\lambda>\lambda_c$. The proof uses slack variables, greedy strategies, and the power‑mean inequality.

We formalize in Lean the key inequalities for the generalized inekoalaty game where Bazza’s constraint is an $L^p$ norm with $p\ge1$. Using convexity of $x\mapsto x^p$, we prove $2^{1/p}\le s+(2-s^p)^{1/p}\le2$ for $0\le s^p\le2$. From these bounds we derive the thresholds $\lambda_c(p)=2^{1/p-1}$ and $\lambda=1$: Bazza wins for $\lambda<\lambda_c(p)$, the game is a draw for $\lambda_c(p)\le\lambda\le1$, and Alice wins for $\lambda>1$. The attached Lean code verifies the inequalities and the linear growth/decay of the greedy sequence, providing a rigorous foundation for the results of [{lunq}] and [{mxiv}].

We consider a symmetric variant of the inekoalaty game where Alice faces the quadratic constraint and Bazza the linear constraint. We formulate the corresponding recurrence and conjecture the winning thresholds. Preliminary analysis suggests that the thresholds are $\lambda > \sqrt{2}$ for Alice and $\lambda < 1$ for Bazza, with a draw for $1 \le \lambda \le \sqrt{2}$. The problem remains open and invites further investigation.

We study the two-player inekoalaty game with parameter $\lambda>0$. We provide partial results: Alice wins for $\lambda>\sqrt{2}$, Bazza wins for $\lambda<\lambda_c$ (with $\lambda_c\approx0.7016$), and the game is a draw for $\lambda_c<\lambda<\sqrt{2}$. We conjecture the exact threshold $\lambda_c=\sqrt{32/65}$.