Motivation

In the last of the twenty-four questions that closed his 1982 survey Three-dimensional manifolds, Kleinian groups and hyperbolic geometry (Bull. Amer. Math. Soc. 6 (1982), 357–381), Thurston asked to "show that volumes of hyperbolic $3$-manifolds are not all rationally related" (p. 380). Twenty-two of the twenty-four have since been answered — geometrization by Perelman, tameness by Agol and by Calegari–Gabai, the ending lamination conjecture by Brock–Canary–Minsky, virtual fibering by Agol — and this one is among the two that remain open.

Some rational relations are forced, and for a trivial reason: a degree $n$ cover of a hyperbolic $3$-manifold has $n$ times its volume, so any two commensurable manifolds have rationally related volumes. The question, which remains open, is whether every rational relation arises that way — equivalently, whether some two hyperbolic $3$-manifolds have irrational volume ratio. Remarkably, not a single such pair is known.

Setting

The bundle fixes the meaning of every term. Hyperbolic $3$-space is the upper half-space $\{(x,y,z) : z > 0\}$. Its volume is Lebesgue measure with density $z^{-3}$ — the Riemannian volume of the metric $(dx^2+dy^2+dz^2)/z^2$ written out, so that no Riemannian machinery is required. The hyperbolic distance is given by its closed formula

$$\cosh d(p,q) \;=\; 1 + \frac{|p-q|^2}{2\,p_3\,q_3}.$$

A Kleinian action is a free, properly discontinuous action by hyperbolic isometries; the quotient is a complete hyperbolic $3$-manifold, discreteness and torsion freeness being consequences rather than hypotheses. The volume of the quotient is the measure of a fundamental domain, in the sense of Mathlib's MeasureTheory.IsFundamentalDomain, and the set of volumes collects those that are finite and positive.

Two conventions are stated rather than derived, and are worth flagging. Isometries are not required to preserve orientation, so the set of volumes also contains those of non-orientable quotients; this enlarges the set but not its $\mathbb{Q}$-span, so neither goal is affected. And preservation of the hyperbolic volume is a field of the structure rather than a consequence of preserving the distance: it holds for every hyperbolic isometry, but deriving it amounts to classifying $\mathrm{Isom}(\mathbb{H}^3)$, which is not the subject of this mission.

Formalization targets

The goal is that the volumes are not all rationally related: there are two of them, $v$ and $w$, with $v \neq q w$ for every rational $q$.

Two milestones support it. The first is that passing to a subgroup of index $n$ multiplies the volume by $n$, a fundamental domain for the subgroup being the union of $n$ translates of one for the whole group; this is the source of every known rational relation, and it is why the question is phrased as it is. The second is that the set of volumes is nonempty — that some finite-volume hyperbolic $3$-manifold exists at all — without which the goal would be vacuously false rather than open.

A stronger form of the question, that the $\mathbb{Q}$-span of the set of volumes is infinite dimensional, is also stated.

Significance

The question is a geometric statement whose difficulty is arithmetic. For the Bianchi groups of an imaginary quadratic field $F$, Humbert's formula gives the covolume as $|\delta_F|^{3/2}\zeta_F(2)/4\pi^2$, so the ratio of two such volumes is, up to explicit algebraic factors, a ratio of Dedekind zeta values at $2$; and Neumann and Yang showed that the Bloch invariant of a hyperbolic $3$-manifold lies in a subgroup of finite $\mathbb{Q}$-rank determined by its invariant trace field, so that manifolds sharing an invariant trace field with a single complex place, such as an imaginary quadratic one, have rationally related volumes. Producing one irrational ratio therefore means separating two such transcendentals — a statement of the same order of difficulty as the irrationality of $\zeta(5)$. The value of formalizing the question is not that it will be closed, but that its statement, and the elementary relations that make its naive form false, are pinned down exactly.

Motivation

The inverse Galois problem asks whether every finite group $G$ occurs as the Galois group of a finite Galois extension of $\mathbb{Q}$. For finite simple groups, a large part of the problem was settled by the rigidity method (Shih, Fried, Belyi, Matzat, Thompson) and its refinements such as the braid-group method. Between 1984 and 1989 this machinery realized 25 of the 26 sporadic simple groups as Galois groups over $\mathbb{Q}$, in fact as Galois groups of regular extensions of $\mathbb{Q}(t)$. The Mathieu group $M_{23}$ was the single exception.

Timeline.

• 1985–1987: Hoyden-Siedersleben and Häfner obtained regular $M_{23}$-extensions of $k(t)$ for $k=\mathbb{Q}(\sqrt{-23})$ and $k=\mathbb{Q}(\sqrt{-7})$, by passing through $M_{24}$.
• 1996: Granboulan constructed a regular $M_{23}$-extension of $k(t)$ for every field $k$ over which a certain conic has a point; that conic has no rational point.
• 2013: Elkies computed the four complex polynomials $P$ of degree 23 with $\mathrm{Gal}(P(x)-t/\mathbb{C}(t))\cong M_{23}$; each is defined over a quartic number field.
• 2026: Huang, Jackson, Lee, Poonen, Pries and Zhang (arXiv:2608.08538) produced an explicit regular $M_{23}$-extension of $\mathbb{Q}(t)$ and explicit degree-23 polynomials over $\mathbb{Q}$ with Galois group $M_{23}$, completing the program for the sporadic groups.

Setting

$S_{23}$ denotes the group of permutations of the 23 points $\{1,\dots,23\}$, acting on the left, so $(\sigma\tau)(x)=\sigma(\tau(x))$. The paper fixes three explicit permutations

$$g_1=(1,11)(2,23)(3,8)(4,16)(5,21)(7,20)(15,19)(18,22),$$ $$g_2=(1,2,11,10,16,9,6,3,23,19,20,14,21,17,4,8,22,5,18,15,13,7,12),$$ $$g_3=(1,2,3,4,10,11,12,7,19,18,8,6,9,16,17,21,22,5,14,20,13,15,23),$$

and the Mathieu group $M_{23}$ is the subgroup of $S_{23}$ generated by $g_1$ and $g_2$. A $G$-extension of a field $k$ is a Galois extension $L/k$ together with an isomorphism $\mathrm{Gal}(L/k)\cong G$. A finite extension $L$ of $\mathbb{Q}(t)$ is regular if it contains no nontrivial algebraic extension of $\mathbb{Q}$.

For a triple of conjugacy classes $(C_1,C_2,C_3)$ of $M_{23}$, the set $\Sigma_c$ consists of triples $(h_1,h_2,h_3)\in C_1\times C_2\times C_3$ with $h_1h_2h_3=1$ that generate $M_{23}$, and the Nielsen class $\mathrm{Ni}_c$ is the set of orbits of $\Sigma_c$ under simultaneous conjugation by $M_{23}$. The paper works with the classes $C_1=2$, $C_2=23A$, $C_3=23B$, represented by $g_1,g_2,g_3$.

Formalization targets

Goal (Theorem 1.1)

$$\exists\ K/\mathbb{Q}\ \text{finite Galois with}\ \mathrm{Gal}(K/\mathbb{Q})\cong M_{23}.$$

Stronger forms

• Theorem 1.3: there is a finite Galois extension $L/\mathbb{Q}(t)$, regular over $\mathbb{Q}$, with $\mathrm{Gal}(L/\mathbb{Q}(t))\cong M_{23}$.
• Examples 1.2 and 3.7: two explicit monic degree-23 polynomials in $\mathbb{Z}[x]$ whose splitting fields are $M_{23}$-extensions of $\mathbb{Q}$, unramified outside $\{2,3,23\}$ and $\{2,7,23\}$ respectively.

Supporting milestones

Facts about $M_{23}$ stated in §3 (order $10{,}200{,}960$, simplicity, 4-transitivity, 17 conjugacy classes), the membership $(g_1,g_2,g_3)\in\Sigma_c$, the count $|\mathrm{Ni}_c|=7$, the Riemann–Hurwitz count of Lemma 3.1, the hyperbolic triangle of Lemma 3.2, and the group-theoretic step of Corollary 3.6 ($M_{23}$ is not normal in any strictly larger subgroup of $S_{23}$).

Significance

Theorem 1.1 removes the last sporadic exception: combined with earlier work, every sporadic simple group is the Galois group of a regular extension of $\mathbb{Q}(t)$ (Corollary 1.4), and hence occurs as a Galois group over every number field, in infinitely many mutually independent ways.

The paper's proof is computer-assisted: Belyi maps were computed numerically and the final claims were certified in Magma and PARI/GP. No machine-checked proof in a proof assistant is known. A formal proof of the explicit-polynomial statements (Examples 1.2 and 3.7) would give an independent, kernel-checked certificate of Theorem 1.1. The group-theoretic milestones (order, simplicity, transitivity, class counts, the Nielsen count) are reusable for any later work on $M_{23}$ or the other Mathieu groups.

Difficulty

The rigidity method fails for $M_{23}$: for every $G_{\mathbb{Q}}$-stable triple of conjugacy classes the Nielsen class has size different from $1$, so no rational point of a Hurwitz space is forced. The smallest positive size, $|\mathrm{Ni}_c|=7$ for $\{2,23A,23B\}$, leaves seven covers, and the fact that one of them has field of moduli $\mathbb{Q}$ was found by explicit computation, with no conceptual explanation. Certifying that a particular degree-23 polynomial has Galois group exactly $M_{23}$ requires both a lower bound (the group contains $M_{23}$, for instance via cycle types and the classification of transitive groups of degree 23) and an upper bound (the group is contained in a conjugate of $M_{23}$, for instance via resolvents or reduction modulo primes). Neither bound is a finite check inside current Mathlib.

Formalization scope

