1. Motivation

Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The Formal Conjectures library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as importantly, stated unambiguously — by machine.

This mission ports a coherent slice of that material to Prove2Me. It is deliberately a portfolio mission: the goal theorem is the Bateman–Horn conjecture, the strongest single statement in the collection, and the milestone list gathers the other conjectures and the landmark theorems that surround them. Some milestones are genuine steps toward the goal (the Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems from other fields, grouped here because they share a source, a level of difficulty, and a need for faithful formal statements. A reader should not assume that proving a milestone advances the goal theorem. The mission's value is that every statement in it has been written against the same Mathlib revision, checked to compile, and documented well enough to be attacked.

A rough timeline of the collection's landmarks:

• 1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime.
• 1962 — Radó: the busy beaver function outgrows every computable function.
• 1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$.
• 1978 — Apéry: $\zeta(3)$ is irrational.
• 1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant subspace.
• 2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational.
• 2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture).
• 2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant.
• 2021 — Gardam: Kaplansky's unit conjecture is false (its zero-divisor and idempotent companions remain open).
• 2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$.
• 2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$.

2. Setting

The goal theorem concerns prime values of polynomials. Fix a finite set $S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the Bunyakovsky condition if its leading coefficient is positive, $\deg f\ge 1$, and $f$ is irreducible over $\mathbb{Z}$; say that $S$ satisfies the Schinzel condition if for every prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides the product at every argument.

For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some $f_i$ vanishes, let $D=\prod_i \deg f_i$, and let

$$\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.$$

The Bateman–Horn constant is the (conditionally convergent) Euler product

$$C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).$$

The other groups use their own vocabulary, each fixed in a definition item of this mission: Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$; Mills' property $\lfloor A^{3^n}\rfloor \in \mathbb{P}$; Wagstaff primes and Catalan–Mersenne numbers; polynomial self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its maximum-shifts function $\mathrm{BB}$.

3. Target

The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses, $C$ exists and is positive and

$$\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).$$

Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's conjecture: under the same hypotheses with $k=1$, $f$ takes prime values infinitely often. The remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality (New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants (Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$, Kakeya over $\mathbb{F}_q$, Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample), group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry (the two-variable Jacobian conjecture), irrationality and transcendence ($\zeta(5)$, all odd zeta values, Zudilin's theorem, $e+\pi$, $e\pi$, $\gamma$, Catalan's constant), order theory (the $1/3$–$2/3$ conjecture), and computability (Radó's theorem).

4. Significance

The results themselves. Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$, and Bunyakovsky as special cases, and it is the standard heuristic behind prime-counting predictions. The other targets are each the headline question of their area: whether every bounded Hilbert-space operator has an invariant subspace; whether group algebras of torsion-free groups are domains; whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir, Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library contributions in their own right.

Formalizing them. None of the open statements is expected to fall here; the concrete deliverable is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones, most of which are not in Mathlib today. Several are realistically in reach: the finite-field Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$ cannot both be algebraic, and Radó's diagonal argument.

5. Difficulty

For Bateman–Horn, the obstruction is visible already for $k=1$, $\deg f = 2$: sieve methods bound $\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes, but the parity problem blocks every known sieve from producing a single prime value of an irreducible quadratic. The conditional convergence of the Euler product is a second, smaller trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered infinite product changes the statement.

Each other group has its own obstruction, and they do not transfer: the parity problem says nothing about Kakeya, where the difficulty is that dimension is not stable under the natural compactness arguments, nor about the invariant subspace problem, where the known counterexamples on $\ell^1$ show that no soft argument can work.

6. Formalization scope

Conventions this mission commits to, all fixed in the definition items:

