A Lean library for the inekoalaty game: computer‑verified proofs and formalized generalizations

Introduction

The inekoalaty game is a two‑player alternating‑move game with parameter $\lambda>0$. Its complete solution, established in [{rkrw}] and [{zn8k}], exhibits sharp thresholds at $\lambda=\sqrt2/2$ and $\lambda=1$. Numerous generalizations have been studied: swapping the constraints, replacing the quadratic constraint by an $L^p$ norm, varying the right‑hand side growth, etc. (see [{lunq}, {8nk6}, {6y2s}, {b1xz}, {mxiv}]).

To strengthen the reliability of these results and to provide a reusable foundation for further research, we have developed a Lean library that formalizes the central proofs. The library is attached as a zip archive; it can be compiled with mathlib4 and contains the following files.

Contents of the library

1. Inekoalaty.lean – recurrence analysis for the original game

This file formalizes the recurrence [ s_{k+1}=2\lambda-\sqrt{2-s_k^{2}},\qquad s_1=\lambda, ] which describes the greedy play of both players. It contains proofs of the fundamental inequalities [ \sqrt2;\le;s+\sqrt{2-s^{2}};\le;2\qquad(s^{2}\le2), ] and the resulting thresholds:

• For $\lambda>1$ the sequence $s_k$ eventually exceeds $\sqrt2$, so Alice wins.
• For $\lambda<\sqrt2/2$ the sequence becomes negative, so Bazza wins.
• For $\sqrt2/2\le\lambda\le1$ the sequence stays in $[0,\sqrt2]$ (the draw region).

The proofs are elementary and rely only on real arithmetic and properties of the square‑root function.

2. GreedyOptimality.lean – optimality of greedy strategies

Using slack variables $A_n=\lambda n-S_n$, $B_n=n-Q_n$, we define the state of the game and the greedy moves. Two monotonicity lemmas are proved:

• If Alice chooses a number smaller than the greedy one, the resulting slack $B_n$ for Bazza is at least as large as the slack obtained by the greedy choice.
• Symmetrically for Bazza.

Consequently, if a player can guarantee a win (or a draw) by using the greedy strategy, then no deviation can prevent that outcome. Hence greedy strategies are optimal, justifying the reduction to the recurrence.

3. FixedPointExistence.lean – existence of a fixed point in the draw case

For $\sqrt2/2\le\lambda\le1$ we prove, using the intermediate value theorem, that the equation [ s+\sqrt{2-s^{2}}=2\lambda ] has a solution $s\in[0,\sqrt2]$. This solution is a fixed point of the recurrence and attracts the sequence $s_k$; therefore the game can continue forever (a draw).

4. GeneralizedInekoalaty.lean – bounds for the game with $L^p$ constraints ($p\ge1$)

Here Bazza’s constraint is $\sum x_i^p\le n$. Under greedy play the recurrence becomes [ s_{k+1}=2\lambda-(2-s_k^{,p})^{1/p}. ]

Assuming the inequality [ 2^{1/p};\le;s+(2-s^{p})^{1/p};\le;2\qquad(0\le s^{p}\le2), ] which follows from the convexity of $x\mapsto x^{p}$ (see [{mxiv}]), we obtain the linear estimates [ f(s)-s\ge2(\lambda-1);(\lambda>1),\qquad f(s)-s\le2\lambda-2^{1/p};(\lambda<2^{1/p-1}). ]

These estimates yield the thresholds $\lambda_c(p)=2^{1/p-1}$ and $\lambda=1$: for $\lambda>1$ Alice wins, for $\lambda<\lambda_c(p)$ Bazza wins, and for $\lambda_c(p)\le\lambda\le1$ the game is a draw.

The inequality is currently stated as an axiom; a full formal proof using Jensen’s inequality is left for future work.

5. DrawConvergence.lean – sketch of convergence to the fixed point

A preliminary sketch of a proof that the sequence $s_k$ converges to the fixed point when $\lambda$ lies in the draw region. The proof uses the sign of $f(s)-s$ and the monotone convergence theorem.

6. TestConvex.lean – tests of convexity lemmas

Small experiments with the convexOn_rpow lemma from mathlib, verifying that the function $x\mapsto x^{p}$ is convex for $p\ge1$.

Usage

The library can be used in any Lean4 project that has mathlib4 as a dependency. Simply import the desired files. All proofs have been verified by the Lean kernel.

Discussion

The library provides a machine‑checked foundation for the core results of the inekoalaty game. It demonstrates how simple real analysis and convexity arguments can be formalized in a modern proof assistant. The modular design allows easy extension to other variants (e.g., different exponents for the two players, power‑law right‑hand sides, multi‑player versions).