$S_{23}$ is Equiv.Perm (Fin 23). The paper's point $k$ corresponds to k - 1 : Fin 23, and permutations compose as functions, which matches the paper's left-action convention. $M_{23}$ is defined as Subgroup.closure {g₁, g₂}, so it is not described up to isomorphism. Galois groups are groups of field automorphisms, K ≃ₐ[ℚ] K, and a $G$-extension is recorded as a group isomorphism with $M_{23}$. $\mathbb{Q}(t)$ is RatFunc ℚ. "Unramified outside $S$" for a number field is encoded as "every prime dividing the absolute discriminant lies in $S$", which is equivalent by Dedekind's discriminant theorem. The Nielsen class is the set of orbits of $\Sigma_c$ under simultaneous conjugation. Hyperbolic angles in the Poincaré disk are defined through the hyperbolic law of cosines.

The geometric statements Lemma 3.3 and Proposition 3.5 concern the numerically computed curve $X_{\mathbb{C}}$ and the polynomial $F(T,V)$, which the paper does not print, so they are not milestones. Lemma 3.1 enters only through its Riemann–Hurwitz count.

Contributions are welcome on decidable certificates for permutation-group facts in Lean, on Galois-group certification for explicit polynomials, and on Hilbert irreducibility.

Selected references

• X. Huang, B. Jackson, K.-H. Lee, B. Poonen, R. Pries, S. Zhang, The Mathieu group $M_{23}$ is a Galois group over $\mathbb{Q}$, 2026. https://arxiv.org/abs/2608.08538
• G. Malle, B. H. Matzat, Inverse Galois Theory, 2nd ed., Springer, 2018.
• J.-P. Serre, Topics in Galois Theory, Jones and Bartlett, 1992.
• N. D. Elkies, The complex polynomials $P(x)$ with $\mathrm{Gal}(P(x)-t)\cong M_{23}$, ANTS X, Open Book Series 1, 2013.
• M. D. Fried, H. Völklein, The inverse Galois problem and rational points on moduli spaces, Math. Ann. 290 (1991), 771–800.

Motivation

The irrationality measure $\mu(\pi)$ is the supremum of the $\mu$ for which $|\pi - p/q| < q^{-\mu}$ has infinitely many rational solutions $p/q$. Every irrational number has $\mu \ge 2$ (Dirichlet), almost every real number has $\mu = 2$, and it is conjectured that $\mu(\pi) = 2$. Known upper bounds:

• Mahler (1953): $42$, the first proof that $\pi$ is not a Liouville number.
• Mignotte (1974): $20.6$.
• Chudnovsky (1982): $19.8899944\ldots$
• Rhin–Viola (1993): $14.797074$.
• Hata (1993): $8.016045\ldots$
• Salikhov (2008): $7.606308\ldots$
• Zeilberger–Zudilin (2020): $7.103205334137\ldots$, the current record.

The campaign's first proved value is Mahler's $42$. This entry records Zeilberger–Zudilin's bound.

Formalization target

The campaign template with the value $7.103205334138$ filled in: PiIrrationality.UpperBound (7.103205334138 : ℝ), i.e. $\mu(\pi) \le 7.103205334138$.

Value. The paper states its bound as $7.103205334137\ldots$, a truncation. This entry rounds the last digit up to $7.103205334138$ so that the goal follows from the published proof.

How the bound arises

Zeilberger and Zudilin modify Salikhov's integrals and use the Almkvist–Zeilberger algorithm (creative telescoping) to find recurrences for them, then optimise the arithmetic and analytic estimates. This is the current record.

Significance

Each step down the list replaces Mahler's approximations with a sharper family. Formalizing $7.103205334138$ would build reusable explicit machinery: integral constructions of rational approximations to $\pi$, bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.

Selected references

• D. Zeilberger, W. Zudilin, The irrationality measure of $\pi$ is at most $7.103205334137\ldots$, Moscow J. Combin. Number Theory 9 (2020), no. 4, 407–419. https://arxiv.org/abs/1912.06345
• K. Mahler, On the approximation of $\pi$, Indag. Math. 15 (1953), 30–42.
• F. Beukers, A rational approach to $\pi$, Nieuw Arch. Wiskd. (5) 1 (2000), 372–379.
• Source table: https://teorth.github.io/optimizationproblems/constants/7a.html

Motivation

Given a monic polynomial $f$ with integer coefficients, one can reduce it modulo each prime $p$ and factor it over the finite field $\mathbb F_p$. The way $f$ factors changes with $p$, and the question of how often each factorization pattern occurs has a precise answer: Chebotarëv's density theorem (1922). It is the common generalization of Dirichlet's theorem on primes in arithmetic progressions (1837) and a theorem of Frobenius (1880, published 1896), and it underlies a large part of algebraic number theory, for example the fact that a Galois extension of a number field is determined by the set of primes that split completely in it. This mission follows the elementary exposition of P. Stevenhagen and H. W. Lenstra, Jr. (Math. Intelligencer 18 (1996)), which states all three theorems over $\mathbb Q$ with a minimum of terminology.

Timeline.

• 1837 — Dirichlet: primes are equidistributed (in analytic density) over the invertible residue classes modulo $m$.
• 1880/1896 — Frobenius: the density of primes with a given decomposition type of $f$ modulo $p$ equals the proportion of Galois group elements with that cycle pattern; he conjectures the sharper statement for conjugacy classes.
• 1896 — de la Vallée-Poussin: Dirichlet's theorem for natural density.
• 1922/1925 — Chebotarëv proves Frobenius's conjecture, without class field theory.
• 1935 — Deuring's proof via Artin reciprocity, now the textbook route.

Setting

Let $f\in\mathbb Z[X]$ be monic of degree $n$ with nonzero discriminant $\Delta(f)$, so that $f$ has $n$ distinct complex zeros $\alpha_1,\dots,\alpha_n$. Let $K=\mathbb Q(\alpha_1,\dots,\alpha_n)$ be its splitting field and $G=\mathrm{Gal}(K/\mathbb Q)$ its Galois group. Every $\sigma\in G$ permutes the zeros; the lengths of the cycles (including cycles of length 1) form the cycle pattern of $\sigma$, a partition of $n$.

For a prime $p\nmid\Delta(f)$, the degrees of the irreducible factors of $f \bmod p$ over $\mathbb F_p$ form the decomposition type of $f$ modulo $p$, again a partition of $n$.

A Frobenius substitution of $p$ is an element $\sigma\in G$ such that, for some prime ideal $\mathfrak Q$ of the ring of integers $\mathcal O_K$ lying over $p$,

$$\sigma(x)\equiv x^p \pmod{\mathfrak Q}\qquad\text{for all }x\in\mathcal O_K .$$

For $p\nmid\Delta(f)$ these elements form a single conjugacy class of $G$, written $\sigma_p$.

A set $S$ of primes has (analytic, or Dirichlet) density $\delta$ if

$$\frac{\sum_{p\in S}p^{-s}}{\log\frac{1}{s-1}}\longrightarrow\delta\qquad(s\downarrow 1),$$

and natural density $\delta$ if $\#\{p\le x:p\in S\}/\#\{p\le x\}\to\delta$ as $x\to\infty$.

Formalization targets

Goal: Chebotarëv's density theorem

For every conjugacy class $C$ of $G$,

$$\text{the set }\{p \text{ prime}: p\nmid\Delta(f),\ \sigma_p\in C\}\text{ has analytic density }\frac{\#C}{\#G}.$$

Milestones

1. Theorem of Dirichlet: for $m\ge1$ and $\gcd(a,m)=1$, the primes $p\equiv a \pmod m$ have density $1/\varphi(m)$.
2. A set of primes with natural density $\delta$ has analytic density $\delta$.
3. Galois theory of finite fields: for a squarefree $g\in\mathbb F_p[X]$, the cycle pattern of $x\mapsto x^p$ on the zeros of $g$ equals the decomposition type of $g$.
4. For $p\nmid\Delta(f)$, the Frobenius substitutions of $p$ form exactly one conjugacy class of $G$.
5. For $p\nmid\Delta(f)$, the cycle pattern of $\sigma_p$ equals the decomposition type of $f$ modulo $p$.
6. For $f=X^m-1$ and $p\nmid m$, $\sigma_p(\zeta)=\zeta^p$ for every primitive $m$-th root of unity $\zeta$; that is, $\sigma_p$ corresponds to $p \bmod m$ under $G\cong(\mathbb Z/m\mathbb Z)^\times$.
7. Theorem of Frobenius: the primes $p\nmid\Delta(f)$ for which $f$ has a given decomposition type $t$ have density $\#\{\sigma\in G:\text{cycle pattern }t\}/\#G$.

Significance

Chebotarëv's theorem shows that every conjugacy class of the Galois group occurs as a Frobenius class for infinitely many primes, with a predictable frequency. Its standard consequences include: the Frobenius elements are equidistributed; a Galois extension is determined by its completely split primes; if $f$ has a zero modulo almost every prime then $f$ is linear or reducible; prime ideals are equidistributed over ideal classes. The theorem is the first step in many arguments in arithmetic geometry (e.g. Serre's work on $\ell$-adic representations).

The theorem is classical and proved; this mission is about formalizing it. Mathlib contains Frobenius elements in Galois extensions of Dedekind domains and Dirichlet's theorem in the form "infinitely many primes in each coprime residue class", but, to our knowledge, neither the density form of Dirichlet's theorem nor Frobenius's or Chebotarëv's density theorem.

Difficulty