• Polynomials are elements of ℤ[X]; primality of a polynomial value is primality of its absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$.
• The Bateman–Horn constant is the limit of the ordered partial products over $p<N$, not an unordered infinite product.
• Kakeya sets carry no compactness or measurability hypothesis, matching the source; the conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$.
• Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$.
• Torsion-freeness of a group is spelled out as "every element of finite order is the identity", which is the hypothesis the source intends (it is weaker than Mathlib's IsMulTorsionFree).
• Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$, and probabilities are quotients of set cardinalities in $\mathbb{Q}$.
• The busy beaver model is an explicit $n$-state, $2$-symbol machine with a bi-infinite Boolean tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition included, and $\mathrm{BB}(0)=0$.
• Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me statements must be definite, so each such question is recorded in its affirmative form (e.g. "$e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one question with no statable answer, "what is $\mathrm{BB}(6)$?", is replaced by Radó's growth theorem rather than guessed at.
• Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions).

Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful statements from the same source library, which contains far more than fits in one mission.

7. Selected references

• P. T. Bateman and R. A. Horn, A heuristic asymptotic formula concerning the distribution of prime numbers, Math. Comp. 16 (1962), 363–367. DOI
• T. Radó, On non-computable functions, Bell System Tech. J. 41 (1962), 877–884. DOI
• R. O. Davies, Some remarks on the Kakeya problem, Math. Proc. Cambridge Philos. Soc. 69 (1971), 417–421. DOI
• C. J. Read, A solution to the invariant subspace problem on the space $\ell_1$, Bull. London Math. Soc. 17 (1985), 305–317. DOI
• K. Falconer, On the Hausdorff dimensions of distance sets, Mathematika 32 (1985), 206–212. DOI
• W. Zudilin, One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational, Russian Math. Surveys 56 (2001), 774–776. DOI
• P. Mihăilescu, Primary cyclotomic units and a proof of Catalan's conjecture, J. reine angew. Math. 572 (2004), 167–195. DOI
• Z. Dvir, On the size of Kakeya sets in finite fields, J. Amer. Math. Soc. 22 (2009), 1093–1097. DOI
• B. Bukh and T.-W. Chao, Sharp density bounds on the finite field Kakeya problem, Discrete Analysis 26 (2021). DOI
• G. Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. 194 (2021), 967–979. DOI
• K. Saito, Mills' constant is irrational, Mathematika 71 (2025), e70027. arXiv:2404.19461
• H. Wang and J. Zahl, Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions, arXiv:2502.17655
• Google DeepMind, Formal Conjectures, Apache-2.0, github.com/google-deepmind/formal-conjectures

---

Provenance note. The Lean statements in this mission are adaptations of the Formal Conjectures library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition items, and checked to compile against the platform's Mathlib revision. Each draft item carries a read-back; those read-backs are non-blind — they were written by the same agent that drafted the statements, and each says so in its first line. They are documentation, not independent testimony.

Motivation

A polynomial $f \in \mathbb{Q}[x]$ is split if $\deg f \ge 1$ and $f(x) = a\prod_{i=1}^{n}(x - r_i)$ for some $a \in \mathbb{Q}^\times$ and $r_1,\dots,r_n \in \mathbb{Q}$. Split polynomials are the simplest non-constant maps defined over $\mathbb{Q}$ that one can apply to an algebraic number: they are exactly the rational polynomials all of whose roots are rational. The question here is how much such a map can do — whether it can always push an algebraic number back down into $\mathbb{Q}$.

Say $\alpha$ is $k$-collapsible if there are split $f_1,\dots,f_k$ with $(f_k \circ \cdots \circ f_1)(\alpha) \in \mathbb{Q}$, collapsible if it is $1$-collapsible, and eventually collapsible if it is $k$-collapsible for some $k \ge 1$. Problem 3 of Griffin Macris's list of open problems asks whether every algebraic number is eventually collapsible. The two notions come apart at degree $3$: Jordi Ribes settled the cubic case of eventual collapsibility using a composition of three split polynomials, and for eventual collapsibility the open frontier is $\deg\alpha \ge 4$. For the one-step notion the picture is different — degrees $1$ and $2$ are settled, and degree $3$ is open. That one-step cubic case is this mission's goal.

Setting

Let $\alpha$ be an algebraic number with $[\mathbb{Q}(\alpha):\mathbb{Q}] = 3$. After an affine change of variable over $\mathbb{Q}$ one may assume $\alpha$ is a root of a depressed cubic

$$m(x) = x^3 + d\,x + e, \qquad d, e \in \mathbb{Q},$$

with discriminant $\Delta = \operatorname{disc}(m) = -4d^3 - 27e^2$. When $\Delta > 0$ the cubic is totally real (three real roots); when $\Delta < 0$ it has one real root and a complex-conjugate pair. In the latter case write the roots as

$$\alpha_1 = -2u, \qquad \alpha_{2,3} = u \pm iv, \qquad d = v^2 - 3u^2, \quad e = 2u(u^2 + v^2),$$

and set $\psi = \arctan(3u/v)$, the parameter that controls the archimedean obstruction below. Scaling $\alpha \mapsto w\alpha$ sends $(d,e) \mapsto (w^2 d, w^3 e)$, so the single rational invariant

$$\tau = e^2/d^3$$

determines the problem up to scaling: the search space is one rational parameter, not two.

Formalization targets

Goal — every cubic algebraic number is collapsible

$$\forall\, \alpha \in \mathbb{C}, \quad [\mathbb{Q}(\alpha):\mathbb{Q}] = 3 \ \Longrightarrow\ \exists\, f \text{ split with } f(\alpha) \in \mathbb{Q}.$$

This is the weakest statement that settles the case: it fixes no bound on $\deg f$, and asserts only that some split $f$ exists. A version with a degree bound would be strictly stronger and is not the goal, because no such bound is known — indeed the archimedean milestone below shows no uniform one can exist.

Supporting targets

The milestone list runs from the reformulation and the invariance reductions, through the known sufficient conditions, to the two obstructions and the two genuinely open sub-targets. Ordered as they are stated there:

1. the product criterion — $\alpha$ is collapsible iff $\prod_i(\alpha - r_i) \in \mathbb{Q}$ for some nonempty finite multiset of rationals, which turns collapsibility into a multiplicative relation in $K^\times/\mathbb{Q}^\times$;
2. affine invariance, and the completeness of $\tau$ as an invariant of the scaling action, which together justify the reduction to one parameter;
3. two sufficient conditions: square discriminant, and the power-family condition subsuming it;
4. three obstructions: gap parity in the totally real case; the archimedean degree bound when $\Delta < 0$; and the extension of that bound beyond cubics, to any algebraic number possessing both a real and a non-real conjugate.

The mission also carries, as a plain theorem rather than a milestone, the single open instance $x^3 + 6x + 1$ — the smallest cubic within computational reach for which no collapsing is known. It is an instance of the goal rather than a step toward it, which is why it is not on the attack path.

Significance

A proof of the goal closes the one-step cubic case and, with Ribes's composition result, would give a complete picture at degree $3$. A disproof would be at least as informative: a single cubic $\alpha$ admitting no split $f$ with $f(\alpha) \in \mathbb{Q}$ would separate $1$-collapsibility from eventual collapsibility by an explicit example, showing that composition is genuinely necessary and not an artefact of the known proof.

The supporting targets have value independent of the goal. The product criterion is the statement everything else is phrased against. The archimedean bound is the only known mechanism forcing $\deg f \to \infty$, and it is what rules out a uniform-degree approach.

Status, stated precisely. Six of the eight milestones have machine-checked Lean 4 + Mathlib proofs in the author's development, against a newer Mathlib revision than this mission's environment; restating and reproving them here is a port, not new mathematics, and they are included because the goal cannot be attacked without them. The two archimedean milestones are not proved in that form. For the cubic bound both halves exist — the convexity argument and the Möbius reduction — but the statement in terms of a collapsing polynomial has not been assembled. The extension beyond cubics has not been formalised at all; the argument is the same one, since nothing in it uses cubicness beyond the identification of a single circle parameter, but that observation is not a proof. The instance $x^3 + 6x + 1$ and the goal itself are open.

Difficulty

The obvious approach is to write down a split $f$ with rational roots and force $f(\alpha) \in \mathbb{Q}$ by solving for the roots. This works when $\Delta$ is a rational square, and more generally under the power-family condition, and produces the bulk of the known examples — but it cannot work in general, for a reason that is quantitative rather than technical.

Suppose $\Delta < 0$ and $f = a\prod_i(x - r_i)$ is split with $f(\alpha) \in \mathbb{Q}$. Irreducibility of $m$ forces $f - c$ to be divisible by $m$, hence $f(\alpha_1) = f(\alpha_2) \ne 0$, hence $\prod_i \frac{\alpha_1 - r_i}{\alpha_2 - r_i} = 1$. Each factor lies on a fixed circle through $0$ and $1$ determined by $\psi$, and a convexity argument on $\log\cos$ then forces

$$\deg f \ \ge\ \pi/\psi.$$

As $\tau \to 0^+$ one has $\psi \to 0$, so the required degree is unbounded: there is no uniform degree in which to search, and any construction must produce split polynomials of growing degree. This is the central difficulty. For $x^3 + 6x + 1$ the bound already gives $\deg f \ge 32$, which is why that cubic resists the searches that settle its neighbours.

Only one step of this argument is special to cubics: the identification of the circle parameter as $3u/v$. For an algebraic number of any degree with a real conjugate $\alpha_1$ and a non-real conjugate $\alpha_2$, irreducibility gives the same relation $\prod_i (\alpha_1 - r_i)/(\alpha_2 - r_i) = 1$, the images again lie on a circle through $0$ and $1$, and the parameter is $\lambda = (\operatorname{Re}\alpha_2 - \alpha_1)/\operatorname{Im}\alpha_2$, which specialises to $3u/v$ in the depressed-cubic case. The obstruction therefore constrains the whole conjecture, not merely its cubic case, which is why the extension is carried as a milestone in its own right.

In the totally real case ($\Delta > 0$) the archimedean argument gives nothing at all — the relevant Möbius maps are real and surject onto $\widehat{\mathbb{R}}$ — and the only known constraint is that each gap between consecutive conjugates contains an even number of roots of $f$. Whether degrees stay bounded there is itself unsettled.

Formalization scope

Representation. IsSplit f says $0 < \deg f$ and $f = C\,a \cdot \prod_{r \in rs}(X - r)$ for a nonzero rational $a$ and a multiset $rs$ of rationals; multiplicities are therefore allowed and the roots need not be distinct. Collapsible α is stated for $\alpha$ in an arbitrary field $K$ carrying a $\mathbb{Q}$-algebra structure, not only for $K = \mathbb{C}$, so the results apply verbatim to a root in $\mathbb{R}$, in $\mathbb{C}$, or in $\mathbb{Q}[x]/(m)$. The goal theorem is stated over $\mathbb{C}$, with "cubic" expressed as $\deg(\operatorname{minpoly}_{\mathbb{Q}}\alpha) = 3$.

Ruling out a trivialisation. Collapsible places no lower bound on $\deg f$ and does not require the value $c = f(\alpha)$ to be nonzero, so one must check that the goal is not satisfiable by degenerate means. It is not: $c = 0$ would make $m \mid f$, impossible for an irreducible cubic $m$ dividing a polynomial that splits over $\mathbb{Q}$. Constant $f$ is excluded by $0 < \deg f$. Nothing in the statement is vacuous — the hypotheses of the goal are satisfied by every cubic irrationality.

Conventions in the archimedean milestones. In the cubic bound the parameters $u, v$ enter as real numbers satisfying the factorisation identity, with the normalisation $0 < uv$; this is not a restriction, since $v$ is determined only up to sign and the sign may be chosen. Under it $\psi = \arctan(3u/v) \in (0, \pi/2)$, and the conclusion is $\pi/\psi \le \deg f$ with $\deg f$ the natural-number degree.

In the general bound the corresponding normalisation is $0 < (\operatorname{Re}\alpha_2 - \alpha_1)\operatorname{Im}\alpha_2$. It forces $\operatorname{Im}\alpha_2 \neq 0$, so $\alpha_2$ is genuinely non-real and $\lambda > 0$, hence $\psi \in (0,\pi/2)$ and no division-by-zero value can arise in the conclusion. Passing to the complex conjugate of $\alpha_2$ flips the sign of both factors, so the condition is a choice of conjugate rather than a restriction — except when $\operatorname{Re}\alpha_2 = \alpha_1$, which the hypothesis excludes and which cannot occur for a depressed cubic with $\Delta<0$. No degree hypothesis on $m$ is needed: possessing both a real and a non-real root already forces $\deg m \ge 3$.

Infrastructure. A complete development needs Polynomial, Multiset, minpoly, and for the archimedean bound Real.arctan, Complex.arg, and strict concavity of $\log\cos$ on $(-\pi/2, \pi/2)$. The convexity and Möbius lemmas are reusable well beyond this mission — they bound the number of factors in any product of complex numbers constrained to a circle through the origin. Contributions of any of the supporting targets are welcome independently of the goal; so is a disproof, and so is an explicit collapsing of $x^3 + 6x + 1$ of any degree.

Selected references

• Griffin Macris, List of open problems, Problem 3. https://sites.google.com/view/griffinmacris/open-problems
• Miles, Collapsible algebraic numbers, 2026. https://quesswho.github.io/miles-blog/2026/08/20/collapsible/ — source of the definitions of split, $k$-collapsible, collapsible and eventually collapsible used above, of Ribes's cubic result for eventual collapsibility, and of the statement that the degree-$3$ case of one-step collapsibility is open.

Motivation

Moment-angle complexes are central objects in toric topology. They convert the combinatorics of a simplicial complex into a topological space assembled from disks and circles, allowing face structure to influence homotopy and homology. When the simplicial complex triangulates a sphere, the resulting space is a moment-angle manifold. Torsion in the integral homology of these manifolds is difficult to realize in low simplicial dimension, and torsion in the homology of their based loop spaces is even more constrained. Yang Han and Keke Li's Theorem 1.7 asserts that dimension four is already universal: every finitely generated abelian group can occur as a subgroup of both homology theories for one and the same simplicial $4$-sphere.

This mission formalizes that headline existence statement. It is not restricted to a chosen finite list of groups or primes, and it requires a common simplicial sphere rather than permitting separate witnesses for ordinary and loop homology.

Setting

Let $L$ be an abstract simplicial complex on a finite vertex set $[m]$. Its geometric realization $|L|$ is formed from probability vectors whose supports are faces of $L$. The condition that $L$ is a simplicial $4$-sphere means that this realization is homeomorphic to the unit sphere $S^4\subset\mathbb R^5$.

For each face $\sigma\in L$, assign a copy of the closed disk $D^2$ at vertices in $\sigma$ and the boundary circle $S^1$ at vertices outside $\sigma$. The associated moment-angle complex is

$$\mathcal Z_L =\bigcup_{\sigma\in L} \prod_{i=1}^{m}Y_i(\sigma), \qquad Y_i(\sigma)= \begin{cases} D^2,&i\in\sigma,\\ S^1,&i\notin\sigma. \end{cases}$$

The all-ones point is a canonical basepoint. Write $\Omega\mathcal Z_L$ for the based loop space with the compact-open topology. For a space $X$, the mission uses total integral singular homology

$$H_*(X;\mathbb Z)=\bigoplus_{q\ge0}H_q(X;\mathbb Z)$$

as an additive abelian group. Saying that an abelian group $G$ is a subgroup means that there is an injective additive homomorphism $G\hookrightarrow H_*(X;\mathbb Z)$.

Formalization targets

Arbitrary torsion in one moment-angle manifold

For every finitely generated abelian group $G$, prove that there are an integer $m$ and a simplicial complex $L$ on Fin m such that $|L|\cong S^4$ and there are injective homomorphisms

$$G\hookrightarrow H_*(\mathcal Z_L;\mathbb Z), \qquad G\hookrightarrow H_*(\Omega\mathcal Z_L;\mathbb Z).$$

The quantifier order matters: the same $m$ and the same $L$ must support both embeddings. The target concerns additive subgroups of total graded homology; it does not require the two embeddings to land in the same degree or to preserve multiplicative structures.

Significance

The theorem gives a universality statement for moment-angle manifolds over simplicial $4$-spheres. It says that no classification by a bounded list of torsion primes or exponents can describe all such homology and loop-homology groups. Requiring both embeddings for a single $L$ connects the ordinary topology of the manifold to its based-loop topology rather than proving two unrelated existence results.

Formalizing the theorem requires reusable foundations in several areas: finite abstract simplicial complexes, geometric realization, polyhedral products, based loop spaces, integral singular homology, graded direct sums, and additive embeddings. The published article presents a human proof; this mission records its intended main theorem as an open Lean target. The definitions do not assume the existence of the required sphere or embeddings, so a solver must supply the mathematical construction and all homological consequences.

Difficulty

The assertion ranges over arbitrary finitely generated abelian groups, including free parts and prime-power torsion of unbounded exponent. A finite check of selected groups cannot establish the target. The same finite simplicial object must simultaneously control two different homology theories, one of which is applied to an infinite-dimensional function space. Standard library support is strongest for singular homology as a functor, while concrete calculations for moment-angle spaces and loop spaces require additional bridges.

There is also a substantial representation boundary between combinatorics and topology. The face data of $L$, the union of disk-circle products, the homeomorphism $|L|\cong S^4$, and the induced maps on homology must all refer to compatible spaces and basepoints. A formal solution cannot replace “simplicial sphere” by a mere Boolean flag or replace homology by an arbitrary group-valued field.

Formalization scope

Lean represents $L$ using AbstractSimplicialComplex (Fin m). Because Mathlib's structure includes singleton faces automatically, the auxiliary face predicate explicitly restores the conventional empty face where the moment-angle union needs it. The geometric realization is the standard support-restricted probability simplex, and the sphere condition is an actual homeomorphism to the Euclidean unit $4$-sphere.

The moment-angle space is a subtype of (Fin m → ℂ) defined by the literal disk/circle coordinate condition. The loop space consists of based continuous paths with matching endpoints and carries the compact-open topology inherited from Mathlib's path construction. Homology is singularHomologyFunctor with coefficients in $\mathbb Z$, and total homology is a direct sum over all natural degrees.

The statement permits the two embeddings to occupy different degrees and makes no ring-embedding claim; these choices match the source phrase “contain $G$ as a subgroup.” It rules out vacuity by requiring an actual simplicial complex, an actual sphere homeomorphism, and injective additive maps. Contributions that isolate degree-specific refinements, compute homology of standard polyhedral products, or formalize reusable loop-space equivalences are welcome, provided they reconnect to the stated root theorem.

Selected references

• Yang Han and Keke Li, Moment Angle Manifolds Corresponding to $S^4$ Whose Homology and Loop Homology May Have Arbitrary Torsion, International Mathematics Research Notices 2026(4), 1--7, 2026. DOI
• A. Bahri, M. Bendersky, F. R. Cohen, and S. Gitler, The polyhedral product functor: a method of decomposition for moment-angle complexes, arrangements and related spaces, Advances in Mathematics 225(3), 2010, 1634--1668. DOI

Motivation

Two orthonormal bases of C^d are mutually unbiased when every transition amplitude has squared modulus 1/d. At most d+1 such bases can coexist, and complete families are known in prime-power dimensions through finite-field constructions. Dimension six is the smallest famous composite case where existence of the complete seven-base family remains unknown.

This mission turns CUHK-Shenzhen AI Math Problem 16, Existence of complete sets of mutually unbiased bases, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.

Setting

Construct seven 6 by 6 unitary-column matrices whose every distinct pair has all transition amplitudes of squared modulus 1/6. The baseline milestone constructs three pairwise mutually unbiased bases, a known lower bound that tests all matrix conventions.

Significance

Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in quantum information theory, mutually unbiased bases, finite fields, Hilbert spaces. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.

Difficulty

The equations are a large coupled system of polynomial equalities over complex phases, modulo substantial gauge symmetry. Numerical near-solutions do not certify exact existence, while nonexistence would require a global obstruction beyond currently known bounds. Dimension six lacks the finite-field structure that supplies complete prime-power constructions.

Suggested attack route

Formalize standard gauge reductions: fix the first basis to the identity and dephase transition Hadamard matrices. Verify a three-basis tensor-product construction. Then encode additional bases through complex Hadamard matrices and study algebraic constraints, Gröbner-style eliminations, semidefinite bounds, or exact certificates. Computational searches may guide conjectures, but uploaded proofs must convert numerical evidence to exact algebraic identities or certified inequalities.

Formalization scope

The Lean target is exact: column orthonormality is U-adjoint times U equals identity, and mutual unbiasedness uses Mathlib complex norm squared. Seven bases are indexed by Fin 7. No quotient by phase, permutation, or global unitary is built into the statement, since these symmetries preserve the predicate and can be used within proofs.

The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.

Milestones

Publish an exact three-basis construction in dimension six, then formalize dephasing and obstruction lemmas for extending a partial family.

The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.

Timeline and literature status

The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.

Acceptance criteria

A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.

The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.

Formal verification policy

The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.

Selected references

• Original problem
• Durt et al., review of MUBs

Motivation

Galois theory attaches to every finite Galois extension $L/K$ a finite group $\mathrm{Gal}(L/K)$, the group of field automorphisms of $L$ fixing $K$ pointwise, and the fundamental theorem of Galois theory turns the subfield structure of $L/K$ into the subgroup structure of that group. The inverse Galois problem asks whether this correspondence is surjective over the rationals: given an arbitrary finite group $G$, is there a Galois extension $L/\mathbb{Q}$ with $\mathrm{Gal}(L/\mathbb{Q}) \cong G$? The question was posed in the early nineteenth century and is unsolved.

What makes it a live research question rather than a curiosity is that the known positive results come from genuinely different sources, and none of them covers all finite groups.

• Cyclic and, more generally, finite abelian groups are realizable over $\mathbb{Q}$ by an explicit cyclotomic construction resting on Dirichlet's theorem on primes in arithmetic progressions.
• Symmetric and alternating groups are realizable over $\mathbb{Q}$; this is due to Hilbert, who realized them first over the rational function field $\mathbb{Q}(t)$ and then specialized $t$ using his irreducibility theorem.
• Every finite solvable group is realizable over $\mathbb{Q}$; this is Shafarevich's theorem (I. R. Shafarevich, The imbedding problem for splitting extensions, Dokl. Akad. Nauk SSSR 120 (1958), 1217–1219), obtained by solving embedding problems.
• Over $\mathbb{C}(t)$ — and over $K(t)$ for any algebraically closed $K$ of characteristic zero — every finite group is realizable, by the Riemann existence theorem. The obstruction to the goal is not the group theory; it is descending the field of constants to $\mathbb{Q}$.
• Case-by-case work covers large finite lists: all transitive permutation groups of degree at most $23$, and every sporadic simple group, are known to be realizable over $\mathbb{Q}$.

Setting

Fix a field $K$ and a group $G$. A Galois realization of $G$ over $K$ is a field $L$ equipped with a $K$-algebra structure such that the extension $L/K$ is Galois — normal and separable — together with a group isomorphism

$$G \;\cong\; \mathrm{Gal}(L/K),$$

where $\mathrm{Gal}(L/K)$ denotes the group of $K$-algebra automorphisms of $L$ under composition. The group $G$ is realizable over $K$, written IsRealizable K G, when at least one Galois realization of $G$ over $K$ exists. No finiteness of $L/K$ is imposed in the definition; it is automatic once $G$ is finite, because an infinite Galois extension has infinite automorphism group.

Two base fields beyond $\mathbb{Q}$ appear throughout. $K(t)$ denotes the field of rational functions in one variable over $K$, written RatFunc K; and for the statement that a group is realizable over some number field, the base field ranges over the intermediate fields of $\mathbb{C}/\mathbb{Q}$.

Formalization targets

Goal — the inverse Galois problem

$$\text{for every finite group } G, \qquad \exists\, L/\mathbb{Q} \text{ Galois with } \mathrm{Gal}(L/\mathbb{Q}) \cong G.$$

The goal fixes no degree, no polynomial and no construction: it asserts only the shape of the truth, so no later refinement of the known constructions can invalidate it.

Milestones — the known partial results

$$G \text{ cyclic} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}, \qquad G \text{ abelian} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q},$$ $$\mathrm{Sym}(S),\; A_n \text{ realizable over } \mathbb{Q}, \qquad G \text{ solvable} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q},$$ $$\exists\, K,\ \mathbb{Q} \subseteq K \subseteq \mathbb{C},\ G \text{ realizable over } K,$$ $$G \text{ realizable over } \mathbb{C}(t), \qquad G \text{ realizable over } K(t) \ (K \text{ algebraically closed, char } 0),$$ $$G \text{ realizable over } \mathbb{Q}(t) \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}.$$