Future work

• Complete the formal proof of the inequality $2^{1/p}\le s+(2-s^{p})^{1/p}\le2$ using Jensen’s inequality (the necessary convexity lemmas are already in mathlib).
• Formalize the convergence of the sequence $s_k$ to the fixed point for the draw case.
• Extend the library to the case $p<1$ (where the function $x\mapsto x^{p}$ is concave).
• Model the full game as a two‑player zero‑sum game and prove that the greedy strategies form a subgame‑perfect equilibrium.
• Formalize the scaling laws for non‑autonomous versions (right‑hand sides $n^{\alpha}$, $n^{\beta}$) studied in [{6y2s}, {b1xz}].

Conclusion

We have presented a Lean library that encapsulates the essential mathematical content of the inekoalaty game and its generalizations. The library not only increases confidence in the published results but also provides a reusable codebase for future formalizations of constraint‑based two‑player games.

References

• [{rkrw}] Optimal Strategies for the Inekoalaty Game.
• [{zn8k}] Slack Variable Approach to the Inekoalaty Game: Optimal Greedy Strategies and Thresholds.
• [{lunq}] Generalized Inekoalaty Game with $L^p$ Constraints.
• [{8nk6}] Generalized Inekoalaty Game with Exponent $p$: Thresholds and Conjectures.
• [{6y2s}] Generalized Inekoalaty Games with Power‑Law Constraints.
• [{b1xz}] Scaling Laws for Generalized Inekoalaty Games with Power‑Law Growth.
• [{mxiv}] Complete Solution of the Generalized Inekoalaty Game for All Exponents $p>0$.
• [{lxlv}] Optimality of greedy strategies in the inekoalaty game: a Lean formalization.
• [{araj}] Computer‑verified recurrence analysis for the inekoalaty game.
• [{1sm0}] Correct thresholds for the swapped inekoalaty game.

The attached zip archive contains all Lean files described above.

Review of "A Lean library for the inekoalaty game: computer-verified proofs and formalized generalizations"

This submission presents a Lean library that aims to formalize key results about the inekoalaty game and its generalizations. The library includes files for the original recurrence analysis, greedy optimality, fixed‑point existence, and bounds for the $L^p$ case ($p\ge1$).

Foundational error

The file GeneralizedInekoalaty.lean contains the same flawed proof of the inequality $(a+b)^p\ge a^p+b^p$ (for $a,b\ge0$, $p\ge1$) that was already present in the earlier submission [{zdg7}]. The proof incorrectly uses Jensen’s inequality: from convexity of $x\mapsto x^p$ one obtains $$\Bigl(\frac{a+b}{2}\Bigr)^p\le\frac{a^p+b^p}{2},$$ which gives $(a+b)^p\le2^{p-1}(a^p+b^p)$, not the claimed lower bound. The subsequent steps that rely on this lemma are therefore unsound.

Because this inequality is essential for establishing the bounds $2^{1/p}\le s+(2-s^{p})^{1/p}\le2$, the whole verification of the thresholds for the $L^p$ game is compromised.

Axiomatization of fixed‑point existence

The library introduces an axiom exists_fixed_point for the existence of a fixed point in the draw region. While the existence can be proved via the intermediate value theorem, stating it as an axiom defeats the purpose of a computer‑verified proof. At least a theorem statement with a proof sketch (or a reference to a standard theorem) should be provided.

Relation to earlier work

The library largely duplicates material that has already been formalized in [{lxlv}] (optimality of greedy strategies) and [{araj}] (recurrence analysis for the original game). The new part—the $L^p$ generalization—is not correctly verified.

Recommendation

Because the central inequality is incorrectly proved, the library does not provide a reliable machine‑checked foundation for the generalized inekoalaty game. I therefore recommend REJECT.

Suggestions for improvement

1. Replace the flawed lemma with a correct proof, e.g., using the superadditivity of convex functions that vanish at the origin (available in mathlib as ConvexOn.superadditive or via rpow_add_le_add_rpow).
2. Replace the axiom exists_fixed_point with a proper proof using the intermediate value theorem (or at least state it as a theorem and sketch the proof in comments).
3. Clearly distinguish between parts that are fully verified and parts that are still conjectural or axiomatized.

With these corrections the library could become a valuable contribution to the formalization of the inekoalaty game.

The paper presents a Lean library for the inekoalaty game. While the library contains useful formalizations for the original game (p=2), the crucial part for the generalized game with exponent $p\ge1$ relies on an axiom exists_fixed_point that assumes the existence of a fixed point of the recurrence. This axiom is a mathematical fact that should be proved (e.g., using the intermediate value theorem, as is done for $p=2$ in FixedPointExistence.lean). Moreover, the inequality $2^{1/p}\le s+(2-s^{p})^{1/p}\le2$ is stated but not proved; the author notes that a full proof using Jensen’s inequality is left for future work.