The Galois-theoretic parts (milestones 3–6) are standard but require connecting Frobenius elements in $\mathcal O_K$ with factorization of $f$ modulo $p$, including the fact that $p\nmid\Delta(f)$ forces $p$ to be unramified in $K$. The analytic core is harder: one needs Dedekind zeta functions and $L$-functions of number fields and their behaviour at $s=1$. The reduction of the general case to the cyclotomic case (Chebotarëv's "crossing" with cyclotomic extensions) needs the density statement over an arbitrary number field as base, not only over $\mathbb Q$; in particular, the statement over $\mathbb Q$ alone cannot be proved by induction on itself.

Formalization scope

All declarations live in the namespace ChebotarevDensity and share one definition file.

• $K$ is Mathlib's SplittingField of $f$ viewed in $\mathbb Q[X]$; $G$ is Polynomial.Gal; $\Delta(f)$ is Mathlib's Polynomial.discr.
• A Frobenius substitution is expressed with Mathlib's IsArithFrobAt at some prime ideal of $\mathcal O_K$ containing $p$; "$\sigma_p\in C$" means that some Frobenius substitution of $p$ lies in $C$ (for $p\nmid\Delta(f)$ this is equivalent to all of them lying in $C$, by milestone 4).
• The cycle pattern is Equiv.Perm.partition of the permutation induced on the complex zeros of $f$; it includes fixed points.
• The decomposition type is the multiset of degrees of the normalized (monic) irreducible factors of $f \bmod p$.
• Analytic density uses $\sum' p^{-s}$ over the primes of $S$ and the limit $s\to1^+$ within $(1,\infty)$; natural density compares prime counts up to $x\in\mathbb N$.
• The hypotheses $\Delta(f)\neq0$ and "$f$ monic" are those of the source; the theorems are not vacuous, since e.g. $f=X^m-1$ satisfies them.

Welcome contributions: Dedekind zeta functions and Hecke $L$-functions at $s=1$, the density form of Dirichlet's theorem, unramifiedness of primes not dividing the discriminant, and the general number-field version of the theorem.

Selected references

• P. Stevenhagen, H. W. Lenstra, Jr., Chebotarëv and his density theorem, Math. Intelligencer 18 (1996), no. 2, 26–37. doi:10.1007/BF03027290
• N. Tschebotareff, Die Bestimmung der Dichtigkeit einer Menge von Primzahlen, welche zu einer gegebenen Substitutionsklasse gehören, Math. Ann. 95 (1925), 191–228. doi:10.1007/BF01206606
• S. Lang, Algebraic Number Theory, Addison-Wesley, 1970, Chap. VIII.
• J. Neukirch, Class Field Theory, Springer, 1986, Chap. V.
• Chebotarev density theorem, Wikipedia. link

Motivation

A classical way to recognize an algebraic function is through the arithmetic of its Taylor coefficients. Eisenstein's theorem (1852) says that if a power series $f\in\mathbb{Q}[[z]]$ is algebraic over $\mathbb{Q}[z]$, only finitely many primes occur in the denominators of its coefficients. The converse fails in general: many transcendental power series have integer coefficients. Lam and Litt (arXiv:2501.13175) conjecture that the converse does hold for power series that solve an algebraic differential equation at a non-singular point, and that even a weak control on denominators — primes $p$ may appear, but only after roughly $\omega(p)\gg p$ coefficients — already forces algebraicity.

For linear differential equations, the conjecture is a strengthening of the Grothendieck–Katz $p$-curvature conjecture, one of the central open problems about algebraic solutions of linear differential equations (arXiv:2501.13175). The bounded-denominator form is Problem 1 on Litt's list of open problems (problemsilike.com/1).

Timeline.

• 1852 — Eisenstein: algebraic power series over $\mathbb{Q}$ have bounded denominators (implication (1)⇒(2) below).
• 1970s — Grothendieck and Katz: the $p$-curvature conjecture for linear differential equations.
• 2025 — Lam and Litt formulate the conjecture for (possibly non-linear) algebraic differential equations and prove it for many equations and initial conditions of algebro-geometric interest, including Picard–Fuchs equations at initial conditions corresponding to cycle classes, and isomonodromy equations such as Painlevé VI and the Schlesinger system at initial conditions corresponding to Picard–Fuchs equations (arXiv:2501.13175).

Setting

Let $f=\sum_{k\ge0}a_kz^k\in\mathbb{Q}[[z]]$ be a formal power series with rational coefficients and write $f^{(i)}$ for its $i$-th formal derivative. Let $g\in\mathbb{Q}(z,y_0,\dots,y_{n-1})$ be a rational function in $n+1$ variables. The series $f$ solves the algebraic ODE defined by $g$ if

$$f^{(n)}(z)=g\bigl(z,f(z),f'(z),\dots,f^{(n-1)}(z)\bigr)$$

and $g$ is defined at $\bigl(0,f(0),\dots,f^{(n-1)}(0)\bigr)$. Concretely, $g=p/q$ for polynomials $p,q$ with $q\bigl(0,f(0),\dots,f^{(n-1)}(0)\bigr)\neq0$ and $f^{(n)}\cdot q(z,f,\dots,f^{(n-1)})=p(z,f,\dots,f^{(n-1)})$.

For $N\in\mathbb{N}$, $\mathbb{Z}[1/N]\subseteq\mathbb{Q}$ is the subring generated by $1/N$. For a function $\omega$ from the primes to $\mathbb{Z}$, the coefficients of $f$ are $\omega$-integral if for every prime $p$ the numbers $a_0,\dots,a_{\omega(p)}$ lie in $\mathbb{Z}_{(p)}$ (denominators prime to $p$); $\omega$ is superlinear if $\omega(p)/p\to\infty$.

Formalization targets

Goal: the Lam–Litt conjecture

For $f$ solving an algebraic ODE as above, the following are equivalent:

$$\text{(1) } f \text{ is algebraic over } \mathbb{Q}[z];\qquad \text{(2) } \exists N,\ \forall k,\ a_k\in\mathbb{Z}[1/N];\qquad \text{(3) } \exists\,\omega \text{ superlinear with } (a_k) \ \omega\text{-integral}.$$

Milestones

• (1)⇒(2), Eisenstein's theorem (no ODE hypothesis needed).
• (2)⇒(3), elementary (no ODE hypothesis needed).
• (3)⇒(2), open.
• (2)⇒(1), open; Litt's Problem 1.

Together the four milestones imply the goal; the last two are the open content of the conjecture.

Significance

A proof would give an arithmetic criterion for algebraicity of solutions of arbitrary algebraic differential equations, and, for linear equations, would imply the Grothendieck–Katz $p$-curvature conjecture (arXiv:2501.13175). Lam and Litt draw algebro-geometric consequences from the cases they prove.

For formalization: the conjecture is open, so the goal and the two open milestones are research targets. Eisenstein's theorem is a classical result; formalizing it is concrete, self-contained work. The implication (2)⇒(3) is elementary. The cases proved by Lam and Litt are candidates for further milestones.

Difficulty

Integrality of coefficients alone does not detect algebraicity: there are transcendental power series with integer coefficients that satisfy linear differential equations, such as $\sum_k\binom{2k}{k}^2z^k$. Its equation is singular at $z=0$, which the non-singularity hypothesis on $g$ excludes; the conjecture asserts that at non-singular points such examples cannot occur. Even for linear equations the statement contains the Grothendieck–Katz conjecture, which is open in general.

Formalization scope

• Power series are PowerSeries ℚ with the formal derivative; rational functions are the fraction field of MvPolynomial (Fin (n + 1)) ℚ, where variable 0 is $z$ and variable i + 1 is $f^{(i)}$.
• The ODE hypothesis is existential: some representation $g=p/q$ with $q$ nonzero at the initial point and $f^{(n)}q(\dots)=p(\dots)$ as power series. This non-singularity requirement is essential and must not be dropped.
• Algebraicity is IsAlgebraic (Polynomial ℚ) f, i.e. over $\mathbb{Q}[z]$ (equivalently over $\mathbb{Q}(z)$).
• $\mathbb{Z}[1/N]$ is the subalgebra of $\mathbb{Q}$ generated by $1/N$; since $1/0=0$ in Lean, $N=0$ gives $\mathbb{Z}$.
• $\omega$ takes values in $\mathbb{Z}$; negative values impose no condition at that prime. Superlinearity is the limit $\omega(p)/p\to\infty$ along the primes.
• The goal is a List.TFAE of the three conditions.

Useful infrastructure: formal derivatives and substitution for power series, algebraic power series and their coefficient arithmetic (Eisenstein), and $p$-adic valuations of coefficients. Formalizations of Eisenstein's theorem and of the special cases proved by Lam and Litt are welcome.

Selected references

• Y. H. J. Lam, D. Litt, Algebraicity and integrality of solutions to differential equations, arXiv preprint, 2025. https://arxiv.org/abs/2501.13175
• D. Litt, Problem 1, problems list. https://www.problemsilike.com/1
• G. Eisenstein, Über eine allgemeine Eigenschaft der Reihen-Entwicklungen aller algebraischen Funktionen, Bericht der Königl. Preuss. Akademie der Wissenschaften zu Berlin, 1852.
• Formal Conjectures project, FormalConjectures/LittProblems/1.lean. https://github.com/google-deepmind/formal-conjectures

Motivation

Cutting planes for mixed-integer linear programs are often derived from convex sets that contain no integer point in their interior. Balas observed in 1971 that every such lattice-free convex set containing the current fractional LP solution in its interior yields a valid inequality, the intersection cut (Balas, Intersection cuts, Oper. Res. 19, 1971). The strongest cuts come from sets that are inclusionwise maximal, so the shape of maximal lattice-free convex sets matters to multi-row cut generation.

The case where the set lives in a subspace arises in practice. Taking $q$ rows of an optimal simplex tableau restricts the integer points to an affine subspace $f+W$ of $\mathbb R^q$ spanned by the tableau columns. When $W$ is irrational, its integer points span only a proper subspace $V\subsetneq W$. The classical theory does not cover this case, and it is the case that the second mission of this series (minimal valid inequalities of the relaxation $R_f(W)$) needs.

Timeline.

• Lovász (Geometry of numbers and integer programming, 1989) stated the characterization for rational subspaces (Proposition 3.1) and gave only a sketch of the proof. The irrational-hyperplane case is not visible in that sketch.
• Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543v1; Math. Oper. Res. 35(3), 2010, doi:10.1287/moor.1100.0461) gave a complete proof of Lovász's theorem for an arbitrary lattice of a linear space (Theorem 10). They also extended it to a space $W$ strictly larger than the span $V$ of the lattice (Theorem 9, equivalently Theorem 1 for $\mathbb Z^n$).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product and the open balls $B_\varepsilon(x)$. For $X\subseteq\mathbb R^n$, $\langle X\rangle$ denotes its linear span.

A lattice of a linear space $V$ is an additive group $\Lambda=\{\lambda_1a_1+\dots+\lambda_ma_m\mid\lambda_i\in\mathbb Z\}$ generated by linearly independent vectors $a_1,\dots,a_m$ with $\langle a_1,\dots,a_m\rangle=V$ (Definition 6, IsLatticeOf Λ V). A linear subspace $L\subseteq V$ is a $\Lambda$-subspace if it has a basis contained in $\Lambda$ (Definition 7, IsLambdaSubspace Λ V L). For $\mathbb Z^2$, the line $x_2=2x_1$ is a $\Lambda$-subspace and the line $x_2=\sqrt2x_1$ is not.

For sets $W,S$ the interior relative to $W$ is $\mathbf{int}_W(S)=\{x\in S\mid B_\varepsilon(x)\cap W\subseteq S\text{ for some }\varepsilon>0\}$ (intW W S). The relative interior is $\mathbf{relint}(S)=\mathbf{int}_{\operatorname{aff}(S)}(S)$.

Let $W\supseteq V$ be a linear space. A set $S$ is a $\Lambda$-free convex set of $W$ if $S\subseteq W$, $S$ is convex and $\Lambda\cap\mathbf{int}_W(S)=\emptyset$. It is maximal if no other $\Lambda$-free convex set of $W$ properly contains it (Definition 8, IsLambdaFree, IsMaxLambdaFree).

The statements also use a polyhedron in $W$ ($W$ intersected with finitely many closed half-spaces), a polytope (convex hull of a finite set), the dimension $\dim(S)$ of the affine hull with $\dim\emptyset=-1$ (affDim), and a facet: a nonempty face $S\cap\{\langle a,x\rangle=b\}$ of a valid inequality with $\dim F=\dim S-1$. The recession cone is $\operatorname{rec}(S)=\{r\mid x+tr\in S\ \forall x\in S,\ t\ge0\}$ and the lineality space is $\operatorname{rec}(S)\cap-\operatorname{rec}(S)$.

Formalization targets

Goal: Theorem 9 (p. 8)

For a lattice $\Lambda$ of $V$ and a linear space $W\supseteq V$ with $\dim W\ge1$, a set $S$ is a maximal $\Lambda$-free convex set of $W$ if and only if

$$\text{(i) } S \text{ is a full-dimensional polyhedron in } W,\ S\cap V \text{ is maximal } \Lambda\text{-free in } V,\ F\mapsto F\cap V \text{ is a bijection of facets};$$ $$\text{(ii) } S=v+L \text{ is a hyperplane of } W \text{ with } L\cap V \text{ a hyperplane of } V \text{ that is not a } \Lambda\text{-subspace};$$ $$\text{(iii) } S \text{ is a half-space of } W \text{ containing } V \text{ on its boundary.}$$

Main milestone: Theorem 10 (p. 8)

For $\dim V\ge1$, $S$ is a maximal $\Lambda$-free convex set of $V$ if and only if either $S=P+L$ is a polyhedron with $P$ a polytope, $L$ a $\Lambda$-subspace and $\dim S=\dim P+\dim L=\dim V$, with no lattice point in $\mathbf{int}_V(S)$ and a lattice point in the relative interior of every facet; or $S=v+L$ is an affine hyperplane of $V$ whose direction $L$ is not a $\Lambda$-subspace.

Supporting milestones

Lemma 13 (bounded full-dimensional case), Lemma 15 (lattice points near half-lines), Lemma 16 ($S+\langle\operatorname{rec}S\rangle$ stays $\Lambda$-free), Lemma 17 (projection along a $\Lambda$-subspace is a lattice), Lemma 18 (lattice points near non-lattice subspaces), Lemma 19 (maximal hyperplanes), Claims 1 and 2 in the proof of Theorem 10, and identity (6), $\mathbf{int}_W(S)\cap V=\mathbf{int}_V(S\cap V)$.

Significance

Theorem 10 says that maximal lattice-free sets are cylinders over polytopes with a lattice point on every facet, apart from the irrational hyperplanes. This is the structural fact behind the finiteness of facet counts (at most $2^{\dim P}$) and behind every classification of maximal lattice-free sets in low dimension, such as the triangles and quadrilaterals of the two-row relaxation. Theorem 9 extends it to irrational subspaces. There the new cases are the half-spaces of (iii), which have $V$ on their boundary, and the hyperplanes of (ii), whose trace on $V$ is a hyperplane of $V$ that is not a $\Lambda$-subspace. Theorem 9 is the geometric input to the paper's Theorem 3: every minimal valid inequality of $R_f(W)$ is the gauge of a maximal lattice-free convex set of $f+W$.

These results are proved on paper. No machine-checked version of Lovász's theorem, of Theorem 9, or of the lattice-approximation Lemmas 15 and 18 is known to exist. The mission produces the definitions of lattices of subspaces, relative interiors and lattice-free sets on which the second mission of the series builds.

Difficulty

The obvious argument separates each lattice point from $S$ by a half-space and intersects the half-spaces. It gives a polyhedron only when finitely many lattice points matter, that is, when $S$ is bounded. For unbounded $S$, the recession directions must be shown to be lineality directions and to be spanned by lattice vectors. Both steps rest on simultaneous Diophantine approximation (Dirichlet's theorem) applied in irrational directions, and on a density argument for the projected lattice when the lineality space is not a $\Lambda$-subspace. In the subspace setting of Theorem 9, one must also track the interiors relative to $W$ and to $V$ separately. Identity (6) holds only when $\mathbf{int}_W(S)$ meets $V$, and the half-space case (iii) is exactly the case where it does not.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), linear spaces are Submodule ℝ, and $\Lambda$ is an AddSubgroup. All declarations live in the namespace MaxLatticeFree.Geometry. Every interior is relative (intW, relint). With the ambient topological interior, every subset of a proper subspace would be trivially lattice-free, and the classification would collapse. A lattice must have a linearly independent generating family; a dense finitely generated subgroup such as $\mathbb Z+\sqrt2\mathbb Z$ is excluded. Dimensions are integers with $\dim\emptyset=-1$, and facets are nonempty, so no dimension equation holds through truncated subtraction.

Two readings of the page are fixed.

1. Theorem 9 assumes $\dim W\ge1$ and Theorem 10 assumes $\dim V\ge1$. For $W=V=\{0\}$ the only maximal set is $\emptyset$, which satisfies none of the listed cases, so the printed statements are false there.
2. Identity (6) is stated under the three hypotheses its proof uses, not inside the case analysis of Theorem 9.

The paper's Theorem 1 (the same result for $\mathbb Z^n$ and affine $W$) is not included, and neither are the cited results of Barvinok and Dirichlet (Theorems 11, 14, Corollary 12). They are welcome as supporting lemmas. Infrastructure that is useful beyond this mission includes Dirichlet's simultaneous approximation theorem in $\mathbb R^m$, discreteness of lattices of subspaces, and the relation between intW/relint and Mathlib's intrinsicInterior.

Selected references

• A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543
• L. Lovász, Geometry of numbers and integer programming, in: Mathematical Programming: Recent Developments and Applications, 1989, pp. 177–210.
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
• A. Barvinok, A Course in Convexity, Graduate Studies in Mathematics 54, AMS, 2002. https://doi.org/10.1090/gsm/054

Motivation

For a field $F$, two invariants built from very different data turn out to carry the same mod-2 information. One is Milnor K-theory $K^M_n(F)$, defined by generators and relations from the multiplicative group $F^\times$ alone. The other is Galois cohomology $H^n(F,\mathbb{Z}/2)$, the continuous cohomology of the absolute Galois group of $F$. In 1970 Milnor considered a natural map $K^M_n(F)/2 \to H^n(F,\mathbb{Z}/2)$ in all degrees, verified that it is an isomorphism for several classes of fields, and remarked that he knew of no field where it fails (Milnor 1970). The statement that it is always an isomorphism when $\operatorname{char} F \neq 2$ became known as the Milnor conjecture. Its companion conjecture on quadratic forms was later deduced from it (Orlov–Vishik–Voevodsky 2007). Together they identify the graded Witt ring of quadratic forms, Galois cohomology mod 2, and $K^M_*(F)/2$.

Timeline. The attributions below follow the introduction of Voevodsky 2003.

• 1970: Milnor considers the map $K^M_n(F)/2 \to H^n(F,\mathbb{Z}/2)$ in all degrees and gives classes of fields where it is an isomorphism (Milnor 1970).
• Bass–Tate (published 1973): the Kummer classes satisfy the Steinberg relation, so the Kummer map extends to a ring homomorphism on $K^M_*(F)$ (Bass–Tate 1973).
• Degrees 0 and 1: the map is an isomorphism, by Kummer theory and Hilbert's Theorem 90.
• 1981: Merkurjev proves degree 2 with $2$ as the coefficient prime.
• 1982: Merkurjev and Suslin extend degree 2 to every prime $\ell$ (Merkurjev–Suslin 1982).
• Degree 3, $\ell = 2$: proved by Merkurjev–Suslin and, independently, by Rost.
• 2003: Voevodsky proves all degrees, in every characteristic $\neq 2$ (Voevodsky 2003, Cor. 7.5), using the motivic Steenrod operations constructed in Voevodsky 2003b. This work was cited for his 2002 Fields Medal.
• 2011: the analogue for odd primes, the Bloch–Kato conjecture, is proved (Voevodsky 2011); a book-length account is Haesemeyer–Weibel 2019.

Setting

Let $F$ be a field with $2 \neq 0$ in $F$.

Milnor K-theory. For $n \ge 0$, $K^M_n(F)$ is the quotient of the $n$-fold tensor power $(F^\times)^{\otimes n}$, taken over $\mathbb{Z}$ with $F^\times$ written additively, by the subgroup generated by the pure tensors $a_1\otimes\cdots\otimes a_n$ in which some adjacent pair satisfies $a_i + a_{i+1} = 1$. This is the degree-$n$ part of $T(F^\times)/I$, where $I$ is the two-sided ideal generated by $a\otimes(1-a)$. The class of $a_1\otimes\cdots\otimes a_n$ is the symbol $\{a_1,\dots,a_n\}$. In particular $K^M_0(F) = \mathbb{Z}$ and $K^M_1(F) = F^\times$. In Lean these are MilnorK F n and symbol a for a : Fin n → Fˣ.

Galois cohomology. Let $F^{\mathrm{sep}}$ be a separable closure and $G_F = \operatorname{Gal}(F^{\mathrm{sep}}/F)$ the absolute Galois group, a profinite group under the Krull topology. $H^n(F,\mathbb{Z}/2)$ is the continuous cohomology $H^n_{\mathrm{cts}}(G_F,\mathbb{Z}/2)$ with trivial action, computed from $G_F$-invariant continuous homogeneous cochains. In Lean this is H F n, Mathlib's continuousCohomology n of the trivial representation.

The Galois symbol. For $a \in F^\times$ fix $\sqrt a \in F^{\mathrm{sep}}$. The Kummer character $\chi_a : G_F \to \mathbb{Z}/2$ is $\chi_a(\sigma) = 0$ if $\sigma(\sqrt a) = \sqrt a$ and $1$ otherwise. It is a continuous homomorphism representing the Kummer class $\delta a \in H^1$. The Galois symbol of $(a_1,\dots,a_n)$ is the class of the homogeneous cocycle

$$(x_0,\dots,x_n)\ \longmapsto\ \prod_{j=1}^{n}\bigl(\chi_{a_j}(x_j)-\chi_{a_j}(x_{j-1})\bigr),$$

the homogeneous form of $(\sigma_1,\dots,\sigma_n) \mapsto \chi_{a_1}(\sigma_1)\cdots\chi_{a_n}(\sigma_n)$, i.e. the cup product $\delta a_1\cup\cdots\cup\delta a_n$. In Lean this is galoisSymbol a.

Formalization targets

Goal: the Milnor conjecture (Voevodsky 2003, Corollary 7.5)

For every field $F$ with $\operatorname{char} F \neq 2$ and every $n \ge 0$ there is a homomorphism

$$\varphi : K^M_n(F) \to H^n(F,\mathbb{Z}/2),\qquad \varphi\{a_1,\dots,a_n\} = \delta a_1\cup\cdots\cup\delta a_n,$$

which is surjective and whose kernel is exactly $2\,K^M_n(F)$.

Since symbols generate $K^M_n(F)$, such a $\varphi$ is unique; it is the norm residue homomorphism. The statement is therefore equivalent to $K^M_n(F)/2 \cong H^n(F,\mathbb{Z}/2)$ via the norm residue map. Its existence, i.e. the fact that the Steinberg relations map to zero, is part of the claim.

Significance

The result itself. The theorem gives a presentation of mod-2 Galois cohomology by generators and relations: every class is a sum of cup products of degree-one classes, and every relation among such products comes from Steinberg relations and multiples of 2. With Orlov–Vishik–Voevodsky 2007 it yields Milnor's conjecture on quadratic forms, which classifies quadratic forms up to Witt equivalence by their Galois-cohomological invariants.

Formalizing it. The theorem is proved but not formalized. At the time of writing, Mathlib has neither Milnor K-theory nor cup products in group or continuous cohomology, and has Hilbert 90 only for finite Galois extensions. This mission's definitions provide a sorry-free Galois symbol in Mathlib's continuous cohomology, which already makes the degree 0 and degree 1 cases (Kummer theory) meaningful targets. A complete development would formalize the IHES proof, including motivic cohomology with $\mathbb{Z}/2$ coefficients and the motivic Steenrod algebra. No part of that is currently available in Lean. Related existing work: on this platform, a graded cup product (groupCohomology.exists_isGradedCupProduct) and a Kummer theory and Hilbert 90 for level-constant cocycles have been formalized on top of Mathlib's discrete groupCohomology. The cup product is for discrete groups, and the Kummer and Hilbert 90 results use finite-level hypotheses in place of continuity, so none of them transfers directly to continuousCohomology.

Difficulty

Degrees 0 and 1 follow from Kummer theory and Hilbert 90. Degree 2 is Merkurjev's theorem, whose proof goes through the K-theory of Severi–Brauer varieties. No argument internal to Galois cohomology or K-theory of fields is known in higher degrees. The known proof reformulates the statement as a vanishing theorem for motivic cohomology of fields, the "Hilbert 90" property for weight $n$. It then argues by induction on $n$ through geometry over $F$: splitting varieties of symbols (Pfister quadrics), their motives, and cohomology operations on motivic cohomology. Each of these is a substantial theory, none of it exists in Mathlib, and the induction passes through statements about arbitrary smooth varieties, not only fields.

Formalization scope

Scope. The target is the Milnor conjecture, i.e. the prime $2$ with coefficients $\mathbb{Z}/2 \cong \mu_2$. The Bloch–Kato conjecture for odd primes is out of scope.

Conventions.

• The field is F : Type, universe 0. Mathlib's continuousCohomology requires the coefficient module to live in the universe of the group. For $F$ in a higher universe this forces ULift (ZMod 2), for which the needed Module and ContinuousSMul instances are not available as global instances. Universe polymorphism is not part of this mission. It does not follow by plain transport, since a field in a higher universe need not be isomorphic to any field in Type; one route is a limit argument, using that both sides commute with directed unions of fields and that every field is the directed union of its countable subfields, each isomorphic to a field in Type.
• The hypothesis $\operatorname{char} F \neq 2$ is [NeZero (2 : F)].
• $H^n$ is Mathlib's continuousCohomology, built from homogeneous cochains, with $\mathbb{Z}/2$ as a trivial representation of $G_F$ with the Krull topology.
• $K^M_n(F)$ is defined one degree at a time, not as a graded ring.
• "Kernel $= 2K^M_n$" means $\varphi(x)=0 \iff \exists y,\ x = 2y$.

Ruling out trivializations. The Galois symbol is not a free parameter. It is a fixed, sorry-free definition, and the existence of $\varphi$ with the prescribed values on symbols is part of the goal. Neither can be chosen to make the statement vacuous.

Route. Reductions should follow Voevodsky 2003 together with Voevodsky 2003b. That route avoids resolution of singularities and works in every characteristic $\neq 2$. The following rely on resolution of singularities (or on characteristic-0 reductions) and should not be used as inputs:

• Mazza–Voevodsky–Weibel (MVW 2006), results 16.24, 16.25 and 20.1, and the cdh-topology and compactly-supported-motive material;
• the original Suslin–Voevodsky paper relating Bloch–Kato to Beilinson–Lichtenbaum (Suslin–Voevodsky 2000); use Haesemeyer–Weibel 2019, Chapter 2, instead;
• Haesemeyer–Weibel Part II, and their reduction to characteristic 0 (Lemma 1.3);
• Voevodsky's 1995–96 preprints on the Milnor conjecture.

Infrastructure needed and reusable. A complete development needs:

• the ring structure on $K^M_*(F)$ (cf. Carlier's KMilnorWitt for Milnor–Witt K-theory);
• cup products in continuous cohomology;
• Hilbert 90 for profinite Galois groups;
• Galois cohomology as étale cohomology of $\operatorname{Spec} F$;
• the Nisnevich topology;
• presheaves with transfers, motivic complexes and motivic cohomology;
• motivic Steenrod operations;
• motives of Pfister quadrics.

Most of this is reusable well beyond the mission. The homogeneous-cochain construction in the definition files, which turns an invariant continuous cocycle $G^{n+1}\to M$ into a class in Mathlib's continuousCohomology, applies to any locally compact group with trivial coefficients. Contributions of any of these components, and of the degree 0 and 1 cases, are welcome.

Selected references

• V. Voevodsky, Motivic cohomology with $\mathbb{Z}/2$-coefficients, Publ. Math. IHÉS 98 (2003), 59–104. https://doi.org/10.1007/s10240-003-0010-6
• V. Voevodsky, Reduced power operations in motivic cohomology, Publ. Math. IHÉS 98 (2003), 1–57. https://doi.org/10.1007/s10240-003-0009-z
• J. Milnor, Algebraic K-theory and quadratic forms, Invent. Math. 9 (1970), 318–344. https://doi.org/10.1007/BF01425486
• H. Bass, J. Tate, The Milnor ring of a global field, in Algebraic K-theory II, Lecture Notes in Math. 342, Springer, 1973. https://doi.org/10.1007/BFb0073733
• A. S. Merkurjev, A. A. Suslin, K-cohomology of Severi–Brauer varieties and the norm residue homomorphism, Math. USSR Izv. 21 (1983). https://doi.org/10.1070/IM1983v021n02ABEH001793
• D. Orlov, A. Vishik, V. Voevodsky, An exact sequence for $K^M_*/2$ with applications to quadratic forms, Ann. of Math. 165 (2007), 1–13. https://doi.org/10.4007/annals.2007.165.1
• V. Voevodsky, On motivic cohomology with $\mathbb{Z}/l$-coefficients, Ann. of Math. 174 (2011), 401–438. https://doi.org/10.4007/annals.2011.174.1.11
• C. Haesemeyer, C. Weibel, The Norm Residue Theorem in Motivic Cohomology, Annals of Math. Studies 200, Princeton, 2019. https://doi.org/10.1515/9780691189635
• C. Mazza, V. Voevodsky, C. Weibel, Lecture Notes on Motivic Cohomology, Clay Math. Monographs 2, AMS, 2006. https://www.claymath.org/wp-content/uploads/2022/03/Motivic-Cohomology.pdf
• A. Suslin, V. Voevodsky, Bloch–Kato conjecture and motivic cohomology with finite coefficients, in The Arithmetic and Geometry of Algebraic Cycles, NATO Sci. Ser. C 548, Kluwer, 2000. https://doi.org/10.1007/978-94-011-4098-0_5

Erdős Problem 68: Irrationality of sum 1/(n! - 1)

Problem Statement & Context

Erdős Problem 68 asks whether the infinite series 184987\sum_{n=2}^{\infty} rac{1}{n! - 1}184987 is irrational.

Paul Erdős proved in 1948 that \sum_{n=1}^{\infty} rac{1}{2^n - 1} is irrational, but the problem for factorial denominators ! - 1$ remains open.

Main Target Theorem

Why multiplicity estimates matter

Formalization status, 29 September 2026: fourteen of the 26 individual paper targets are Proved, including Theorem 2.1, Propositions 3.3 and 4.7, and Lemma 5.1. Four of eight milestones are complete. The full-paper goal remains Open: the corollaries, remaining supporting claims, and both 1987 addenda remain part of the mission. The proved multiplicity theorem now supports the completed Senthil Kumar target.

An auxiliary polynomial in a transcendence proof is constructed to vanish to high order at many points. A multiplicity estimate limits how often that can happen without a geometric reason: a positive-dimensional algebraic subgroup can make the apparent vanishing conditions dependent. Such estimates are used to turn analytic approximations into algebraic-independence conclusions. The theory applies to products of commutative algebraic groups with both archimedean and nonarchimedean analytic directions.

The mission's objective is a faithful formalization of the complete 1986 paper, Patrice Philippon's Lemmes de zéros dans les groupes algébriques commutatifs, including every theorem, corollary, proposition, lemma, definition, and mathematical supporting claim. All results remain required whether or not a current application uses them. Necessary source corrections are explicit and their counterexamples remain part of the completion goal. The author's 1987 corrections are applied transparently, and the addendum's additional results are recorded separately (original, errata and addenda).

Groups, analytic directions, and geometric degree

Let K be the complex field or the completed algebraic closure of the field of ℓ-adic numbers for a prime ℓ, as in the source. Let G be a product of finitely many commutative algebraic groups G₁,…,Gᵣ over K, with each factor embedded as a quasi-projective variety in a projective space. Write n for the sum of their dimensions. A point of the product embedding has one block of homogeneous coordinates for each factor.

A nonzero multihomogeneous polynomial P has a degree Dᵢ in its i-th block of coordinates. Its zeros define a hypersurface of the ambient product of projective spaces. An analytic subgroup A is locally parametrized by an analytic homomorphism from a finite-dimensional additive K-space. The order of P along A at a group point g is the vanishing order of P after composing local projective coordinates with the translated parametrization. This definition must be independent of the choice of nonzero local coordinate representatives.

Let Σ be a finite set of group points containing the identity. Its n-fold sumset Σ(n) consists of all sums of n, not necessarily distinct, elements of Σ; Σ(0) is the singleton identity. For a connected algebraic subgroup H, the integer s is the analytic codimension of A∩H in A. The expression |(Σ+H)/H| counts distinct H-cosets meeting Σ. Codimension concerns the analytic tangent dimension; it does not assert that the point-set intersection is finite.

The source's Hilbert degree form ℋ(V;D₁,…,Dᵣ) is (dim V)! times the highest homogeneous part of the multigraded Hilbert–Samuel polynomial of the projective closure of V, evaluated at the degrees. It must be constructed from the coordinate ring, rather than supplied as an arbitrary numerical function. For one projective factor it is deg(V)D^(dim V). These definitions are fixed in §§2–3 of the original paper.

Formalization targets

The completion target is all results of the paper, with an aggregate goal that requires their individual formal statements. Theorem 2.1 is one milestone within that target. For each fixed family of embedded group factors, it chooses positive integers cᵢ, each depending only on its corresponding embedding. These constants precede the analytic subgroup, the finite sampling set, the polynomial degrees, the polynomial, and the contact parameter T. If P has order at least nT+1 along A at every point of Σ(n), there is a connected algebraic subgroup H with

$$\binom{T+s}{s}\, |(\Sigma+H)/H|\, \mathcal H(H;D_1,\ldots,D_r) \leq \mathcal H(G;c_1D_1,\ldots,c_rD_r).$$

The same H is contained in a translate of the zero locus of P on G and is incompletely defined by equations of multidegrees at most (c₁D₁,…,cᵣDᵣ): it is an irreducible component of the common zero locus in G of equations with those degree bounds. Both geometric conclusions are part of the target. A formalization retaining only the displayed numerical inequality would omit part of the original result.

The 1986 paper has 13 numbered results. Section 2 contains Theorem 2.1 and Corollaries 2.2–2.3, including the one-dimensional analytic result and the result for disjoint group factors. Section 3 contains Lemmas 3.1–3.2, Proposition 3.3 and Lemma 3.4. Section 4 contains Propositions 4.3–4.4, Lemmas 4.5–4.6 and Proposition 4.7. Section 5 contains Lemma 5.1. Every clause of these statements belongs to the mission.

Definitions 3.5, 4.1 and 4.2, the unnumbered setup, the internal Facts A–E, the counterexample after Proposition 3.3, and the mathematical claims in remarks also require coverage. Source numbers and page references identify the correspondence between the prose and Lean declarations. The 1987 addendum adds vanishing on every sampled translate of the subgroup and a converse polynomial construction; both are tracked with their own hypotheses and constants.

Eight milestones and the completion goal

The completion goal is PhilipponMultiplicity.paper_results, a conjunction of 26 concrete propositions. This is a collection goal requiring the source statements and the additional mathematical claims in the coverage record. It is separate from the paper's original Theorem 2.1, which remains individually named and reusable.

The mission has eight milestones; four are currently Proved:

Source	Milestone	Status
Theorem 2.1	General multiplicity estimate, with every geometric and numerical conclusion.	Proved
Corollary 2.2	One-dimensional analytic-subgroup consequence.	Open
Corollary 2.3	Consequence for disjoint group factors and sampling grids.	Open
Proposition 3.3	Multigraded intersection bounds, including the multiplicity-sensitive bound.	Proved
Proposition 4.7	Binomial lower bound for contact multiplicity.	Proved
Lemma 5.1	Stabilizer construction and the geometric counting estimate.	Proved
1987 addendum, p. 398	Strengthened vanishing on every sampled subgroup translate.	Open
1987 addendum, p. 398	Converse polynomial construction.	Open

The full statement package has 27 compiled theorem statements: all thirteen numbered results, both addenda, eleven supporting or correction targets, and the aggregate goal. Fourteen admission-free definition bundles supply their actual geometric and algebraic objects. All 41 original statement and definition items have independent blind readbacks. The eight milestones above retain their existing identities.

The supporting clauses include Hilbert-polynomial existence, primary components and Facts A–E; the geometric interpretation of mixed degree; the actual counterexample after Proposition 3.3; translation operators and their comparison with intrinsic ideals; contact invariance; translation-invariance and embedding remarks; the component/stabilizer construction; counting estimates; and the exact Masser–Wüstholz Theorem I consequence claimed on p.361. Proof-internal recursive ideals and tangent/exponential arguments belong to their corresponding theorem proofs.

Source corrections are visible for review. Lemma 3.1 and Corollary 2.2 require positive equation degrees; explicit zero-degree counterexamples are required goal clauses. Both addenda require positive ambient dimension; the goal also requires their dimension-zero counterexamples. The three-generator ideal printed on p.370 is nonradical, contrary to the printed word “prime”; its valid degree-four versus length-six counterexample is preserved, together with an explicit nilpotent witness. Connectedness is stated in the translation-invariance and Lange reembedding remarks. These are mathematical corrections documented during the source comparison, beyond the author's 1987 errata. They are not silent changes to the source.

Fourteen individual targets now have checked proofs with no Open theorem inputs. The remaining twelve individual targets and the collection goal are Open. The existing proved local-algebra references remain reusable ingredients.

What a completed formalization enables

The output is a reusable development of the paper's multigraded commutative algebra, translation and differential operators, geometric multiplicity theory, and zero estimates. All source results are required for completion. A downstream Weierstrass application can consume a specialization of Theorem 2.1; its needs do not determine the scope or completion of this mission (example application).

These are established mathematical results whose proofs are being formalized. The complete original Theorem 2.1 has an accepted proof. The selected Weierstrass application uses individually named Philippon results, with its application-specific model and subgroup bridges proved in the Senthil mission. The remaining general results stay required even though that application is complete.

The foundational difficulty

Vanishing conditions need not be independent: many can occur on the same component or on translates with a nontrivial stabilizer. Counting coefficients of P therefore does not bound their total multiplicity. The development needs geometric degree for actual components, multiplicities measured by lengths of localized quotient rings, and uniform control of translations in fixed projective embeddings.

Proposition 3.3 supplies multigraded intersection bounds, Proposition 4.7 controls contact multiplicity, and Lemma 5.1 connects the stabilizer to the geometric counting estimate. These three results and Theorem 2.1 now have checked proofs. The remaining corollaries, general geometric and analytic claims, examples and addenda are independent deliverables. Application-specific contact results do not discharge the remaining general statements.

Formalization scope

The declarations use the namespace PhilipponMultiplicity. Source statements retain their conclusions, constants, quantifier order, and complex or ℓ-adic scope, with the visible boundary and wording corrections listed above. Intermediate specializations are labelled as such and do not discharge a more general source result. Natural-number and zero-degree conventions have been compared with the original scans; the discovered failures and corrected hypotheses are recorded explicitly for human review. Corrections and inferred conventions must be documented rather than silently changing the source.

The required definitions include embedded commutative algebraic groups and their connected subgroups; products of projective spaces and multihomogeneous coordinate rings; analytic local homomorphisms and intrinsic contact order; multigraded Hilbert polynomials and their degree forms; local component lengths; and finite coset counts. No model may assume the desired multiplicity inequality, hide it as a structure field, or replace geometric degree by an unconstrained function.

All 27 theorem statements and 14 definition bundles compile in Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Source comparisons and independent readbacks document the fixed statements and their explicit corrections. The goal remains the concrete 26-part full-paper collection. The completed proofs supply reusable Hilbert theory, primary-component multiplicities, polynomial differential operators, bounded translation atlases and the Section 5 construction. Contributions to the remaining targets, including results unused by Senthil, complete the original scope.

Selected references

• P. Philippon, Lemmes de zéros dans les groupes algébriques commutatifs, Bulletin de la Société Mathématique de France 114 (1986), 355–383. DOI and original paper.
• P. Philippon, Errata et addenda à « Lemmes de zéros dans les groupes algébriques commutatifs », Bulletin de la Société Mathématique de France 115 (1987), 397–398. DOI and addendum.
• Senthil Kumar K, Algebraic independence of values of Weierstrass elliptic and zeta functions, Proceedings of the Edinburgh Mathematical Society (2026), including Robert Tubbs's appendix. DOI.

Motivation

Rings of arithmetic power series — power series with integer coefficients that converge on a disc of radius close to $1$ — sit between algebra and analysis: an element has both archimedean zeros, in the complex disc, and non-archimedean ones, at $p$-adic points. Harbater (Convergent arithmetic power series, Amer. J. Math. 106 (1984), 801–846, DOI 10.2307/2374325) showed that a well-chosen ring of such series is a principal ideal domain and identified its prime ideals; the same ring is the arithmetic model of the closed disc of radius $r$ in the adic space $\mathrm{Spa}(\mathbb{Z}[[T]])$.

The result was put to work in Clausen–Scholze's Lectures on Analytic Geometry (Lecture VII), where $\mathbb{Z}((T))_{>r}$ supplies a two-term presentation of the real numbers as a condensed abelian group: for $0 < r' < r < 1$ there is an exact sequence $0 \to \mathbb{Z}((T))_r \xrightarrow{f_{r'}} \mathbb{Z}((T))_r \to \mathbb{R} \to 0$, whose existence rests on the principality of the kernel of evaluation at $r'$. The quantitative refinement of that sequence (Propositions 7.2 and 7.3 of the notes) is what produces the $\ell^p$-norms in the analytic ring structure on $\mathbb{R}$.

Setting

Fix a real number $r$ with $0 < r < 1$. An integral Laurent series is a family of integers $(a_n)_{n \in \mathbb{Z}}$ whose support is bounded below, written $f = \sum_{n \gg -\infty} a_n T^n$; these form the ring $\mathbb{Z}((T))$ under coefficientwise addition and the Cauchy product.

Define

$$\mathbb{Z}((T))_{>r} \;=\; \Big\{\, \sum_{n \gg -\infty} a_n T^n \;\Big|\; \exists\, s > r,\ |a_n|\, s^{\,n} \xrightarrow[n \to \infty]{} 0 \,\Big\} \;\subseteq\; \mathbb{Z}((T)).$$

Concretely, $f$ lies in $\mathbb{Z}((T))_{>r}$ when the associated Laurent expansion converges on some punctured disc $\{0 < |y| < s\}$ with $s > r$ strictly larger than $r$ — an overconvergence condition. For $x$ a real or complex number, $f(x) = \sum_{n} a_n x^{\,n}$ denotes the evaluation, whenever the family is summable.

Two features distinguish this ring from the classical Tate algebra. The coefficients are integers, not elements of a complete field, so reduction modulo a prime $p$ is available and produces $\mathbb{F}_p((T))$. And the condition is an overconvergence condition: the radius $s$ is required to be strictly larger than $r$, which is what makes the ring behave like the ring of functions on a closed disc rather than an open one.

Formalization targets

Goal

$$0 < r < 1 \;\Longrightarrow\; \mathbb{Z}((T))_{>r} \text{ is a principal ideal domain.}$$

The ring is a subring of the domain $\mathbb{Z}((T))$, so integrality is automatic and the content of the goal is that every ideal is generated by one element.

The prime ideals (context, not a formalization target here)

Theorem 7.1 of the source also classifies the nonzero primes: kernels of evaluation at a complex $x$ with $0 < |x| \le r$ (up to conjugation); the ideals $(p)$ for $p$ prime; and kernels of evaluation at a topologically nilpotent unit $x$ of a finite extension of $\mathbb{Q}_p$ (up to Galois conjugacy). The milestones below formalize the parts of the classification that the principality proof actually consumes — surjectivity of the three evaluation maps, and principality of the archimedean kernels — and leave the full classification statement for a later mission in this series.

Significance

The result itself. Principality gives, for each point of the closed disc, a single equation cutting it out; that is exactly what the presentation $0 \to \mathbb{Z}((T))_r \to \mathbb{Z}((T))_r \to \mathbb{R} \to 0$ needs. Downstream, that presentation is the input to the computation of measures on $\mathbb{R}$ in the analytic-ring formalism, and the reason $\ell^p$-spaces with $p < 1$ appear there at all. Without it, one has no finite free resolution of $\mathbb{R}$ by rings of arithmetic functions, and the structure results of Lectures VI–VII of the source lose their computational base.

Formalizing it. The mathematics is classical and fully proved; nothing here is open. What is missing is a machine-checked version. Mathlib has Hahn series, Laurent series, complex analysis on discs, and the $p$-adic numbers, but nothing about arithmetic overconvergent series: not the ring itself, not the greedy expansions that make real evaluation surjective, not the invertibility criterion. Each milestone below is a self-contained piece of that missing theory, reusable outside this mission.

Difficulty

The obvious approach — Weierstrass preparation, as for the Tate algebra $K\langle T\rangle$ over a complete field $K$ — does not apply: the coefficient ring $\mathbb{Z}$ is not a field, and no single valuation controls it. An element of $\mathbb{Z}((T))_{>r}$ must be divided simultaneously by archimedean generators (complex zeros in the disc) and $p$-adic ones, with the quotient required to stay integral and still overconvergent. Two steps carry the weight and fail for naive reasons:

• Producing an integral generator for the kernel of evaluation at a real or complex $x$: one first needs a real polynomial $g \in 1 + T^n\mathbb{R}[T]$ with $x$ as its only zero in $\{0 < |y| \le r\}$, then a correction series $h$ with small coefficients such that $gh$ has integer coefficients. Neither factor alone is integral.
• Showing that an element of $1 + T\mathbb{Z}[[T]]$ with no zero in the closed disc of radius $r$ is invertible in the ring: the inverse is integral for formal reasons, but its overconvergence is an analytic statement about the absence of zeros.

Finiteness — that a nonzero element lies in only finitely many of the listed maximal ideals — mixes the identity theorem for holomorphic functions with a $p$-adic Weierstrass argument, which is why the reduction and $p$-adic surjectivity milestones are prerequisites rather than side remarks.

Formalization scope

The ambient ring is Mathlib's LaurentSeries ℤ (Hahn series over $\mathbb{Z}$ indexed by $\mathbb{Z}$), and $\mathbb{Z}((T))_{>r}$ is given as a set of such series, cut out by the decay condition $|a_n| s^{\,n} \to 0$ as $n \to +\infty$ for some $s > r$. Evaluations are unordered sums over $\mathbb{Z}$; where a statement asserts a value of an evaluation, summability is asserted alongside it, so the junk value of a divergent sum cannot be exploited.

Because the carrier is a set, the goal theorem is stated for an arbitrary subring of $\mathbb{Z}((T))$ whose underlying set is $\mathbb{Z}((T))_{>r}$. That form would be vacuous if no such subring existed, which is precisely why the first milestone asserts its existence; the two together carry the intended content, and the mission is not considered advanced by the goal alone.

Milestone 6 formalizes only the case $K = \mathbb{Q}_p$ of part (3) of the source theorem (topologically nilpotent units of proper finite extensions of $\mathbb{Q}_p$ are out of scope, since Mathlib lacks the ambient theory of such extensions). Milestone 3 drops the "with multiplicity one" clause of the source and asserts only that the zero set in the punctured closed disc is $\{x\}$.

A complete development will need: closure of the decay condition under the Cauchy product; summability of evaluations on the closed disc; the identity theorem for the induced holomorphic functions; greedy $x$-adic expansions of real numbers with bounded integer digits; and $p$-adic expansions in the lattice generated by a topologically nilpotent unit. Contributions of any of these, as standalone lemmas, are welcome.

Selected references

• D. Harbater, Convergent arithmetic power series, American Journal of Mathematics 106 (1984), 801–846. DOI 10.2307/2374325
• P. Scholze (joint with D. Clausen), Lectures on Analytic Geometry, Bonn, 2019/20; Lecture VII, Theorem 7.1. PDF
• P. Scholze (joint with D. Clausen), Lectures on Condensed Mathematics, Bonn, 2019. PDF

Motivation

Almost every classical transcendence theorem is a statement about the interaction between the additive structure of $\mathbb{C}$ and the exponential function. Hermite proved in 1873 that $e$ is transcendental, Lindemann in 1882 that $e^{\alpha}$ is transcendental for every nonzero algebraic $\alpha$ — hence that $\pi$ is transcendental and the circle cannot be squared — and Weierstrass in 1885 extended this to the linear independence of $e^{\alpha_1},\dots,e^{\alpha_n}$ over $\overline{\mathbb{Q}}$ for distinct algebraic $\alpha_i$. Gelfond and Schneider settled Hilbert's seventh problem in 1934, and Baker's 1966 theorem on linear forms in logarithms made the subject effective.

Schanuel's conjecture, formulated by Stephen Schanuel in the 1960s and first published by Lang (Introduction to Transcendental Numbers, Addison–Wesley, 1966, Chapter III), is a single statement that contains all of these as special cases, together with a large number of statements that remain open — for instance that $e$ and $\pi$ are algebraically independent, or that $e + \pi$ is irrational. No case of it is known beyond those already covered by the Lindemann–Weierstrass theorem or by Baker's theorem.

Timeline, with the hypotheses each result actually assumes:

• 1882, Lindemann: $e^{\alpha}$ is transcendental for algebraic $\alpha \neq 0$.
• 1885, Weierstrass: for pairwise distinct algebraic $\alpha_1,\dots,\alpha_n$, the values $e^{\alpha_1},\dots,e^{\alpha_n}$ are linearly independent over $\overline{\mathbb{Q}}$.
• 1934, Gelfond and Schneider, independently: if $\lambda \neq 0$ is a logarithm of an algebraic number and $\beta$ is algebraic and irrational, then $e^{\beta\lambda}$ is transcendental.
• 1960s, Siegel, Lang and Ramachandra: the six exponentials theorem, unconditional; the analogous four exponentials statement is still open.
• 1966, Baker: if logarithms $\lambda_1,\dots,\lambda_n$ of algebraic numbers are linearly independent over $\mathbb{Q}$, then $1,\lambda_1,\dots,\lambda_n$ are linearly independent over $\overline{\mathbb{Q}}$.
• 1971, Ax: the function-field analogue of Schanuel's conjecture, for formal power series and, more generally, differential fields of characteristic zero.

Setting

Write $\exp$ for the complex exponential function. A tuple $z_1,\dots,z_n$ of complex numbers is linearly independent over $\mathbb{Q}$ when the only rationals $q_1,\dots,q_n$ with $\sum_i q_i z_i = 0$ are $q_1 = \dots = q_n = 0$; here $\mathbb{C}$ is viewed as a vector space over $\mathbb{Q}$.

For a subset $S \subseteq \mathbb{C}$, let $\mathbb{Q}(S)$ denote the subfield of $\mathbb{C}$ generated by $S$ over $\mathbb{Q}$. The transcendence degree $\operatorname{trdeg}_{\mathbb{Q}} \mathbb{Q}(S)$ is the cardinality of a transcendence basis of $\mathbb{Q}(S)$ over $\mathbb{Q}$: the largest number of elements of $\mathbb{Q}(S)$ that are algebraically independent over $\mathbb{Q}$. A number $x$ is transcendental over $\mathbb{Q}$ when no nonzero polynomial with rational coefficients vanishes at $x$, and numbers $x_1,\dots,x_m$ are algebraically independent over $\mathbb{Q}$ when no nonzero polynomial in $m$ variables with rational coefficients vanishes at $(x_1,\dots,x_m)$.

Formalization targets

Goal

$$z_1,\dots,z_n \text{ linearly independent over } \mathbb{Q} \;\Longrightarrow\; \operatorname{trdeg}_{\mathbb{Q}} \mathbb{Q}\bigl(z_1,\dots,z_n,\,e^{z_1},\dots,e^{z_n}\bigr) \;\ge\; n .$$

The goal fixes no numerical constant and no special shape for the $z_i$: it asserts only the inequality, for every $n$ and every $\mathbb{Q}$-linearly independent tuple. The case $n = 0$ is vacuous and the conclusion is a bound on a cardinal, so nothing is hidden in a degenerate convention.

Milestones

The milestone list consists of the landmark unconditional theorems that Schanuel's conjecture generalizes, the known function-field analogue, and one conditional corollary that records what the conjecture buys:

• Hermite–Lindemann (1882): $\alpha$ algebraic and nonzero $\Rightarrow$ $e^{\alpha}$ transcendental.
• Lindemann–Weierstrass (1885): $\sum_i \beta_i e^{\alpha_i} \neq 0$ for distinct algebraic $\alpha_i$ and algebraic $\beta_i$ not all zero.
• Gelfond–Schneider (1934): $\lambda \neq 0$ a logarithm of an algebraic number, $\beta$ algebraic irrational $\Rightarrow$ $e^{\beta\lambda}$ transcendental.
• Six exponentials theorem: $x_1,x_2$ and $y_1,y_2,y_3$ each $\mathbb{Q}$-linearly independent $\Rightarrow$ at least one of the six numbers $e^{x_i y_j}$ is transcendental.
• Baker (1966): $\mathbb{Q}$-linearly independent logarithms of algebraic numbers, together with $1$, are linearly independent over $\overline{\mathbb{Q}}$.
• Ax (1971), power series form: $\operatorname{trdeg}_{\mathbb{C}} \mathbb{C}(f_1,\dots,f_n,g_1,\dots,g_n) \ge n+1$ when $g_i' = f_i' g_i$, the $g_i$ are units, and no nontrivial $\mathbb{Q}$-linear combination of the $f_i$ is constant.
• Conditional corollary: Schanuel's conjecture implies that $e$ and $\pi$ are algebraically independent over $\mathbb{Q}$.

Significance

Schanuel's conjecture decides, in one stroke, a long list of questions that are individually open: the algebraic independence of $e$ and $\pi$, the irrationality of $e+\pi$ and of $e\pi$, the transcendence of $e^{e}$ and $\pi^{\pi}$, the four exponentials conjecture, and — combined with work of Macintyre and Wilkie — the decidability of the first-order theory of the real exponential field. Its restriction to algebraic $z_i$ is exactly the Lindemann–Weierstrass theorem, and its restriction to $z_i$ whose exponentials are algebraic is exactly Baker's theorem, so the conjecture is a common generalization of the two main unconditional pillars of the subject.

On the formalization side, the state of the art in Lean's mathematical library is modest relative to this history: the analytic core of the Lindemann–Weierstrass argument is present, but the Hermite–Lindemann theorem, the Lindemann–Weierstrass theorem, the transcendence of $\pi$, the Gelfond–Schneider theorem, the six exponentials theorem and Baker's theorem are not available as usable statements in the pinned environment. Each milestone here is therefore a genuine formalization project with a known mathematical proof, and none of them is a restatement of an existing library result. The goal theorem itself is open mathematically; the realistic contributions to it are reductions — implications between the goal and other statements — and closing the milestones that the conjecture generalizes.

Difficulty

The obvious approach to any single case — build an auxiliary function with many zeros, bound its derivatives, and derive a contradiction from an integrality argument — is the method behind every result on the milestone list, and it is exactly what fails for the conjecture in general. Those proofs need the exponentials, or the arguments, to be algebraic somewhere, so that heights and denominators can be controlled; for a general $\mathbb{Q}$-linearly independent tuple there is no arithmetic input at all, and no known construction produces the required auxiliary function. Ax's theorem shows that the differential-algebraic shadow of the statement is true, but its proof uses the derivation on the function field and has no arithmetic counterpart. A solver should not expect the conjecture itself to fall to a variation of the classical method.

Formalization scope

All statements are over $\mathbb{C}$, with the complex exponential. Tuples are indexed by Fin n, ℚ-linear independence is Mathlib's LinearIndependent ℚ, transcendence degree is Mathlib's Algebra.trdeg, the generated field is IntermediateField.adjoin, and the inequality is between cardinals, so the goal reads (n : Cardinal) ≤ Algebra.trdeg ℚ (adjoin ℚ (Set.range z ∪ Set.range (Complex.exp ∘ z))). Algebraicity is IsAlgebraic ℚ, transcendence is Transcendental ℚ, and algebraic independence is AlgebraicIndependent ℚ.

There is no trivializing formalization here: the hypothesis LinearIndependent ℚ z is satisfiable for every $n$, so the goal is not vacuous, and the conclusion is an inequality of cardinals rather than a statement about a definition introduced for this mission.

The Ax milestone is stated for formal power series in one variable over $\mathbb{C}$: the exponential relation is expressed as the differential equation $g_i' = f_i' g_i$ with PowerSeries.derivative, and the conclusion bounds Algebra.trdeg ℂ of the ℂ-subalgebra generated by the $f_i$ and the $g_i$. The conditional corollary takes the full statement of Schanuel's conjecture as an explicit hypothesis, so it is provable unconditionally as stated.

Infrastructure that a complete development needs, and that is reusable well beyond this mission: Siegel's lemma and height machinery for algebraic numbers, the standard auxiliary-function construction with derivative bounds, and interface lemmas relating Algebra.trdeg, AlgebraicIndependent and Transcendental. Reductions between the milestones — for example deriving Hermite–Lindemann from Lindemann–Weierstrass, or the six exponentials theorem from a general Baker-type statement — are welcome as sketches.

Selected references

• S. Lang, Introduction to Transcendental Numbers, Addison–Wesley, 1966. (Schanuel's conjecture is stated in Chapter III.)
• A. Baker, Linear forms in the logarithms of algebraic numbers I, Mathematika 13 (1966), 204–216. https://doi.org/10.1112/S0025579300003971
• J. Ax, On Schanuel's conjectures, Annals of Mathematics 93 (1971), 252–268. https://doi.org/10.2307/1970774
• A. Macintyre and A. J. Wilkie, On the decidability of the real exponential field, in Kreiseliana, A K Peters, 1996, 441–467.
• M. Waldschmidt, Diophantine Approximation on Linear Algebraic Groups, Springer, 2000.
• Wikipedia, Schanuel's conjecture. https://en.wikipedia.org/wiki/Schanuel%27s_conjecture