The last milestone is the Hilbert-irreducibility descent step; together with the geometric milestones it makes precise which half of the classical programme is missing.

Significance

The result itself would settle a two-century-old question and, with it, the surjectivity of the Galois correspondence over $\mathbb{Q}$: every abstract finite group would be known to arise from an explicit arithmetic object, a polynomial with rational coefficients. Its absence is felt in practice — constructing a single new Galois group over $\mathbb{Q}$ is publishable work, as the recent additions of the degree-$17$ group $17T7$ (van Bommel–Costa–Elkies–Keller–Schiavone–Voight, 2024) and of the Mathieu group $M_{23}$ show.

Formalizing it produces something available today independently of the goal: a machine-checked library of the known realizability results. Mathlib has the fundamental theorem of Galois theory, cyclotomic extensions, the Kronecker–Weber theorem, solvability of groups and symmetric/alternating group theory, but it does not have a predicate for "$G$ is a Galois group over $K$", nor any of the milestones above. Every milestone here is a proved theorem of classical number theory and an unformalized one; the cyclic and abelian cases are within reach of current Mathlib, while the Shafarevich and Riemann-existence milestones are substantial formalization projects in their own right.

Difficulty

The obvious strategy fails at a well-understood point. Over $\mathbb{C}(t)$ the problem is solved: by the Riemann existence theorem every finite group occurs as the deck-transformation group of a branched cover of the projective line. Hilbert's irreducibility theorem then descends realizability from $\mathbb{Q}(t)$ to $\mathbb{Q}$. What is missing is the step in between: producing the cover over $\mathbb{Q}$ rather than over $\mathbb{C}$, i.e. showing that the geometric solution can be chosen with rational field of constants. The rigidity method makes this work for many groups, but there is no known argument covering all of them; an approach that only produces realizability over some number field is not enough, and that weaker statement is included as a milestone precisely to mark the line.

