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