\documentclass[11pt]{amsart}

\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{booktabs}
\usepackage{array}
\usepackage{xcolor}
\usepackage{fancyvrb}
\usepackage{url}
\usepackage{hyperref}

% ---------------------------------------------------------------------------
% Theorem environments
% ---------------------------------------------------------------------------
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\numberwithin{equation}{section}
\setlength{\emergencystretch}{2em}

% ---------------------------------------------------------------------------
% Macros
% ---------------------------------------------------------------------------
\newcommand{\NN}{\mathbb{N}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\CC}{\mathbb{C}}
\newcommand{\Qbar}{\overline{\mathbb{Q}}}
\newcommand{\Lt}{\widetilde{\mathcal{L}}}
\newcommand{\cL}{\mathcal{L}}
\newcommand{\Ga}{\mathbb{G}_{\mathrm{a}}}
\newcommand{\Gm}{\mathbb{G}_{\mathrm{m}}}
\newcommand{\hdim}{\operatorname{hdim}}
\newcommand{\height}{\operatorname{ht}}
\newcommand{\Lie}{\operatorname{Lie}}
\DeclareUrlCommand\lean{\urlstyle{tt}}

% ---------------------------------------------------------------------------
% Lean code blocks: fancyvrb, with the Unicode used in them mapped for pdflatex
% ---------------------------------------------------------------------------
\fvset{frame=single,fontsize=\footnotesize,xleftmargin=1em,framesep=2mm}
\DeclareUnicodeCharacter{2102}{\ensuremath{\mathbb{C}}}
\DeclareUnicodeCharacter{211A}{\ensuremath{\mathbb{Q}}}
\DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}}
\DeclareUnicodeCharacter{2113}{\ensuremath{\ell}}
\DeclareUnicodeCharacter{03B2}{\ensuremath{\beta}}
\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}}
\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}}
\DeclareUnicodeCharacter{2192}{\ensuremath{\to}}
\DeclareUnicodeCharacter{2208}{\ensuremath{\in}}
\DeclareUnicodeCharacter{2209}{\ensuremath{\notin}}
\DeclareUnicodeCharacter{2227}{\ensuremath{\wedge}}
\DeclareUnicodeCharacter{2211}{\ensuremath{\sum}}

\begin{document}

\title[A Lean formalization of the strong six exponentials theorem]{A Lean formalization of Roy's
strong six exponentials theorem}

\author{Shawn Krisman}

\subjclass[2020]{Primary 11J81; Secondary 11J86, 14L10, 13C14, 68V20}
\keywords{strong six exponentials theorem, linear forms in logarithms, multiplicity estimates,
interpolation determinants, formal verification, Lean}

\date{\today}