A second, purely formal difficulty: the milestones are classical but their published proofs are long. Shafarevich's theorem rests on a delicate analysis of embedding problems, and the Riemann existence theorem is analytic input that Mathlib does not currently have in the required form.

Formalization scope

The mission fixes one definition file, published first, carrying the structure GaloisRealization and the one-field class IsRealizable. Conventions it commits to:

• IsGalois K L is Mathlib's Galois condition (normal and separable); finiteness of the extension is not assumed.
• The isomorphism is with the full automorphism group $L \simeq_{\mathrm{alg}[K]} L$, not with a quotient or a subgroup of it.
• The carrier $L$ of a realization is required to live in the same universe as $K$. This costs no generality for the statements of the mission — for finite $G$ a realization is a finite extension of $K$ — and keeps every statement universe-monomorphic.
• $\mathrm{Sym}(S)$ is Equiv.Perm S for a finite type $S$, and $A_n$ is alternatingGroup (Fin n); degenerate small cases are included rather than excluded.
• Solvability is Group.IsSolvable.

The statements cannot be satisfied vacuously: IsRealizable K G asserts the existence of data, so a solver must exhibit an extension; and the hypotheses of the milestones (cyclic, abelian, solvable, or none at all) are all satisfiable, so no milestone is empty. The one conditional milestone, Hilbert descent, is stated with realizability over $\mathbb{Q}(t)$ as an explicit hypothesis.

