% Copyright (c) 2026 Arthur Freitas Ramos, David Barros Hulak, and Ruy J. G. B. de Queiroz.
% Manuscript source licensed CC BY 4.0: https://creativecommons.org/licenses/by/4.0/
\documentclass[11pt]{amsart}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[a4paper,margin=29mm]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{booktabs,array}
\usepackage{listings}
\usepackage{microtype}
\usepackage{xurl}
\usepackage[hidelinks]{hyperref}

\hypersetup{
  pdftitle={A Lean Formalization of Finite Zero Sum Minimax via Sion's Theorem},
  pdfauthor={Arthur Freitas Ramos; David Barros Hulak; Ruy J. G. B. de Queiroz},
  pdfsubject={Expository formalization note on finite two-player zero-sum games},
  pdfkeywords={minimax, Lean, Mathlib, Sion, formalization, zero-sum games}
}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\R}{\mathbb{R}}
\newcommand{\EA}{\Delta(A)}
\newcommand{\EB}{\Delta(B)}
\newcommand{\pay}{P_u}
\newcommand{\lowerval}{\underline v(u)}
\newcommand{\upper}{\overline v(u)}
\newcommand{\decl}[1]{\nolinkurl{#1}}
\newcommand{\source}[2]{\href{https://github.com/Arthur742Ramos/minimax-theorem-lean/blob/f1d1d00591548c174407cd59ddc623a461c082c1/#1}{#2}}
\lstdefinestyle{lean}{
  basicstyle=\ttfamily\small,columns=fullflexible,keepspaces=true,
  breaklines=true,breakatwhitespace=false,showstringspaces=false,
  aboveskip=9pt,belowskip=9pt,frame=none,
  literate={ℝ}{{\(\mathbb R\)}}1 {→}{{\(\to\)}}1
    {∀}{{\(\forall\)}}1 {∃}{{\(\exists\)}}1
    {≤}{{\(\le\)}}1 {⨆}{{\(\sup\)}}1 {⨅}{{\(\inf\)}}1
    {∑}{{\(\sum\)}}1 {⟨}{{\(\langle\)}}1 {⟩}{{\(\rangle\)}}1
}
\lstset{style=lean}

\title[Finite zero sum minimax in Lean]{A Lean Formalization of Finite Zero Sum Minimax via Sion's Theorem}
\author{Arthur Freitas Ramos}
\author{David Barros Hulak}
\author{Ruy J. G. B. de Queiroz}
\thanks{Author ORCID identifiers: Arthur Freitas Ramos,
\href{https://orcid.org/0009-0003-3568-0325}{0009-0003-3568-0325};
David Barros Hulak,
\href{https://orcid.org/0009-0002-8056-1774}{0009-0002-8056-1774};
Ruy J. G. B. de Queiroz,
\href{https://orcid.org/0000-0003-1482-0977}{0000-0003-1482-0977}.}
\thanks{Copyright 2026 the authors. Licensed under \href{https://creativecommons.org/licenses/by/4.0/}{Creative Commons Attribution 4.0 International (CC BY 4.0)}.}
\date{September 30, 2026}
\subjclass[2020]{91A05, 68V20}
\keywords{Finite zero-sum games, minimax theorem, Lean 4, Mathlib, Sion's theorem}

\begin{document}
\begin{abstract}
We describe a Lean 4 formalization of the minimax theorem for finite
nonempty two-player zero-sum games with arbitrary real payoffs. Mixed
strategies are probability vectors, and the two game values are defined
using real indexed suprema and infima. An explicit payoff bound supplies
the boundedness obligations required by these conditional extrema.
The reverse minimax inequality follows by applying Mathlib's proved
Sion saddle-point theorem to compact convex coordinate simplices, with
the minimizing player placed in its first argument. We explain the
representation bridge, the proof obligations, and the passage from a
saddle point to equality. The accompanying version-pinned artifact
separates a reusable library from a statement-only challenge and its
proved solution. This is an exposition of a finite-game specialization
of existing formal analysis, with no claim of a new mathematical proof
or formalization priority.
\end{abstract}
\maketitle
\raggedbottom

\section{Scope and mathematical context}

Von Neumann's finite minimax theorem concerns two players with opposing
interests who may randomize over their available actions
\cite{vonNeumann1928}. The maximizing player's best guaranteed payoff
equals the minimizing player's best guaranteed ceiling. The theorem
also provides optimal mixed strategies. Here we explain a Lean
formalization of that statement, including the details that connect a
finite payoff matrix to the analytic infrastructure used in its proof.

The mathematical result is classical. Our proof route specializes the
Sion saddle-point theorem already available in Mathlib
\cite{Sion1958,MathlibSion}, whose source credits Antoine Chambert-Loir
and Anatole Dedecker and describes its proof as following Komiya
\cite{Komiya1988}. We do not reconstruct von Neumann's original
argument. Mathlib's general theorem carries the principal analytic
existence result; the development under discussion supplies the
finite-game representation, boundedness lemmas, simplex facts,
application of that theorem, and a public minimax interface.

All implementation claims in this note refer to commit
\nolinkurl{f1d1d00591548c174407cd59ddc623a461c082c1}
of the artifact \cite{MinimaxArtifact}. Lean is pinned to
\texttt{v4.35.0-rc2}. The Mathlib dependency is pinned to the same
release tag and resolved to commit
\nolinkurl{065356127b1dc0016f66b7283ce0ce2c4055aa55}.
The statements quantify over arbitrary finite nonempty pure-strategy
types $A$ and $B$ and an arbitrary function $u:A\times B\to\R$.
No rationality, sign, or extra regularity assumption is imposed on
the payoffs. The first player maximizes $u$ and the second minimizes
it, so their payoffs may be interpreted as $u$ and $-u$.
The implementation stores just this one payoff function.

The exposition makes the formal theorem's meaning and dependencies
inspectable: where nonemptiness is used, why real extrema require
explicit bounds, and why the players change order at the Sion
interface. Source alignment and ordinary scholarly review remain
necessary for the surrounding prose and historical claims.

\section{Finite games and their real values}

\subsection{Probability vectors}
For a finite nonempty set $S$, put
\[
  \Delta(S)=\left\{z:S\to\R\;\middle|\;
     (\forall s,\ 0\le z_s)\ \text{and}\ \sum_{s\in S}z_s=1\right\}.
\]
The public structure \decl{Minimax.MixedStrategy} carries these data
directly. In the following excerpts, mathematical symbols are rendered
typographically from the Lean source.
\begin{lstlisting}
public structure MixedStrategy (A : Type*)
    [Fintype A] [Nonempty A] where
  val : A → ℝ
  nonneg : ∀ a, 0 ≤ val a
  sum_one : ∑ a, val a = 1
\end{lstlisting}
The \texttt{Fintype} instances provide finite enumerations, while
\texttt{Nonempty} excludes an empty action type. A uniform strategy
has every coordinate equal to $|S|^{-1}$; since $|S|\ne0$, its mass
is one. This construction gives the instance
\decl{MixedStrategy.instNonempty} without selecting a particular
pure action. The lemma \decl{MixedStrategy.val_le_one} proves that
each probability coordinate is at most one, by comparing it with
the sum of all nonnegative coordinates.

The library also defines pure strategies and convex mixing. For
$p,q\ge0$ with $p+q=1$, the mixture of $x,z\in\Delta(S)$ has
coordinates $p x_s+q z_s$. Both its nonnegativity and its mass-one
condition are proved in the structure constructor. Mixed strategies
themselves are not treated as a vector space: arbitrary addition or
scalar multiplication need not preserve probability mass.

\subsection{Payoff and bilinear extension}
The expected payoff at independent mixed strategies is
\begin{equation}\label{eq:payoff}
  \pay(x,y)=\sum_{a\in A}\sum_{b\in B}x_a y_b u(a,b),
  \qquad x\in\EA,\quad y\in\EB.
\end{equation}
This is \decl{Minimax.expPayoff}. Its unrestricted extension
\decl{Minimax.weightedPayoff} uses the same formula on
$(A\to\R)\times(B\to\R)$. Additivity and scalar compatibility are
proved in each variable by finite-sum identities. The extension is
bilinear; its restriction to each simplex is affine.
The identity \decl{expPayoff_eq_weightedPayoff} is definitional,
so passing from a probability vector to its underlying coordinates
does not require a mathematical approximation or an encoding change.

Pure strategies are Dirac vectors. The simplification lemmas
\decl{expPayoff_pure_left}, \decl{expPayoff_pure_right}, and
\decl{expPayoff_pure_pure} identify their expected payoffs with the
corresponding row average, column average, and matrix entry.
For a constant payoff $c$, \decl{expPayoff_const} gives expected
payoff $c$. These are useful checks on the probability convention.

\subsection{Bounds before extrema}
Define the explicit finite bound
\begin{equation}\label{eq:bound}
  C_u=\sum_{a\in A}\sum_{b\in B}|u(a,b)|.
\end{equation}
The declaration \decl{payoffBound} uses this expression. Every
matrix entry satisfies $|u(a,b)|\le C_u$, because it is one
nonnegative summand of the double sum. The weights $x_a y_b$ are
nonnegative and have total mass one. Monotonicity of finite sums
therefore gives
\begin{equation}\label{eq:payoffbound}
  -C_u\le\pay(x,y)\le C_u
  \qquad(x\in\EA,\ y\in\EB).
\end{equation}
In the code this conclusion is \decl{expPayoff_bounds}, obtained
through \decl{expPayoff_mono}, \decl{le_expPayoff}, and
\decl{expPayoff_le}. The bound is deliberately simple rather than
tight; the proof only needs a uniform finite interval.

The two values are
\begin{equation}\label{eq:values}
  \lowerval=\sup_{x\in\EA}\inf_{y\in\EB}\pay(x,y),
  \qquad
  \upper=\inf_{y\in\EB}\sup_{x\in\EA}\pay(x,y).
\end{equation}
Their Lean definitions use indexed real extrema:
\begin{lstlisting}
noncomputable def maxminValue (u : A → B → ℝ) : ℝ :=
  ⨆ x : MixedStrategy A, ⨅ y : MixedStrategy B,
    expPayoff u x y

noncomputable def minmaxValue (u : A → B → ℝ) : ℝ :=
  ⨅ y : MixedStrategy B, ⨆ x : MixedStrategy A,
    expPayoff u x y
\end{lstlisting}
Here the displayed definitions abbreviate their common finite and
nonempty type hypotheses. In Mathlib, $\R$ is conditionally complete,
not a complete lattice with real elements representing $\pm\infty$.
Indexed extrema are total definitions, but the usual order laws
must be applied with their nonemptiness and boundedness conditions.
The uniform strategy witnesses nonempty indexing types, and
\eqref{eq:payoffbound} supplies bounded ranges for fixed-player payoffs.
The lemmas \decl{iInf_payoff_bounds} and \decl{iSup_payoff_bounds}
then bound the inner extrema; their ranges are bounded in turn.
Consequently \decl{maxminValue_bounds} and \decl{minmaxValue_bounds}
place both values in $[-C_u,C_u]$. Thus every extremum used in
\eqref{eq:values} has the intended real order-theoretic meaning.

\section{The elementary inequality}

\begin{lemma}\label{lem:easy}
For the game described above, $\lowerval\le\upper$.
\end{lemma}
\begin{proof}
For every $x\in\EA$ and $y\in\EB$,
\[
  \inf_{y'\in\EB}\pay(x,y')\le\pay(x,y)
     \le\sup_{x'\in\EA}\pay(x',y).
\]
Taking the supremum over $x$ and then the infimum over $y$ gives
the desired inequality. The nonempty bounded ranges established
above justify these order operations in $\R$.
\end{proof}

The implementation in \source{Minimax/EasyDirection.lean}{\texttt{EasyDirection.lean}}
is a direct transcription. It uses \decl{ciSup_le} and
\decl{le_ciInf} for the two outer comparisons, then composes
\decl{ciInf_le} with \decl{le_ciSup}. The latter two calls
explicitly use \decl{bddBelow_payoff_right} and
\decl{bddAbove_payoff_left}. This direction requires no
saddle-point theorem.

\section{Preparing the Sion application}

\subsection{An ambient coordinate space}
Sion's theorem is expressed for subsets of real topological vector
spaces. A probability-vector structure does not directly provide
that interface. The declaration \decl{coordSimplex S} therefore
defines $\Delta(S)$ as a subset of the ambient function space
$S\to\R$, with its standard pointwise vector operations and
product topology.

The map from \decl{MixedStrategy S} to this set takes the field
\texttt{val}; membership is given by the fields
\texttt{nonneg} and \texttt{sum\_one}. Conversely,
\decl{MixedStrategy.ofCoordSimplex} builds the probability-vector
structure from a coordinate function and its membership proof.
The resulting coordinates are definitionally the original
function. The code needs these two conversions, rather than a
separate transported topology on the structure.

\begin{proposition}\label{prop:simplex}
The coordinate simplex $\Delta(S)$ is nonempty, convex, and compact.
\end{proposition}
\begin{proof}
Nonemptiness follows from the uniform strategy. A convex combination
preserves nonnegativity, and finite-sum distributivity gives
$\sum_s(p x_s+q z_s)=p+q=1$.

For closedness, each constraint $0\le x_s$ defines a closed set
because coordinate evaluation is continuous. Their intersection
is closed. The finite coordinate sum is continuous, so its
level set at $1$ is closed as well. Their intersection is
$\Delta(S)$.

Each coordinate of a point in the simplex lies in $[0,1]$.
Hence $\Delta(S)$ is a closed subset of the compact box
$\prod_{s\in S}[0,1]$, and is compact.
\end{proof}

The corresponding declarations are \decl{coordSimplex_nonempty},
\decl{convex_coordSimplex}, \decl{isClosed_coordSimplex}, and
\decl{isCompact_coordSimplex}. The compactness proof uses
\decl{isCompact_univ_pi}, \decl{isCompact_Icc}, and the
closed-subset compactness principle. Finiteness also makes
the mass constraint a finite continuous sum.

\subsection{Continuity and convexity of payoff sections}
For each fixed $y$, the function $x\mapsto\pay(x,y)$ on the
ambient coordinate space is a finite sum of coordinate evaluations
multiplied by constants. It is continuous. The same argument
applies to $y\mapsto\pay(x,y)$ for fixed $x$.
These facts are proved as
\decl{continuous_weightedPayoff_left} and
\decl{continuous_weightedPayoff_right}; only separate
continuity is needed for the application.

The additivity and scalar-compatibility lemmas from the basic
library are packaged into two private linear maps,
\decl{payoffLeftLinearMap} and \decl{payoffRightLinearMap}.
A linear real-valued function is both convex and concave on a
convex set, since its convex-combination inequality is an equality.
Mathlib then supplies quasiconvexity and quasiconcavity, the weaker
conditions used by Sion. Continuity similarly supplies the
appropriate lower and upper semicontinuity on the simplices.
These properties follow from the finite formula for every $u$;
they are not additional assumptions in the final game theorem.

\section{From a Sion saddle point to minimax}

\subsection{Player order at the library boundary}
The real-valued declaration \decl{Sion.exists_isSaddlePointOn}
used here assumes nonempty compact convex sets $X,Y$; each section
in its first variable is lower semicontinuous and quasiconvex,
and each section in its second variable is upper semicontinuous
and quasiconcave. Its conclusion gives $a\in X$ and $b\in Y$
with
\[
  f(a,y)\le f(x,b)\qquad(x\in X,\ y\in Y).
\]
This is the precise saddle-point interface in the pinned Mathlib
source \cite{MathlibSion}. Both sets are compact in this interface.
Sion's classical equality theorem has more general variants,
including one-compact-set hypotheses \cite{Sion1958}; those
variants are unnecessary for this finite-game application.

The minimizing player occupies the first variable. In
\source{Minimax/HardDirection.lean}{\texttt{HardDirection.lean}}, the instantiation is
\begin{equation}\label{eq:sioninst}
 X=\EB,\qquad Y=\EA,\qquad f(y,x)=\pay(x,y).
\end{equation}
Mathlib returns a minimizing coordinate vector $y$ first and a
maximizing vector $x$ second. Converting them to mixed-strategy
structures gives the following exact property.

\begin{theorem}[Formalized saddle-point property]\label{thm:saddle}
There exist $x_*\in\EA$ and $y_*\in\EB$ such that
\begin{equation}\label{eq:saddle}
  \pay(x',y_*)\le\pay(x_*,y')
  \qquad\text{for all }x'\in\EA,\ y'\in\EB.
\end{equation}
\end{theorem}

The declaration \decl{Minimax.exists_payoff_saddle} states
this property as follows, under the same common hypotheses:
\begin{lstlisting}
∃ x : MixedStrategy A, ∃ y : MixedStrategy B,
  ∀ x' : MixedStrategy A, ∀ y' : MixedStrategy B,
    expPayoff u x' y ≤ expPayoff u x y'
\end{lstlisting}
There are no admitted proof steps in this declaration. Sion's
theorem is a proved dependency, not a new axiom introduced by
the finite-game development.

\subsection{The common value}
Setting $y'=y_*$ and $x'=x_*$ in \eqref{eq:saddle} separately
gives the familiar optimality inequalities
\begin{equation}\label{eq:optimality}
  \pay(x',y_*)\le\pay(x_*,y_*)\le\pay(x_*,y')
  \qquad(x'\in\EA,\ y'\in\EB).
\end{equation}
Thus $y_*$ is a minimizing best response to $x_*$ and $x_*$
is a maximizing best response to $y_*$.

\begin{theorem}[Finite minimax]\label{thm:minimax}
For finite nonempty $A,B$ and every real payoff $u:A\times B\to\R$,
\[
  \sup_{x\in\EA}\inf_{y\in\EB}\pay(x,y)
   =\inf_{y\in\EB}\sup_{x\in\EA}\pay(x,y).
\]
\end{theorem}
\begin{proof}
Choose $x_*,y_*$ from Theorem~\ref{thm:saddle} and set
$v=\pay(x_*,y_*)$. Equation~\eqref{eq:optimality} implies
\[
  \upper\le\sup_{x'\in\EA}\pay(x',y_*)\le v
   \le\inf_{y'\in\EB}\pay(x_*,y')\le\lowerval.
\]
All real supremum and infimum comparisons are justified by the
bounds in Section~2. Combining $\upper\le\lowerval$ with
Lemma~\ref{lem:easy} yields equality by antisymmetry.
\end{proof}

The proof of \decl{minmax_le_maxmin} follows exactly this
chain. The final declaration is a single antisymmetry step:
\begin{lstlisting}
public theorem minimax_theorem (u : A → B → ℝ) :
    maxminValue u = minmaxValue u :=
  le_antisymm (maxmin_le_minmax u) (minmax_le_maxmin u)
\end{lstlisting}
Its full common binder is
\begin{lstlisting}
{A B : Type*} [Fintype A] [Fintype B]
  [Nonempty A] [Nonempty B] (u : A → B → ℝ)
\end{lstlisting}
In particular, $A$ and $B$ may be distinct finite types.

\begin{remark}[Attainment and existence]\label{rem:attain}
Equation~\eqref{eq:optimality}, together with the strategies
themselves as witnesses, also shows that the displayed inner
extrema at $x_*,y_*$ equal $v$, and that $v=\lowerval=\upper$.
This is a mathematical consequence of the formal saddle-point
property and the value definitions. The pinned public interface
exports that property and minimax equality, rather than separate
named declarations for every attainment identity. The development
is noncomputable and does not supply an executable algorithm
for finding optimal strategies from a numerical matrix.
\end{remark}

\subsection{A small interpretive example}
To illustrate the distinction between pure and mixed play,
consider the matching-pennies matrix
\[
 \begin{pmatrix}1&-1\\-1&1\end{pmatrix}.
\]
If the maximizing player chooses the first row with probability
$p$ and the minimizing player chooses the first column with
probability $q$, then the expected payoff is
$(2p-1)(2q-1)$. At $p=q=1/2$ both players guarantee value $0$.
Restricting to pure strategies instead gives maxmin $-1$ and
minmax $1$, so the equality genuinely depends on allowing
randomization. This calculation is an explanatory example here;
the pinned artifact does not contain a dedicated formalized
matching-pennies example.

\section{Artifact structure and verification}

\subsection{Library and statement interface}
The reusable proof is organized into three source modules.
\source{Minimax/Basic.lean}{\texttt{Minimax/Basic.lean}}
defines strategies, payoff, mixing, pure embeddings, bounds,
and values.
\source{Minimax/EasyDirection.lean}{\texttt{Minimax/EasyDirection.lean}}
proves the elementary inequality.
\source{Minimax/HardDirection.lean}{\texttt{Minimax/HardDirection.lean}}
establishes the coordinate-simplex interface and proves saddle
existence, the reverse inequality, and equality.
The top-level \texttt{Minimax.lean} imports the library.

The additional \texttt{Challenge.lean}, \texttt{Solution.lean},
and \texttt{comparator.json} files provide a Palomar-compatible
statement/solution package. The challenge contains a copy of the
strategy structure, three definition holes, and three theorem
placeholders. Its six uses of \texttt{sorry} are intentional
statement-surface placeholders. It imports only the relevant
Mathlib modules and does not import the solution.

The solution imports the actual library and restates the three
proved results in namespace \decl{Minimax.Palomar}, using
the corresponding \decl{Minimax} library theorems.
Challenge and Solution are compiled in separate environments
because their fully qualified statement names coincide.
The comparator lists \decl{expPayoff}, \decl{maxminValue},
and \decl{minmaxValue} as the three definitions, and the
two inequalities plus equality as the three theorem targets.
The strategy structure is copied in the challenge and is not
listed as a definition target.

\subsection{What is checked}
The pinned script \texttt{scripts/verify-palomar.sh} builds the
library and the challenge/solution modules, checks the comparator
declarations and their kinds in the separate environments,
and checks proof tokens and axiom dependencies. Its intended
proof-bearing scope is the library and Solution, which contain
no \texttt{sorry}; it treats the challenge's six deliberate
placeholders separately.

The source audit \texttt{M4\_AUDIT.md} records the checked
declaration signatures and reports that the library and the
three solution theorems depend only on
\decl{propext}, \decl{Classical.choice}, and \decl{Quot.sound}.
These are the permitted axioms recorded by the comparator.
The verification report for the pinned submission, checked on
September 30, 2026, reports a passing build and comparator and
acceptance by Lean's default kernel and the additional
\texttt{con-ron} and \texttt{nanoda} checkers
\cite{VerificationRun}. This dated result is evidence about
that artifact version, rather than a promise about arbitrary
future dependency versions or environments.

Kernel checking establishes the formal conclusions from the
actual definitions and accepted foundations. It does not by
itself certify the interpretation of an informal theorem, the
accuracy of citations, authorship, novelty, or the contents of
this exposition. Those require the source alignment described
here and ordinary scholarly review. Likewise, a passing
mechanical report does not assert repository registration or
publication status.

\subsection{Reproduction and provenance}
For reproduction, retrieve the repository, check out the commit
identified in Section~1, and use the pinned Lean and Mathlib
environment. The artifact's documented entry point is
\texttt{scripts/verify-palomar.sh}; it includes setup specific
to its managed execution environment. The accompanying README
describes that setup, the separate challenge build, and the
comparator invocation. The source code is licensed
\texttt{BSD-3-Clause}; this statement describes the code license
and does not prescribe the license selected for depositing
this manuscript.

The artifact metadata records GPT-6.1 via Codex assistance
for formalization and packaging. AI assistance was also used
in preparing this exposition. The source metadata labels review
as self-assessed. We do not infer a level of human understanding
or independent human review from automated checks. No
person-specific contribution statement is asserted in this note.

\section{Limitations and conclusion}

The formal result covers finite nonempty pure-strategy types,
independent probability-vector mixed strategies, and a single
arbitrary real payoff with opposing player objectives. It does
not cover infinite pure-strategy sets, general multiplayer or
non-zero-sum Nash equilibrium existence, correlated strategies,
or an executable solver. Although the proof ingredient is a
general analytic minimax theorem, the exported game statement
has precisely the finite scope given above.

The specialization shows how a concise classical existence
argument can be connected to a reusable formal interface.
Probability structures provide the game model, explicit bounds
make real extrema safe to manipulate, coordinate simplices
provide the topological vector-space setting, and the Sion
saddle point yields the reverse inequality. The resulting
equality is therefore supported by a transparent chain from
the finite payoff formula to the version-pinned library theorem.

\section*{Acknowledgments}
We acknowledge the Mathlib community \cite{Mathlib2020} and,
in particular, Antoine Chambert-Loir and Anatole Dedecker for
the Sion implementation on which this
development relies.

\bibliographystyle{amsplain}
\bibliography{references}

\end{document}