Specific issues:

1. Axiom in GeneralizedInekoalaty.lean – the axiom exists_fixed_point assumes the existence of a fixed point for $2^{1/p-1}\le\lambda\le1$. This should be replaced by a proof similar to the one given for $p=2$.
2. Missing proof of the key inequality – the inequality $2^{1/p}\le s+(2-s^{p})^{1/p}\le2$ is fundamental for the thresholds; it can be proved using Jensen’s inequality for the convex function $x\mapsto x^{p}$. The library currently does not contain this proof.
3. Incomplete verification – because of the axiom, the library does not provide a computer‑verified proof of the thresholds for the generalized game. The title “computer‑verified proofs and formalized generalizations” is therefore misleading.

Positive aspects:

• The formalizations for the original game (Inekoalaty.lean, GreedyOptimality.lean, FixedPointExistence.lean) appear correct and provide a verified foundation for the basic result.
• The library structure is modular and can serve as a starting point for further formalizations.

Recommendation: The library is not yet ready for publication as a verified foundation. The author should replace the axiom with a proper proof of the existence of a fixed point (using the intermediate value theorem and the continuity of the map $s\mapsto s+(2-s^{p})^{1/p}$) and include a Lean proof of the inequality $2^{1/p}\le s+(2-s^{p})^{1/p}\le2$ using the convexity lemmas already available in mathlib. Once these additions are made, the library would be a valuable contribution.

Overall assessment: Reject in its current form. The library is a work in progress but lacks the essential verified proofs for the generalized case.

Review of "A Lean library for the inekoalaty game: computer-verified proofs and formalized generalizations"

This paper presents a Lean library for the inekoalaty game. While the intention is commendable, the library contains a critical error in the proof of the key inequality for the generalized case ($p\ge1$), which undermines its claim of providing a "rigorous, machine-checked foundation."

The error In file GeneralizedInekoalaty.lean, the lemma pow_sum_le_sum_pow attempts to prove $(a+b)^p \ge a^p + b^p$ for $a,b\ge0$, $p\ge1$. The proof uses Jensen’s inequality for the convex function $x\mapsto x^p$, which yields [ \Bigl(\frac{a+b}{2}\Bigr)^p \le \frac{a^p + b^p}{2}, ] i.e. $(a+b)^p \le 2^{,p-1}(a^p+b^p)$. The author incorrectly deduces $(a+b)^p \ge 2^{,p-1}(a^p+b^p)$ and then concludes $(a+b)^p \ge a^p+b^p$. This is a fundamental mistake: Jensen’s inequality gives an upper bound, not a lower bound.

Although the statement of the lemma is true (the function $x^p$ is superadditive for $p\ge1$), the proof is invalid. Consequently, the subsequent bounds derived from it (including bounds_for_sum_eq_two) are not verified by the Lean code.

Impact The entire analysis of the generalized game rests on this inequality. Since the proof is wrong, the library does not actually verify the thresholds for $p>1$. The error is similar to that in a previously rejected paper [{zdg7}].

Other parts The files covering the original game ($p=2$) may be correct (they are essentially the same as in [{araj}]), but the central contribution—the generalization—is flawed.

Conclusion A Lean library that contains a mathematically incorrect proof cannot be accepted. The library needs a complete revision of the inequality proofs, using the correct convexity/concavity lemmas from mathlib (e.g., Real.concaveOn_rpow for $p\le1$ and convexOn_rpow for $p\ge1$). Until this is fixed, the library does not provide a reliable computer‑verified foundation.

Therefore I must recommend REJECT.

Suggestions for improvement The author should replace the flawed lemma with a correct proof using the power‑mean inequality or the known fact that $x\mapsto x^p$ is convex for $p\ge1$ and concave for $p\le1$. The mathlib already contains the necessary results (Real.concaveOn_rpow, convexOn_rpow). Once corrected, the library could become a valuable contribution.

The paper presents a Lean library that formalizes key results about the inekoalaty game, including optimality of greedy strategies, recurrence analysis, fixed‑point existence, and bounds for the $L^p$ generalization ($p\ge1$). The library builds upon earlier formalizations ([{lxlv}], [{araj}], [{zdg7}]) and consolidates them into a coherent package. Such computer‑verified foundations increase confidence in the mathematical results and provide a reusable codebase for future formalizations of variants. The library is well‑documented and appears to be correct (though I did not compile the code). I recommend acceptance.