Infrastructure a complete development needs, most of it reusable well beyond this mission: transport of a Galois realization along an isomorphism of groups and along an isomorphism of base fields; the fixed-field construction and the fundamental theorem in the form "$\mathrm{Gal}(L/L^H) \cong H$"; Galois groups of cyclotomic fields; Dirichlet's theorem on primes in arithmetic progressions (already in Mathlib); Hilbert's irreducibility theorem (not in Mathlib). Contributions of any of these as reusable platform definitions or lemmas are welcome, as are decompositions of the harder milestones into sketches.

Selected references

• Inverse Galois problem, Wikipedia. https://en.wikipedia.org/wiki/Inverse_Galois_problem
• I. R. Shafarevich, The imbedding problem for splitting extensions, Dokl. Akad. Nauk SSSR 120 (1958), 1217–1219.
• C. U. Jensen, A. Ledet, N. Yui, Generic Polynomials: Constructive Aspects of the Inverse Galois Problem, MSRI Publications 45, Cambridge University Press, 2002. http://library.msri.org/books/Book45/files/book45.pdf
• G. Malle, B. H. Matzat, Inverse Galois Theory, Springer Monographs in Mathematics, 1999.
• R. van Bommel, E. Costa, N. D. Elkies, T. Keller, S. Schiavone, J. Voight, 17T7 is a Galois group over the rationals, arXiv:2411.07857, 2024. https://arxiv.org/abs/2411.07857