\begin{abstract}
We formalize in Lean~4 with Mathlib Roy's strong six exponentials theorem: if $x_1,x_2$ are linearly
independent over $\Qbar$ and $y_1,y_2,y_3$ are linearly independent over $\Qbar$, then one of the six
products $x_iy_j$ lies outside the $\Qbar$-vector space spanned by $1$ and the logarithms of
algebraic numbers. The proof closure uses only Lean's three standard axioms. Along the way the
development proves Waldschmidt's transcendence theorem on $\Ga^{d_0}\times\Gm^{d_1}$ in the form
used by Roy, and Philippon's multiplicity estimate with derivatives on $\Ga^{d_0}\times\Gm^{d_1}$
over every algebraically closed field of characteristic zero, following Roy's account in
Waldschmidt's book. We reproduce the public Lean statements, summarize the mathematical route, and
record how the artifact is verified. The code is available at
\url{https://github.com/telaviv/strong-six-exponentials}.
\end{abstract}

\maketitle

% ===========================================================================
\section{Main theorems}\label{sec:main}
% ===========================================================================

The formalization is public at
\begin{center}
\url{https://github.com/telaviv/strong-six-exponentials},
\end{center}
and the revision described here is pinned in Section~\ref{sec:verify}. The endpoint is
\lean{StrongSix.M2.strongSixExponentials}. Its type is the proposition
\lean{StrongSix.StrongSixExponentials}, defined in \lean{StrongSix/Defs.lean} as follows.

\begin{Verbatim}
def logAlg : Set ℂ := {ℓ | IsAlgebraic ℚ (exp ℓ)}

def LTilde : Set ℂ :=
  {z | ∃ (n : ℕ) (β : Fin (n + 1) → ℂ) (ℓ : Fin n → ℂ),
      (∀ i, IsAlgebraic ℚ (β i)) ∧ (∀ i, ℓ i ∈ logAlg) ∧
      z = β 0 + ∑ i, β i.succ * ℓ i}

def QbarIndep {n : ℕ} (v : Fin n → ℂ) : Prop :=
  ∀ c : Fin n → ℂ, (∀ i, IsAlgebraic ℚ (c i)) →
    ∑ i, c i * v i = 0 → ∀ i, c i = 0

def StrongSixExponentials : Prop :=
  ∀ (x : Fin 2 → ℂ) (y : Fin 3 → ℂ), QbarIndep x → QbarIndep y →
    ∃ i j, x i * y j ∉ LTilde

theorem StrongSix.M2.strongSixExponentials : StrongSixExponentials
\end{Verbatim}
(Docstrings are omitted; the source documents \lean{logAlg} as $\cL$ and \lean{LTilde} as $\Lt$.)
The mathematical content is the following.

\begin{theorem}[Strong six exponentials; Roy {\cite[Cor.~2]{Roy1992}}]\label{thm:strong-six}
Let $\cL=\{\ell\in\CC : e^{\ell}\in\Qbar\}$ and let $\Lt$ be the $\Qbar$-vector space spanned by $1$
and $\cL$. If $x_1,x_2\in\CC$ are linearly independent over $\Qbar$ and $y_1,y_2,y_3\in\CC$ are linearly
independent over $\Qbar$, then $x_iy_j\notin\Lt$ for some $i\in\{1,2\}$ and $j\in\{1,2,3\}$.
\end{theorem}

Here $\Qbar$ is the algebraic closure of $\QQ$ in $\CC$; "algebraic" means algebraic over $\QQ$, and
$\cL$ contains every branch of the logarithm of every nonzero algebraic number. Roy states
\cite[Cor.~2]{Roy1992} for $2\times3$ matrices: a $2\times3$ matrix with entries in $\Lt$ whose rows
and whose columns are linearly independent over $\Qbar$ has rank $2$. Theorem~\ref{thm:strong-six} is
the case of the rank-one matrix $(x_iy_j)$, whose rows and columns are $\Qbar$-independent exactly
when $x$ and $y$ are. The Lean set
\lean{LTilde} is the set of finite sums $\beta_0+\sum_i\beta_i\ell_i$ with $\beta_i\in\Qbar$ and
$\ell_i\in\cL$, which is exactly the $\Qbar$-span of $\{1\}\cup\cL$. The predicate \lean{QbarIndep}
is linear independence over $\Qbar$, phrased with complex coefficients that are required to be
algebraic.

\begin{remark}\label{rem:qbar}
Independence over $\Qbar$, not over $\QQ$, is essential. Since $\Lt$ is a $\Qbar$-vector space, the
$\QQ$-independent families $x=(1,\sqrt2)$ and $y=(\log2,\log3,\log5)$ put all six products in $\Lt$.
An independent review of the statements (Section~\ref{sec:verify}) checked that the Lean
definitions use $\Qbar$-independence; an earlier version of our README stated the theorem with
$\QQ$-independence, which is false.
\end{remark}

The development exposes four further endpoints, all with the same axiom closure.

\begin{center}
\begin{tabular}{@{}lp{0.42\textwidth}@{}}
\toprule
Declaration & Content \\
\midrule
\lean{StrongSix.M2.waldschmidtTheorem1} & Theorem~\ref{thm:waldschmidt} \\
\lean{StrongSix.M2.multEst_of_isAlgClosed} & Theorem~\ref{thm:multest}, any $K=\overline K$, $\operatorname{char}K=0$ \\
\lean{StrongSix.M2.multEst_Qb} & Theorem~\ref{thm:multest} for $K=\Qbar$ \\
\lean{StrongSix.SixExp.six_exponentials} & six exponentials theorem \cite[Ch.~2]{Lang1966}, \cite{Ramachandra1968} \\
\bottomrule
\end{tabular}
\end{center}

The six exponentials theorem (with $\QQ$-independence and the conclusion
$e^{x_iy_j}\notin\Qbar$ for some $i,j$) is proved separately by the classical auxiliary-function
method; it is not used in the proof of Theorem~\ref{thm:strong-six}.

\subsection{Waldschmidt's theorem}
Write $d=d_0+d_1$, $E=\CC^{d_0}\times\CC^{d_1}$, and $\Omega=0\times 2\pi i\,\QQ^{d_1}\subset E$. A
$\CC$-subspace of $E$ is \emph{rational over $\Qbar$} if it is spanned by vectors with algebraic
coordinates. The proposition \lean{StrongSix.Roy.WaldschmidtTheorem1} transcribes the following
statement \cite[Thm.~1]{Roy1992}, which Roy derives from \cite[Thm.~4.1]{Waldschmidt1988}.

\begin{theorem}[Waldschmidt]\label{thm:waldschmidt}
Let $Y\subset\Qbar^{d_0}\times\cL^{d_1}$ be a finite-dimensional $\QQ$-subspace of $E$, let $W\subset E$
be a $\CC$-subspace rational over $\Qbar$, and let $V\ne E$ be a $\CC$-subspace containing $Y$ and
$W$. Then there are $d_0',d_1'$ and a surjective $\CC$-linear map
$s:E\to E'=\CC^{d_0'}\times\CC^{d_1'}$ with $s(\Qbar^{d_0}\times0)\subset\Qbar^{d_0'}\times0$ and
$s(0\times\QQ^{d_1})\subset0\times\QQ^{d_1'}$, such that $s(W)\ne E'$ and
\[
\frac{d_1'-\dim_\QQ\bigl(s(Y)\cap\Omega'\bigr)+\dim_\QQ s(Y)}{d_0'+d_1'-\dim_\CC s(W)}
\;\le\;
\frac{d_1-\dim_\QQ(Y\cap\Omega)}{d_0+d_1-\dim_\CC V}.
\]
\end{theorem}

\subsection{The multiplicity estimate}\label{sec:multest-stmt}
The interface between the analytic and the algebraic halves of the proof is the proposition
\lean{StrongSix.Thm1.MultEst}~$K$. Points of $G=\Ga^{d_0}\times\Gm^{d_1}$ are pairs
$g=(x,y)\in K^{d_0}\times(K^\times)^{d_1}$, polynomials live in $K[X_1,\dots,X_{d_0},Y_1,\dots,Y_{d_1}]$,
and $w=(\xi,\eta)\in K^{d}$ acts by the invariant derivation
$D_w=\sum_k\xi_k\,\partial/\partial X_k+\sum_j\eta_jY_j\,\partial/\partial Y_j$. A polynomial
$P$ \emph{vanishes to order $\ge k$ along $W$ at $g$} if $D_{w_1}\cdots D_{w_r}P(g)=0$ for all $r<k$
and $w_i\in W$. Connected algebraic subgroups are $H=h_0\times T_U$ with $h_0\subset K^{d_0}$ a
subspace, $U\subset\QQ^{d_1}$ a subspace and $T_U=\{y:y^\varphi=1 \text{ for all }\varphi\in U\cap\ZZ^{d_1}\}$;
then $\Lie H=h_0\times U^\perp$. Two points are \emph{equivalent modulo $H$} if they differ by an
element of $H$.

\begin{theorem}[Multiplicity estimate; Philippon \cite{Philippon1986}, in the form of Roy
{\cite[Ch.~8]{DALAG}}]\label{thm:multest}
Let $K$ be algebraically closed of characteristic $0$ and $d=d_0+d_1$. Put
$C=d^{\,d}d_0^{\,d_0}d_1^{\,d_1}\,d!\,2^{d_1}$. Let $W\subset K^d$ be a subspace, $S\subset G(K)$ a finite
set containing the identity, $T,D_0,D_1\ge1$, and $P\ne0$ a polynomial of degree $\le D_0$ in $X$ and
$\le D_1$ in $Y$. Suppose $P$ vanishes to order $\ge dT+1$ along $W$ at every point
$\sigma_1+\dots+\sigma_d$ with $\sigma_i\in S$. Then there is a connected algebraic subgroup
$H=h_0\times T_U\ne G$ such that every subset $F\subset S$ of pairwise inequivalent points modulo $H$
satisfies
\[
T^{\,\ell}\,|F|\,D_0^{\dim h_0}D_1^{\,d_1-\dim U}\;\le\;C\,D_0^{d_0}D_1^{d_1},
\qquad \ell=\dim W-\dim\bigl(W\cap\Lie H\bigr).
\]
\end{theorem}

The Lean proposition \lean{MultEst}~$K$ asserts the existence of \emph{some} constant $C(d_0,d_1)$;
the proof produces the explicit constant above (\lean{StrongSix.M2.Cst}).

\begin{remark}
Theorem~\ref{thm:waldschmidt} is the case $G=\Ga^{d_0}\times\Gm^{d_1}$ of Waldschmidt's theorem
\cite[Thm.~4.1]{Waldschmidt1988}, often called the linear subgroup theorem. As explained in
\cite[Ch.~13]{WaldschmidtLIL}, special cases of that theorem contain Baker's theorem on linear forms in
logarithms, both homogeneous and non-homogeneous. We have not stated or derived Baker's theorem
itself from it in Lean; a Lean proof of the qualitative form of Baker's theorem, by a different route,
is in \cite{DiazModulus}.
\end{remark}

% ===========================================================================
\section{Mathematical route}\label{sec:route}
% ===========================================================================

The proof has three parts: the multiplicity estimate (Theorem~\ref{thm:multest}), the deduction of
Waldschmidt's theorem from it, and Roy's deduction of strong six from Waldschmidt's theorem:
\[
\text{Thm.~\ref{thm:multest}}\ \Longrightarrow\ \text{Thm.~\ref{thm:waldschmidt}}
\ \Longrightarrow\ \text{Thm.~\ref{thm:strong-six}}.
\]
We describe them in the reverse order.

\subsection{From Waldschmidt's theorem to strong six (Roy's reduction)}
We follow \cite[\S\S1--4]{Roy1992}. Roy works in an \emph{admissible} category in which kernels
and cokernels exist and compose, with additive and upper-additive functions on objects; his
Section~3 shows that four statements about such functions are equivalent. We encode an admissible
category only through the existence of kernels, cokernels and exact triples, which is all the
argument uses (\lean{Roy/Abstract.lean}). The concrete category is realized as subquotients
$T/S$ of a fixed ambient $(E,Y,W,V)$, with $S\le T$ products of a $\Qbar$-rational and a
$\QQ$-rational subspace (\lean{Roy/Subquot.lean}). Each subquotient is realized in coordinates by a
map preserving the $\Qbar$- and $\QQ$-structures (\lean{Roy/Realize.lean},
\lean{Roy/Transport.lean}), so Theorem~\ref{thm:waldschmidt} applies to every object; this gives
Roy's Theorem~1bis and then his Theorem~2bis. For strong six one writes
$x_iy_j=\beta^{(ij)}_0+\sum_r\beta^{(ij)}_{r+1}\ell^{(ij)}_r$, chooses a $\QQ$-basis
$\omega_1,\dots,\omega_m$ of the number field generated by all $\beta$, and lifts the products to
$\ell_{kj}\in\Qbar^2\times\cL^{2m}$. With $W=\ker\varphi$, $V=\varphi^{-1}(\CC x)$ and
$Y=\operatorname{span}_\QQ\{\ell_{kj}\}$, Theorem~2bis gives $(2m+\dim Y)/2\le 2m$, whereas
$\Qbar$-independence of $y$ gives $\dim Y\ge3m$ (\lean{Roy/Core.lean}, \lean{Roy/Final.lean}). This
layer is about $2{,}700$ lines.

\subsection{From the multiplicity estimate to Waldschmidt's theorem}
This is a transcendence proof by Laurent's interpolation determinants \cite{Laurent1994}, in the
setting of \cite[Ch.~4, 9, 11]{WaldschmidtLIL}; the choice of parameters is our own derivation.
A first reduction (\lean{Thm1/Reduce.lean}) quotients by $\CC\cdot(Y\cap\Omega)$ and disposes of
the cases $\dim V=0$ and $\dim V<d_0$. In the main case all parameters are powers of one integer
base $\beta$ (\lean{Thm1/Params.lean}). Rows of the interpolation matrix are pairs (derivation
word of length $<T$ over a basis of $W$, grid point $\sum s_i\eta_i$); columns are monomials
$X^aY^b$ of bidegree $\le(L_0,L_1)$.
\begin{itemize}
\item If the columns are dependent, a kernel vector is a nonzero polynomial vanishing along $W$ on
the grid. Theorem~\ref{thm:multest} over $\Qbar$ yields an obstruction subgroup $H=h_0\times T_U$,
which is turned into the map $s$ of Theorem~\ref{thm:waldschmidt} (\lean{Thm1/Quot.lean}); a count
of inequivalent grid points (\lean{Thm1/Count.lean}) gives the inequality.
\item Otherwise a maximal minor $\Delta$ is nonzero. The analytic side bounds $|\Delta|$ from above
through $\Psi(z)=\det\bigl(D^{t_\nu}f_\lambda(z\zeta_\nu)\bigr)$, which vanishes to order
$M(N-M^n)-\sum t_\nu$ at $0$ by a rank count (\lean{Thm1/Rank.lean}, \lean{Thm1/InterpDet.lean});
analytic derivatives of $P(v_0,e^{v_1})$ are identified with the invariant derivations
(\lean{Thm1/Deriv.lean}). The arithmetic side gives Liouville's lower bound from heights of the
entries in a number field (\lean{Thm1/Heights.lean}, \lean{Thm1/Core4.lean}). For large $\beta$
the two bounds are incompatible (\lean{Thm1/Growth.lean}).
\end{itemize}
This layer is about $3{,}900$ lines.

\subsection{The multiplicity estimate}
Philippon's original proof works with multihomogeneous ideals in $\mathbb P^{d_0}\times\mathbb
P^{d_1}$. We follow instead Roy's affine treatment \cite[Ch.~5 and 8]{DALAG}, which reduces the
deep input to a single theorem of commutative algebra. Let $B=K[X,Y,Z]$ with $d_0+2d_1$ variables,
$G$ embedded by $(x,y)\mapsto(x,y,y^{-1})$, and $I_G=(Y_jZ_j-1)_j$.

\emph{Filtered Hilbert functions.} For an ideal $J\subset B$ and $D=(D_0,D_1)$ let
$H(J;t)=\dim F_{tD}-\dim(J\cap F_{tD})$, where $F_{tD}$ is the space of polynomials of block degree
$\le tD$. A Veronese-type bridge to graded Hilbert--Serre theory shows that $H(J;t)$ is eventually
polynomial, so $J$ has a Hilbert dimension $\hdim J$ and degree. The key bridge is
\begin{equation}\label{eq:bridge}
\hdim L+\height L=d_0+2d_1\qquad\text{for every proper ideal }L\subset B,
\end{equation}
proved from Macaulay's unmixedness theorem for polynomial rings (an ideal of height $r$ generated by
$r$ elements is unmixed) together with the height of maximal ideals. Unmixedness comes from a port of
Guan and Hu's Cohen--Macaulay library \cite{GuanHu2025} to our Mathlib version (about $2{,}200$
lines, Section~\ref{sec:verify}); see \cite[Thm.~17.6]{Matsumura} for the mathematics.