Motivation

An equation for a magma constrains a binary operation without assuming that it is associative, commutative, or has an identity. Determining which equations force other equations separates the consequences of a single law from familiar properties that require additional assumptions. Restricting the underlying set to be finite can change the answer: a structural argument may depend on the fact that a surjective self-map of a finite set is injective.

The Equational Theories Project studies these implications systematically. Its December 2025 paper reports the finite implication from E677 to E255 as unresolved, while reporting a counterexample to the implication when infinite magmas are allowed. The paper also tentatively conjectures that a finite counterexample exists. This mission makes the affirmative implication its formal target and also accepts a rigorous refutation of the complete finite statement.

This mission treats the universal target as open. Supporting structural facts and conditional reductions are separately identified, so that progress on one does not assert completion of the target.

Setting

A magma here is a type $A$ with a total binary operation $\diamond:A\times A\to A$. Parentheses specify the order of evaluation throughout; no reassociation is permitted. The condition E677 means

$$\forall x,y\in A,\quad x=y\diamond\bigl(x\diamond((y\diamond x)\diamond y)\bigr).$$

The condition E255 means

$$\forall x\in A,\quad x=((x\diamond x)\diamond x)\diamond x.$$

These are the two laws used in Chapter 13 of the project blueprint. For a fixed element $y$, the left multiplication map is $L_y(x)=y\diamond x$. A fixer for $x$ is an element $y$ satisfying $y\diamond x=x$. This definition concerns one element $x$; it does not require $y$ to act as an identity on every element.

Formalization targets

The supporting targets expose the relevant distinction between a constraint on a possible fixer and the existence of a fixer. For every finite $A$ satisfying E677, the first supporting statement is

$$\forall y\in A,\quad L_y\text{ is bijective}.$$

The second supporting statement specifies any fixer:

$$\forall x,y\in A,\quad y\diamond x=x\ \Longrightarrow\ y=(x\diamond x)\diamond x.$$

The third supporting statement is the backward recurrence

$$\forall x,y\in A,\quad x=(y\diamond x)\diamond\bigl((y\diamond(y\diamond x))\diamond y\bigr).$$

These supporting statements come from ETP blueprint Lemma 13.1(i)–(iii); local direct proof files accompany their statements. The following universal fixer-existence assertion is retained as an explicit equivalent reformulation:

$$\forall x\in A,\quad\exists y\in A,\quad y\diamond x=x.$$

The mission goal is

$$\forall\text{ finite magmas }A,\quad \operatorname{E677}(A)\ \Longrightarrow\ \operatorname{E255}(A).$$

For finite E677 magmas, fixer existence is equivalent to E255: E255 supplies the fixer $(x\diamond x)\diamond x$, and Lemma 13.1(ii) converts any fixer into E255. Thus it is not presented as a strictly weaker milestone.

The active open milestone is an orbit-local producer statement. For a fixed $x$, if two elements in the forward orbit $x,L_x(x),L_x^2(x),\ldots$ have equal right products by $x$, they must be equal unless $x$ has a fixer. This isolates a genuine structural step without asserting a fixer for every element. None of the displayed statements restricts the cardinality to a tested range.

Significance

A resolution determines whether this particular law gains E255 as a consequence upon restriction to finite carriers. An affirmative proof must cover every finite cardinality, every operation on each carrier, and every assignment of the universally quantified elements. A finite counterexample must supply an operation that satisfies every instance of E677 while failing E255 at some element.

The formal package provides small, reusable statements of the two laws, the left multiplication property, and the fixer constraint. Keeping these statements separate allows their precise hypotheses and conclusions to be checked individually. In particular, the second supporting result says what a fixer must be when one exists; the fixer-existence formulation records the additional mathematical content needed to ensure existence.

Difficulty

The left multiplication conclusion concerns maps with the left input fixed. The fixer-existence formulation instead asks about the image of the map $y\mapsto y\diamond x$, with its right input fixed. No assumption in the formal goal makes these two maps interchangeable. Bijectivity of every left multiplication map alone does not state that a fixer exists.

Likewise, checking a collection of finite operation tables does not quantify over arbitrary finite cardinalities. Such computation does not discharge the goal submitted here. Any proof must justify every use of finiteness and retain the displayed parenthesization of the laws.

Formalization scope

The representation uses an arbitrary universe-polymorphic type, an explicit binary operation, and a Fintype instance for finite targets. Passing the operation explicitly avoids importing a separate magma package or imposing algebraic typeclass laws. The predicates E677 and E255 themselves do not assume finiteness; each theorem states its own finite-carrier hypothesis.

Empty carriers are included. Both laws hold vacuously on them; the pointwise fixer statement is also vacuous because there is no element $x$. Consequently an empty carrier cannot refute the main goal. Nonempty carriers of every finite size are included without further assumptions. There is no associativity, commutativity, idempotence, identity element, or cancellation hypothesis hidden in the representation.

Selected references

• Matthew Bolan et al., The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale, arXiv:2512.07087v2 (December 16, 2025), paper.
• The Equational Theories Project contributors, Equational Theories, online proof blueprint, Chapter 13, equations (1)–(2) and Lemmas 13.1–13.2, chapter, accessed September 7, 2026.

Motivation

The mean value problem, also called Smale's mean value conjecture, was posed by Stephen Smale in 1981 in his study of the complexity of root-finding algorithms for polynomials (Smale 1981). For a real differentiable function the mean value theorem produces, between two points, a point where the derivative equals a difference quotient. For a complex polynomial no such point need exist on a segment, and Smale asked for a substitute in which the special point is a critical point of the polynomial (a zero of its derivative). Estimates of this kind control how far Newton-type iterations can move, which is where Smale's original interest came from. The problem appears in lists of unsolved problems in mathematics, including Smale's own list of problems for the next century.

Timeline

• 1981 — Smale poses the problem and proves the inequality below with constant $K = 4$ (Smale 1981). The example $P(z) = z^d - dz$ shows that the constant cannot be smaller than $\frac{d-1}{d}$ in degree $d$, so no constant below $1$ works in all degrees.
• 1989 — Tischler proves the inequality with the optimal constant $K = \frac{d-1}{d}$ when all roots of $P$ are real, and when all roots of $P$ have the same absolute value (Tischler 1989).
• 2007 — Conte, Fujikawa and Lakic prove $K \le 4\frac{d-1}{d+1}$ (Conte–Fujikawa–Lakic 2007). Crane proves $K < 4 - \frac{2.263}{\sqrt d}$ for $d \ge 8$ (Crane 2007).
• 2009 — Dubinin and Sugawa prove the reverse (dual) inequality with constant $\frac{1}{d\,4^d}$ (Dubinin–Sugawa 2009); optimizing this lower bound is the dual mean value problem (Ng–Zhang 2016).

No absolute constant $K < 4$ is known that works in every degree.

Setting

Let $P$ be a polynomial with complex coefficients of degree $d \ge 2$, and write $P'$ for its derivative. A critical point of $P$ is a complex number $c$ with $P'(c) = 0$; since $d \ge 2$, $P'$ is a nonconstant polynomial of degree $d-1$, so $P$ has at least one and at most $d-1$ distinct critical points. Fix a complex number $z$ that is not a critical point, $P'(z) \ne 0$. For every critical point $c$ we then have $c \ne z$, and the difference quotient