\emph{B\'ezout} (Roy's Theorem 8.4). If $I_G\subset A=I_G+(F)$ with $F$ of block degree $\le D$, then
$\deg A\le\deg I_G$. The proof builds a complete-intersection chain, choosing each new generator
outside the associated primes by an avoidance argument over an infinite field.

\emph{Algebraic subgroups.} An algebraic subgroup of $G$ has the form $V\times T_\Lambda$
(Roy's Proposition 5.6), proved through linear independence of exponential polynomials; we also
compute its Hilbert dimension and a lower bound for its degree, separate distinct cosets, and
show that the connected component has finite index.

\emph{Wüstholz's lemma} (Roy's Lemmas 8.14--8.16, Theorem 8.18 \cite{Wustholz1989}). If every element
of $A$ vanishes to order $>S_0$ along $W$ on a finite union of cosets $\Gamma+G'$ with ideal $J$,
then $H(A;t+c)\ge (k+1)^\ell H(J;t)$ whenever $\ell k\le S_0$. Roy's argument uses the multi-index
operators $D^\alpha$ and the commutativity of the $D_w$. We instead apply derivations along
\emph{words} of indices and index the products $Q^m$ by multisets, which removes the need for
commutativity; the products $P_aQ^{m_a}$ are then shown to be linearly independent modulo $A$.

\emph{The main argument} (Roy \S8.4.1). Let $L_r=I_G+(\tau_\sigma D_l P:\sigma\in\Sigma[r],\ |l|\le
rT)$. Since $I(G)$ is prime (the torus is irreducible, proved by mapping $B$ into the domain
$K[X,Y][1/\prod Y_j]$), $\hdim L_0<d$, and a pigeonhole argument gives $r<d$ with
$\hdim L_r=\hdim L_{r+1}$. Roy now takes an irreducible component common to the zero sets of $L_r$
and $L_{r+1}$. We avoid component theory: we take a prime $p\supseteq L_{r+1}$ with
$\hdim p=\hdim L_r$ (which exists by \eqref{eq:bridge}) and show that any such prime is a minimal
prime of $L_r$, by strict decrease of $\hdim$ along chains of primes. With $V=Z(p)$ and the
Nullstellensatz, the stabilizer $G_V=\{h:hV\subseteq V\}$ is an algebraic subgroup, and the zero
set of $A=I_G+(P'\circ\tau_v:P'\in L_r,\ v\in V)$ is covered by finitely many cosets of $G_V$, one
for each minimal prime of $L_r$ hit. The elements of $A$ vanish to order $>T$ along $W$ on $S+G_V$;
since that set of elements is an ideal (by Leibniz' rule), this is checked on generators. Finally
B\'ezout, Wüstholz's lemma, coset separation and the two degree bounds for $G_V^{0}$ and $I_G$ give
the inequality of Theorem~\ref{thm:multest}. This layer, without the ported library, is about
$6{,}600$ lines.

% ===========================================================================
\section{AI-assisted formalization}\label{sec:workflow}
% ===========================================================================

The Lean code, the planning documents and the text of this paper were produced by AI models
(Claude, Anthropic; mainly Claude Opus~5.5) working in Claude Code under the direction of the
author. Work was organized by written plans (not part of the published repository): an overall
blueprint, a plan for deducing Theorem~\ref{thm:waldschmidt} from Theorem~\ref{thm:multest}, and a
plan for proving Theorem~\ref{thm:multest}. The deduction of Theorem~\ref{thm:waldschmidt} was
first proved with Theorem~\ref{thm:multest} as an explicit hypothesis, so that the implication could
be checked before the multiplicity estimate was attempted. The plan for the multiplicity estimate
was revised once: after a first attempt along Philippon's projective proof, the route was switched to Roy's affine treatment, whose only deep input is the
unmixedness theorem; that input was obtained by porting an existing library rather than proving
it from scratch.

An independent AI review session, separate from the one that wrote the proofs, checked the
statements of Theorems~\ref{thm:strong-six}--\ref{thm:multest} against their sources, the chain of
endpoint declarations, and the axiom closure. It found no problem with the Lean statements or the
proof. It did find that the README stated the theorem with the wrong (and false) independence
hypothesis; this has been corrected (Remark~\ref{rem:qbar}).

Apart from the check by the Lean kernel, all verification so far has been carried out by AI
systems. No human expert has yet reviewed the Lean definitions against the literature or read the
proofs; we would be grateful for corrections. The author is responsible for the intended
statements and for the claims made here.

% ===========================================================================
\section{Formal artifact and verification}\label{sec:verify}
% ===========================================================================

The formalization uses Lean~4 \cite{Lean4} and Mathlib \cite{Mathlib}.

\begin{center}\small
\begin{tabular}{@{}ll@{}}
\toprule
Repository & \url{https://github.com/telaviv/strong-six-exponentials} \\
Commit & \lean{1625bdf3c0a7d9222bacd876d738d7540109bea6} \\
Lean & \lean{leanprover/lean4:v4.35.0} \\
Mathlib & \lean{v4.35.0} \\
Mathlib commit & \lean{56a005855ea17e0b0958f73ec801ae140b0a1679} \\
\bottomrule
\end{tabular}
\end{center}

The toolchain and package revisions are pinned in \lean{lean-toolchain} and
\lean{lake-manifest.json}. The library \lean{StrongSix} has 76 files and about $16{,}600$ lines:

\begin{center}
\begin{tabular}{@{}lrp{0.52\textwidth}@{}}
\toprule
Directory & Lines & Content \\
\midrule
\lean{Roy/} & 2{,}734 & Theorem~\ref{thm:waldschmidt} $\Rightarrow$ Theorem~\ref{thm:strong-six} (Roy's reduction) \\
\lean{Thm1/} & 3{,}918 & Theorem~\ref{thm:multest} $\Rightarrow$ Theorem~\ref{thm:waldschmidt} \\
\lean{M2/} & 6{,}634 & the multiplicity estimate (Theorem~\ref{thm:multest}) \\
\lean{CM/} & 2{,}201 & ported Cohen--Macaulay library \\
other & 1{,}138 & \lean{SixExp/} (six exponentials), \lean{Analytic/}, \lean{Arith/}, \lean{Defs.lean} \\
\bottomrule
\end{tabular}
\end{center}

\emph{Third-party code.} \lean{StrongSix/CM/} is a port of Guan and Hu's Cohen--Macaulay files
\cite{GuanHu2025} from their Mathlib fork (\url{https://github.com/Thmoas-Guan/mathlib4_fork}, branch
\lean{ABS-Criterion-Project-new}, commit \lean{0ff6e01f}; Apache-2.0). The original headers are
kept, and local changes are marked \lean{PORT}.

To build the library at the pinned revision:
\begin{Verbatim}
git clone https://github.com/telaviv/strong-six-exponentials
cd strong-six-exponentials
git checkout 1625bdf3c0a7d9222bacd876d738d7540109bea6
lake exe cache get
lake build
\end{Verbatim}
To inspect the endpoint and its axiom closure, run \texttt{lake env lean Axioms.lean}. The file
contains, among \texttt{\#print axioms} queries for the main intermediate results,
\begin{Verbatim}
#check (StrongSix.M2.strongSixExponentials :
  StrongSix.StrongSixExponentials)
#print axioms StrongSix.M2.strongSixExponentials
#print axioms StrongSix.M2.waldschmidtTheorem1
#print axioms StrongSix.M2.multEst_of_isAlgClosed
#print axioms StrongSix.M2.multEst_Qb
\end{Verbatim}
Every query yields \texttt{[propext, Classical.choice, Quot.sound]}. The source contains no
\lean{sorry}, no \lean{axiom} declaration and no \lean{native_decide}. These checks concern the named
declarations and their dependencies; the mathematical meaning of the result also depends on the
definitions in \lean{Defs.lean}, reproduced in Section~\ref{sec:main} for review. (The statement
\lean{Roy/Theorem1.lean} of Theorem~\ref{thm:waldschmidt} matters only for the intermediate
endpoint \lean{waldschmidtTheorem1}.)

% ===========================================================================
\section{Related work}\label{sec:related}
% ===========================================================================

Karatarakis and Wiedijk formalized the Gelfond--Schneider theorem in Lean
\cite{KaratarakisWiedijk2026}. The library \cite{DiazModulus} proves, among other classical results,
the six exponentials theorem and the qualitative form of Baker's theorem (by the Bertrand--Masser
route, without a zero estimate), and it carries Roy's strong six exponentials theorem as an explicit
hypothesis of several statements; Theorem~\ref{thm:strong-six} could discharge that hypothesis. We
are not aware of an earlier formalization of a zero estimate or a multiplicity estimate in any proof
assistant.

% ===========================================================================
\section*{Acknowledgements}
% ===========================================================================

We thank Nailin Guan and Yongle Hu for their Cohen--Macaulay library, and Michel Waldschmidt for
making \cite{DALAG} and \cite{WaldschmidtLIL} freely available.

\bibliographystyle{amsplain}
\bibliography{references}

\end{document}