$$\frac{P(z) - P(c)}{z - c}$$

is well defined. The question is how small this quotient can be made, relative to $|P'(z)|$, by choosing the critical point $c$ well.

Formalization targets

Goal: Smale's mean value conjecture ($K = 1$)

For every complex polynomial $P$ of degree $d \ge 2$ and every $z \in \mathbb C$ with $P'(z) \ne 0$ there is a critical point $c$ of $P$ with

$$\left| \frac{P(z) - P(c)}{z - c} \right| \le |P'(z)|.$$

Stronger: the optimal constant

The same with $|P'(z)|$ replaced by $\frac{d-1}{d}\,|P'(z)|$; the example $z^d - dz$ shows this constant cannot be lowered.

Known results (milestones)

1. Smale's inequality with $K = 4$.
2. The extremal example $P(z) = z^d - dz$ at $z = 0$, where every critical point gives exactly $\frac{d-1}{d}|P'(0)|$, and its consequence that no constant $K < 1$ works in all degrees.
3. Tischler's optimal inequality for polynomials with only real roots, and for polynomials whose roots all have the same absolute value.
4. The Conte–Fujikawa–Lakic bound $K \le 4\frac{d-1}{d+1}$.
5. Crane's bound $K < 4 - \frac{2.263}{\sqrt d}$ for $d \ge 8$.
6. The Dubinin–Sugawa dual inequality $\left|\frac{P(z)-P(c)}{z-c}\right| \ge \frac{|P'(z)|}{d\,4^d}$ for some critical point $c$.

Significance

The result itself. A positive answer gives a sharp, degree-independent mean value inequality for complex polynomials: for every non-critical point, some critical value is reachable along a chord whose slope is at most the local derivative. Bounds of this type feed into the analysis of Newton's method and of path-following root finders, and into the study of how critical values of a polynomial are distributed relative to its values. The conjecture is part of a family of open extremal problems on the geometry of critical points, alongside Sendov's conjecture.

Formalizing it. The goal and the optimal-constant form are open. The milestones are published theorems, none of which is known to have a machine-checked proof. Formalizing Smale's $K = 4$ bound and Tischler's special cases would put the classical tools of the subject (critical points of polynomials, univalent function estimates, root location) on a formal footing that later attempts can reuse.

Difficulty

The obvious strategies control the quotient through one critical point at a time: for instance, bounding $|P(z) - P(c)|$ by integrating $P'$ along the segment from $c$ to $z$. Such estimates lose a constant factor that depends on how the critical points are spread out, and the known uniform arguments all pass through distortion theorems for univalent functions, whose constants lead to $K$ close to $4$. Reaching $K = 1$ requires using all critical points simultaneously, and no argument doing this in every degree is known. The equality case $z^d - dz$, in which every critical point is equally bad, shows that any successful argument must be sharp for polynomials with maximally symmetric critical configurations.

Formalization scope

Polynomials are elements of ℂ[X] (Mathlib's Polynomial ℂ); the degree is natDegree, the derivative is Polynomial.derivative, evaluation is Polynomial.eval, and the roots of $P$ are the multiset P.roots (counted with multiplicity). A critical point is a c : ℂ with P.derivative.eval c = 0. The absolute value is the norm ‖·‖ on ℂ, and the constants $\frac{d-1}{d}$ and $4\frac{d-1}{d+1}$ are computed in ℝ from the cast of natDegree.

Every statement assumes $P'(z) \ne 0$. This is the standard normalization and is essential in Lean: division by zero returns $0$, so without it the choice $c = z$ would make the inequality trivially true whenever $z$ is itself a critical point. With the hypothesis, every critical point $c$ differs from $z$ and the quotient is a genuine difference quotient.

Crane's bound is stated as the existence, for each degree $d \ge 8$, of a constant strictly below $4 - \frac{2.263}{\sqrt d}$ that works for all polynomials of degree exactly $d$; this is equivalent to the best constant in degree $d$ being strictly below that value.

A complete development needs basic facts on critical points of complex polynomials (existence, the Gauss–Lucas theorem), and, for the classical bounds, results from the theory of univalent functions such as the Koebe quarter theorem and coefficient estimates. These are reusable well beyond this mission. Contributions of any milestone, of supporting lemmas, and of partial results in fixed small degree are welcome.

Selected references

• S. Smale, The fundamental theorem of algebra and complexity theory, Bull. Amer. Math. Soc. (N.S.) 4 (1981), 1–36. https://doi.org/10.1090/S0273-0979-1981-14858-8
• D. Tischler, Critical points and values of complex polynomials, J. Complexity 5 (1989), 438–456. https://doi.org/10.1016/0885-064X(89)90019-8
• A. Conte, E. Fujikawa, N. Lakic, Smale's mean value conjecture and the coefficients of univalent functions, Proc. Amer. Math. Soc. 135 (2007), 3295–3300. https://doi.org/10.1090/S0002-9939-07-08861-2
• E. Crane, A bound for Smale's mean value conjecture for complex polynomials, Bull. London Math. Soc. 39 (2007), 781–791. https://doi.org/10.1112/blms/bdm063
• V. Dubinin, T. Sugawa, Dual mean value problem for complex polynomials, Proc. Japan Acad. Ser. A 85 (2009), 135–137. https://arxiv.org/abs/0906.4605
• T.-W. Ng, Y. Zhang, Smale's mean value conjecture for finite Blaschke products, J. Anal. 24 (2016), 331–345. https://arxiv.org/abs/1609.00170
• Wikipedia, Mean value problem. https://en.wikipedia.org/w/index.php?title=Mean_value_problem&oldid=1374678764

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

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