Motivation

An additive question about the primes asks how many of them are needed to represent every integer. Shnirelman's constant is the least $k$ such that every natural number greater than $1$ is a sum of at most $k$ primes; that such a $k$ exists at all is Shnirelman's theorem (1930). The even Goldbach conjecture would give $k = 3$, and is close to equivalent to that claim, but Goldbach is open, so every bound on $k$ has come from the circle method together with explicit numerical input.

The history is a sequence of shrinking bounds, each one effective and each one resting on a numerical verification available at the time:

• 1937. Vinogradov proves that every sufficiently large odd integer is a sum of three primes, with no effective threshold (Vinogradov's theorem).
• 1956. Borozdkin makes the threshold effective; later work reduces it, and Liu and Wang bring it to $\exp(3100)$ (Liu–Wang, 2002).
• 1995. Ramaré proves that every even natural number is a sum of at most six primes, giving Shnirelman's constant $k \le 7$ (Ramaré).
• 1995. Kaniecki obtains "at most five primes" under the Riemann hypothesis (Kaniecki).
• 2012. Tao removes the hypothesis: every odd number greater than $1$ is a sum of at most five primes, unconditionally, lowering Shnirelman's constant to $k \le 6$ (arXiv:1201.6656). This mission's goal.
• 2013. Helfgott proves the ternary Goldbach conjecture outright — every odd $n > 5$ is a sum of three primes — which supersedes the statement above (arXiv:1312.7748). Neither result is formalized.

Setting

For a real number $\theta$ write $e(\theta) = \exp(2\pi i\theta)$. The von Mangoldt function $\Lambda(n)$ equals $\log p$ when $n = p^m$ is a prime power and $0$ otherwise; it is Mathlib's ArithmeticFunction.vonMangoldt.

The paper does not work with the sharp-cutoff exponential sum $S(x,\alpha) = \sum_{n \le x} \Lambda(n)e(\alpha n)$ but with a smoothed variant. For a piecewise smooth $\eta : \mathbb{R} \to \mathbb{C}$ and a modulus $q_0$, set

The modulus $q_0$ is a technical device: taking $q_0 = 2$ restricts the sum to odd $n$ and saves a factor of two in the explicit constants. Because of that restriction it is $4\alpha$, not $\alpha$, that gets approximated by a rational $a/q$.

Two explicit cutoffs are fixed. The Lipschitz cutoff

has unit mass and is supported on $[1/4, 1]$; it is chosen because it factorises the Type II sums. The $L^2$-normalised cutoff

is supported on $[0.1,0.9]$ and symmetric, $\eta_1(1-t) = \eta_1(t)$.

Throughout, $O^*(Y)$ denotes a quantity of magnitude at most $Y$ — an explicit bound, not an asymptotic one. Two numerical constants are fixed once and for all: $T_0 := 3.29\times 10^9$ and $N_0 := 4\times 10^{14}$.

Formalization targets

Goal (Theorem 1.4)

The goal fixes no constants and no thresholds, so no later improvement can invalidate it.

The milestone list is the paper's own attack path, in its numbering: the two numerical verifications (Theorems 1.5, 1.6) and the short-interval prime bound (Theorem 8.1) that together settle $n \le 8.7\times10^{36}$; the $L^2$ apparatus (Lemma 4.4, Proposition 4.10) and Vaughan-type identity (Lemma 4.11) feeding the minor-arc bound (Theorem 5.1) and hence the main exponential sum estimate (Theorem 1.3); the major-arc analysis (Proposition 7.2); and the circle-method core (Theorem 8.2).

Significance

The result itself. Theorem 1.4 lowers Shnirelman's constant from $7$ to $6$ and removes the Riemann hypothesis from Kaniecki's conditional "five primes". Its durable content, however, is not the headline but the explicit exponential sum estimate of Theorem 1.3: a bound on $|S_{\eta_0,q_0}(x,\alpha)|$ with constants small enough to be useful for $x$ between $10^{30}$ and $10^{1300}$, a range where the asymptotically superior estimates of Vinogradov, Chen–Daboussi and Ramaré carry constants too large or too ineffective to apply. That estimate is the reusable object; it has been improved since (Helfgott–Platt) but not superseded in method.

Formalizing it. Status honesty matters here. Theorem 1.4 is closed mathematics, and as a statement it was superseded within a year by Helfgott's ternary Goldbach theorem, which gives three primes for every odd $n > 5$ and hence five a fortiori. Neither Tao's theorem nor Helfgott's is formalized anywhere, and this mission does not claim to be attacking an open problem: the work is formalizing a known, fully explicit proof. That proof happens to be an unusually good formalization target, because every constant in it is written down.

The platform already hosts the surrounding infrastructure. The CircleMethod namespace carries a large verified development of Hardy–Littlewood apparatus following Vaughan, and the ThreePrimes namespace carries a machine-checked proof of Vinogradov's three primes theorem conditional on Siegel–Walfisz. This mission sits directly downstream of both and should import from them rather than rebuild.

Difficulty

The obvious route — deduce five primes from three primes — fails on the range where it is needed. Vinogradov's theorem is asymptotic, and the best effective threshold is $\exp(3100)$; below it the theorem says nothing, and $\exp(3100)$ is far beyond any possible exhaustive check. So the entire difficulty lives in the window $8.7\times10^{36} \le x \le \exp(3100)$, which must be handled by a circle-method argument carrying explicit constants at every step.

Within that window the specific obstruction is the minor arc $T_0/x \ll \|\alpha\|_{\mathbb{R}/\mathbb{Z}} \ll 1/N_0$. A direct Plancherel bound on the $L^2$ side costs a factor of $\log x$, which is more than the argument can afford; Montgomery's uncertainty principle cuts the loss to roughly $2\log x/\log N_0$, and only a large-sieve estimate on prime pairs brings it down to a bounded factor of $8$. On the $L^\infty$ side, Theorem 1.3 must be non-trivial across the whole window, which is why the refinements (1.10)–(1.12) for $q$ near $1$ and near $x$ exist at all. Neither bound alone suffices; the proof closes only because both are pushed to explicit constants simultaneously.

Formalization scope

The goal is stated over $\mathbb{N}$ as a Multiset ℕ of cardinality at most $5$ whose members are all Nat.Prime and whose sum is $n$. A multiset, not a list or a finset: repetition is essential ($9 = 3+3+3$) and order is not. "At most five" is not "exactly five" — $3$ is a sum of one prime and cannot be a sum of five, since the least sum of five primes is $10$. A formalization asserting exactly five primes is false, not merely weaker.

The goal admits no trivializing reading: the empty multiset has sum $0 \ne n$, and the cardinality bound is on the multiset itself, so no prime can be counted with multiplicity zero to evade it.

Everything else in the mission is stated with explicit constants and $O^*(\cdot)$ bounds rather than asymptotic notation, matching the paper: $X = O^*(Y)$ becomes $\|X\| \le Y$ outright. Sums over $n$ are unrestricted sums against a compactly supported cutoff, not sums over Finset.range. Real powers are Real.rpow. The two cutoffs $\eta_0,\eta_1$ and the sum $S_{\eta,q_0}$ are published as mission definitions; solvers should use them verbatim rather than re-deriving equivalent forms.

Three of the milestones are honest dead weight for a solver to attempt directly, and are listed so the dependency graph is truthful rather than because they are tractable. Theorem 1.5 (all zeroes of $\zeta$ up to height $3.29\times10^9$ lie on the critical line) and Theorem 1.6 (every even number up to $4\times10^{14}$ is a sum of two primes) are finite, decidable statements that Lean can express and that are true, but each represents a verified computation of a scale no current proof assistant can replay — Theorem 1.6 alone is $2\times10^{14}$ cases. Theorem 8.1 is quoted from Ramaré–Saouter and itself depends on Theorem 1.5. They are leaves that will stay open; a solver's effort is far better spent on the analytic milestones, and the circle-method core (Theorem 8.2) can be closed independently of them.

A complete development additionally needs the smoothed Vaughan identity bookkeeping, the large sieve in Siebert's form, the von Mangoldt explicit formula with a zero sum (Proposition 7.1), and Bourgain's trick of taking one of the three summands of size $x/K$. The exponential sum machinery is reusable well beyond this mission — it is the standard input to every explicit Goldbach-type result. Contributions to any milestone are welcome independently, and a formalization of Helfgott's theorem that closes the goal by a different route would be an entirely acceptable solution.

Selected references

• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Mathematics of Computation 83 (2014), 997–1038. arXiv:1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. arXiv:1312.7748
• H. A. Helfgott and D. Platt, Numerical verification of the ternary Goldbach conjecture up to $8.875\cdot10^{30}$, 2013. arXiv:1305.3062
• O. Ramaré, On Shnirel'man's constant, Ann. Scuola Norm. Sup. Pisa 22 (1995), 645–706. numdam
• L. Kaniecki, On Shnirelman's constant under the Riemann hypothesis, Acta Arithmetica 72 (1995), 361–374. doi:10.4064/aa-72-4-361-374
• J. Richstein, Verifying the Goldbach conjecture up to $4\cdot10^{14}$, Mathematics of Computation 70 (2001), 1745–1749. doi:10.1090/S0025-5718-00-01290-4
• O. Ramaré and Y. Saouter, Short effective intervals containing primes, Journal of Number Theory 98 (2003), 10–33. doi:10.1016/S0022-314X(02)00029-X
• M. C. Liu and T. Z. Wang, On the Vinogradov bound in the three primes Goldbach conjecture, Acta Arithmetica 105 (2002), 133–175. doi:10.4064/aa105-2-3
• H. L. Montgomery, The analytic principle of the large sieve, Bulletin of the AMS 84 (1978), 547–567. doi:10.1090/S0002-9904-1978-14497-8
• R. C. Vaughan, The Hardy–Littlewood Method, 2nd ed., Cambridge University Press, 1997. doi:10.1017/CBO9780511470929

Motivation

This mission seeks a Lean proof that every odd natural number greater than 1 is the sum of at most three primes. It follows from Helfgott's ternary Goldbach theorem for odd numbers greater than 5, together with the small cases 3 and 5, each of which is itself prime.

Setting and goal

For every natural number n with Odd n and 1 < n, construct a multiset of at most three prime natural numbers whose sum is n. Repetition is allowed and order is irrelevant. Examples include 3 = 3, 5 = 5, 7 = 2 + 2 + 3, and 9 = 3 + 3 + 3. The primes need not all be odd.

Relationship to the five-primes mission

The goal uses the same Multiset ℕ representation and the same hypothesis 1 < n as Every Odd Number Greater Than 1 is the Sum of at Most Five Primes. The cardinality bound changes from s.card ≤ 5 to s.card ≤ 3. No custom definitions are needed.

Formalization scope

The target is unconditional and covers every odd natural number greater than 1. At most three is essential: 3 and 5 cannot be sums of exactly three primes. All summands must satisfy Nat.Prime, and multiplicities count toward the cardinality bound. The initial proposal contains the goal with an open proof, ready for formalization.

Proof approach

A proof may combine a formalization of Helfgott's theorem, which supplies exactly three primes for odd n > 5, with singleton multisets for n = 3 and n = 5. Establishing Helfgott's result requires verified proofs of the analytic and computational ingredients of the chosen argument.

Reference

H. A. Helfgott, The ternary Goldbach conjecture is true, 2013, revised 2014. The mission's at-most-three formulation also includes the elementary cases n = 3 and n = 5.

Motivation

The source defines a two-variable integral on strictly positive-definite real matrices. Its numerator is the absolute bilinear form of A minus B on two unit vectors, while the denominator uses the quadratic forms of A and B. The desired inequality says that componentwise matrix addition is nonexpansive for this quantity, with the larger of the two input distances controlling the output. The surface measure normalization is immaterial because the same constant multiplies every distance.

This mission turns CUHK-Shenzhen AI Math Problem 1, Positive definite matrix integral inequality, 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

For every positive dimension and every four positive-definite matrices A, B, C, and D, prove d(A+B,C+D) is at most max(d(A,C),d(B,D)). The first milestone fixes dimension one, where the sphere and every matrix entry can be analyzed explicitly.

Significance

Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in matrix analysis, positive definite matrices, integral inequality. 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 absolute value prevents a direct cancellation argument, and the denominators couple each integration variable to a different matrix. Positive definiteness gives pointwise positivity but does not immediately compare the ratios after addition. A successful proof must find a convexity, change-of-measure, or projective-metric mechanism that survives the double integral.

Suggested attack route

Promising routes include reducing by congruence to normalized matrices, studying the scalar inequality on each pair of directions, and interpreting the denominator as a density change on the sphere. The dimension-one case should reveal the sharp scalar inequality. Numerical experiments in dimensions two and three may identify equality cases, but the Lean proof must ultimately derive every bound from positivity and measurable integration.

Formalization scope

The Lean model uses finite matrices, Mathlib positive definiteness, the canonical sphere measure obtained from polar decomposition, and an explicit iterated integral. It does not assume symmetry through an unchecked flag: positive definiteness is the Mathlib predicate. Integrability obligations and zero-denominator issues must be proved from positive definiteness.

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

Establish the dimension-one specialization, including any exact evaluation of the two-point sphere integral needed by the proof.

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 May 28, 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 CUHK-Shenzhen problem

Motivation

Harmonic maps into singular nonpositively curved spaces arise in geometric analysis, rigidity theory, and the study of group actions on buildings. Near a point in the domain, their infinitesimal growth is measured by an order, obtained from an Almgren-type frequency quotient. For smooth targets that order is tied to familiar Taylor expansion data. Euclidean buildings are instead assembled from Euclidean apartments along reflection walls, so a map can branch through a singular link and a priori might exhibit a much less controlled spectrum of homogeneities. Breiner and Dees prove that, for maps from surfaces, this spectrum is discrete and is governed by the finite rotational Weyl group of the building. The mission formalizes their headline classification theorem, Theorem 1.1 of Breiner--Dees.

The discreteness matters because frequency information is a basic input to stratification and regularity arguments for singular harmonic maps. A finite list of possible denominators prevents homogeneities from accumulating arbitrarily and isolates rank-one behavior. The formal target makes explicit the nonconstant condition used by the source paper's tangent-map reduction. Without it, the usual numerator and denominator of the frequency quotient both vanish for a constant map, so its order is not defined.

Setting

A Euclidean Coxeter complex consists of Euclidean space together with an affine reflection group. Taking the linear parts of its affine isometries produces a finite rotational reflection group $W$. A Euclidean building of type $W$ is a complete metric space covered by isometric Euclidean apartments whose overlaps are related by elements of the affine Weyl group; the atlas is required to contain the relevant geodesic segments, rays, and lines and to be maximal with these compatibility properties.

The domain is a connected open subset $D$ of a complex one-dimensional manifold, hence a Riemann surface domain. The formalization uses a concrete Korevaar--Schoen-style metric Sobolev energy built from normalized local difference quotients and Lebesgue area in charts. A map $u:D\to X$ is harmonic when it has finite local energy and minimizes that energy against competitors with the same trace. For $x_0\in D$ and small radii $r$, the energy and boundary moment determine a frequency quotient. When its limit exists with positive denominator, that limit is the order $\operatorname{Ord}_u(x_0)$.

Formalization targets

Main classification

For a nonconstant energy-minimizing harmonic map $u:D\to X$ and any $x_0\in D$, prove that the order is defined and that there are positive integers $m,k$ such that

If the building has rank one, prove the sharper form

The same theorem also records the small-scale energy and positive-boundary-moment facts needed for the order to be meaningful; these are conclusions, not assumptions supplied by a solver.

Significance

The result identifies a purely algebraic constraint on an analytic singularity invariant: every denominator divides the order of the finite rotational Weyl group. In rank one, where the target is a tree or an $\mathbb R$-tree, it recovers the half-integer spectrum and its lower bound. This converts an apparently continuous local invariant into a discrete one determined by the building type.

Formalizing the theorem requires reusable infrastructure that is largely absent from current Mathlib: concrete Euclidean-building atlases, metric-valued Sobolev energy, trace and boundary-moment constructions, harmonic energy minimization, frequency quotients, and homogeneous tangent-map interfaces. The paper theorem is proved in ordinary mathematics; the open task is to replace the single sorry in the target with a machine-checked Lean proof. A completed development would provide components useful for other singular-target harmonic-map and CAT(0) formalizations.

Difficulty

The target is not a direct consequence of treating the building as a Euclidean vector space. A harmonic map can cross apartment walls, and a single chart need not contain the image of a punctured neighborhood. The local problem must respect both metric energy and Weyl-group compatibility. Moreover, the frequency quotient is defined through limiting analytic quantities, while the conclusion is an exact rational arithmetic classification. Bridging those levels requires controlling tangent maps and the geometry of directions in the building rather than merely proving monotonicity of the frequency.

The rank-one clause is not obtained by substituting $|W|=2$ into the general statement alone: it also asserts $m\ge2$. The formal proof therefore must preserve the nonconstant hypothesis and the positivity information that rules out the degenerate zero-order case.

Formalization scope

The Lean bundle fixes a complex one-dimensional manifold model for the source, a genuine complete metric target, a finite affine reflection group acting by Euclidean isometries, and an explicit building atlas. The rotational group $W$ is the image of the affine group under taking linear parts, so $|W|$ is not an arbitrary external number. The domain carries a point $x_0$ and is nonempty by construction. The map is required to be nonconstant on the domain; this is the necessary explicit repair of the printed headline, whose later reduction theorem uses the same condition.

Energy, trace, boundary moment, frequency, and order are transparent definitions tied to the supplied geometry. In particular, the caller cannot choose a zero measure or an unrelated predicate to make the target vacuous. The theorem must establish finite small-scale energy, positivity of the boundary moment, existence of the frequency limit, and its classification. Solvers may contribute supporting files for metric Sobolev estimates, tangent-map compactness, homogeneous harmonic-map classification, or finite-reflection-group lemmas, provided they preserve the exact conventions in the definition bundle.

Selected references

• Christine Breiner and Ben K. Dees, On the Possible Orders of Harmonic Maps into Euclidean Buildings, Calculus of Variations and Partial Differential Equations, 2026, Theorem 1.1 and Sections 2--4. DOI
• Mikhail Gromov and Richard Schoen, Harmonic Maps into Singular Spaces and p-adic Superrigidity for Lattices in Groups of Rank One, Publications Mathématiques de l'IHÉS 76 (1992), 165--246. EuDML

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

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

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

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

An elliptic curve over $\mathbb{Q}$ is a smooth cubic curve with a rational point. Its rational points form a finitely generated abelian group $E(\mathbb{Q})$ (Mordell, 1922), so $E(\mathbb{Q}) \simeq \mathbb{Z}^r \oplus E(\mathbb{Q})_{\mathrm{tors}}$ for an integer $r \ge 0$, the rank. No algorithm is known that decides, for a given curve, whether $r > 0$, i.e. whether there are infinitely many rational points. The Birch and Swinnerton-Dyer conjecture predicts $r$ from an analytic object, the Hasse–Weil $L$-function $L(E,s)$: it asserts that $r$ equals the order of vanishing of $L(E,s)$ at $s = 1$. It is one of the seven Millennium Prize Problems of the Clay Mathematics Institute; the official formulation is Andrew Wiles' problem description, The Birch and Swinnerton-Dyer Conjecture (2000). This mission formalizes that statement, its weak form, and the results Wiles lists as known.

Timeline.

• 1922: L. Mordell (Proc. Cambridge Phil. Soc. 21) proves that $E(\mathbb{Q})$ is finitely generated, answering a question of Poincaré (1901).
• 1936: H. Hasse proves $|p + 1 - \#E(\mathbb{F}_p)| \le 2\sqrt p$ at primes of good reduction, so the Euler product for $L(E,s)$ converges for $\operatorname{Re} s > 3/2$; he conjectures that $L(E,s)$ continues to an entire function.
• 1965: B. Birch and H. P. F. Swinnerton-Dyer, Notes on elliptic curves II, state the conjecture, found experimentally on the EDSAC computer.
• 1977: J. Coates and A. Wiles, On the conjecture of Birch and Swinnerton-Dyer: for curves with complex multiplication, $L(E,1) \ne 0$ implies $E(\mathbb{Q})$ finite.
• 1986: B. Gross and D. Zagier, Heegner points and derivatives of L-series: for modular $E$ with $L(E,1) = 0 \ne L'(E,1)$, a Heegner point has infinite order.
• 1989–1990: V. Kolyvagin, Finiteness of $E(\mathbb{Q})$ and Ш$(E,\mathbb{Q})$ for a subclass of Weil curves: for modular $E$ with $L(E,s)$ vanishing to order at most $1$ at $s=1$, the rank equals that order (with a non-vanishing theorem of Bump–Friedberg–Hoffstein and Murty–Murty).
• 1995–2001: A. Wiles (Ann. Math. 141), R. Taylor and A. Wiles (Ann. Math. 141), and C. Breuil, B. Conrad, F. Diamond and R. Taylor (J. Amer. Math. Soc. 14): every elliptic curve over $\mathbb{Q}$ is modular, so $L(E,s)$ is entire and Kolyvagin's theorem applies to all $E/\mathbb{Q}$.
• 2000: the Clay Mathematics Institute adopts Wiles' formulation as a Millennium Prize Problem.
• 2014: M. Bhargava, C. Skinner and W. Zhang, A majority of elliptic curves over $\mathbb{Q}$ satisfy the Birch and Swinnerton-Dyer conjecture: the rank conjecture holds for more than $66\%$ of curves ordered by height. The general case is open.

Setting

A Weierstrass equation over $\mathbb{Q}$ is

with discriminant $\Delta$; in Lean, WeierstrassCurve ℚ. It is an elliptic curve when $\Delta \ne 0$ (Mathlib's typeclass IsElliptic). Its rational points $E(\mathbb{Q})$ are the rational solutions $(x,y)$ together with the point at infinity $O$, an abelian group under the chord-and-tangent law (W.toAffine.Point). The rank is the rank of this group as a $\mathbb{Z}$-module, $r = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{Q}) \qquad \text{(`BSD.rank W`)},$ the $r$ in $E(\mathbb{Q}) \simeq \mathbb{Z}^r \oplus E(\mathbb{Q})_{\mathrm{tors}}$.

The Hasse–Weil $L$-series is built prime by prime. For each prime $p$ take a Weierstrass equation for $E$ that is minimal at $p$ (integral coefficients, with the $p$-adic valuation of $\Delta$ as small as possible) and reduce it modulo $p$; put $a_p = p + 1 - \#\tilde E(\mathbb{F}_p)$ when the reduction is smooth (good reduction). The local factor is

and $L(E,s) = \prod_p L_p(E,s) = \sum_{n \ge 1} a_n n^{-s}$, convergent for $\operatorname{Re} s > 3/2$ by Hasse's bound. In Lean this is Mathlib's WeierstrassCurve.LSeries W s, defined by exactly this recipe (WeierstrassCurve.LFunction is the arithmetic function $n \mapsto a_n$, an Euler product of local factors computed on a model minimal at each prime); where the Dirichlet series does not converge, Mathlib's LSeries takes the junk value $0$. This is the complete $L$-series $L^*(C,s)$ of Wiles' Remark 1; it differs from the incomplete product over $p \nmid 2\Delta$ in Wiles' display by finitely many factors holomorphic and non-zero at $s = 1$, so both have the same order of vanishing there.

An $L$-function of $E$ is an entire function $\Lambda : \mathbb{C} \to \mathbb{C}$ with $\Lambda(s) = L(E,s)$ for $\operatorname{Re} s > 3/2$ (BSD.IsLFunction W Λ). By the identity theorem there is at most one; by modularity there is exactly one. The order of vanishing of $\Lambda$ at $s = 1$ is the $m$ with $\Lambda(s) = c(s-1)^m + \dots$, $c \ne 0$; in Lean, analyticOrderAt Λ 1, valued in $\mathbb{N} \cup \{\infty\}$, with value $\infty$ exactly when $\Lambda$ vanishes identically near $1$.

Formalization targets

Goal: the Birch and Swinnerton-Dyer conjecture (BSD.birch_swinnerton_dyer)

For every elliptic curve $E$ over $\mathbb{Q}$ there is an entire $\Lambda$ agreeing with $L(E,s)$ on $\operatorname{Re} s > 3/2$ such that

This is Wiles' Conjecture (Birch and Swinnerton-Dyer): $L(C,s) = c(s-1)^r + \text{higher order terms}$ with $c \ne 0$ and $r = \operatorname{rank} C(\mathbb{Q})$. Open.

Weaker target: the weak conjecture (BSD.weak_birch_swinnerton_dyer)

There is an $L$-function $\Lambda$ of $E$ with $\Lambda(1) = 0$ if and only if $E(\mathbb{Q})$ is infinite. Wiles: "In particular this conjecture asserts that $L(C,1) = 0 \Leftrightarrow C(\mathbb{Q})$ is infinite." Open.

Milestones: what Wiles lists as known

1. Mordell's theorem (BSD.mordell): $E(\mathbb{Q})$ is a finitely generated abelian group.
2. Convergence of the $L$-series (BSD.lSeriesSummable): $\sum a_n n^{-s}$ converges for $\operatorname{Re} s > 3/2$. Wiles: "this Euler product is then known to converge for $\operatorname{Re}(s) > 3/2$."
3. Analytic continuation (BSD.exists_isLFunction): $E$ has an $L$-function. Wiles: Hasse's conjecture, "now been proved" by Wiles, Taylor–Wiles and Breuil–Conrad–Diamond–Taylor.
4. Gross–Zagier–Kolyvagin (BSD.birch_swinnerton_dyer_of_analyticOrderAt_le_one): if an $L$-function of $E$ vanishes to order at most $1$ at $s = 1$, its order equals the rank. Wiles: "If $L(C,s) \sim c(s-1)^m$ with $c \ne 0$ and $m = 0$ or $1$, then the conjecture holds."

A bridging lemma, BSD.isLFunction_unique, records that an $L$-function of $E$ is unique when it exists.

Significance

The result itself. The conjecture makes the finiteness of $E(\mathbb{Q})$ decidable from $L(E,1)$ and, in its refined form, gives an effective procedure for finding generators (Manin, 1971). Conditionally on it, Tunnell (1983) characterises the congruent numbers, the areas of right triangles with rational sides, a problem open since the tenth century. It is the prototype of the conjectures of Tate, Deligne, Beilinson and Bloch–Kato relating ranks of arithmetic groups to orders of vanishing of $L$-functions.

Formalizing it. None of the statements in this mission has a machine-checked proof. Mathlib provides the objects: the group law on $E(\mathbb{Q})$, minimal models and reduction types over discrete valuation rings, and the Hasse–Weil $L$-series as a Dirichlet series (2025–2026). It does not contain Mordell's theorem (no theory of heights), Hasse's bound, modularity, or the continuation of $L(E,s)$. On this platform, earlier library entries named birch_swinnerton_dyer are retired placeholders whose formal statements reduce to trivialities such as $0 = 0$; they carry a notice saying so and are not formalizations of the conjecture. This mission gives the first faithful statement against Mathlib's own $L$-series. Two published platform results bear directly on the milestones: the descent step WeierstrassCurve.Affine.Point.addGroup_fg_of_finiteIndex (finite index of $2E(\mathbb{Q})$ implies finite generation) reduces milestone 1 to the weak Mordell–Weil theorem, and WeierstrassCurve.modularity_of_semistableModel from the platform's Fermat's Last Theorem development proves modularity of semistable curves for a notion of modularity defined through eigenform coefficients; relating that notion to WeierstrassCurve.LSeries would give milestone 3 for semistable curves.

Difficulty

Neither side of the equation is computable in general. On the algebraic side, descent bounds the rank from above by the rank of a Selmer group, but the gap is the Tate–Shafarevich group Ш$(E)$, which is not known to be finite; the obvious plan, compute the Selmer group and show it has the rank of $E(\mathbb{Q})$, founders on Ш. On the analytic side one can certify $\Lambda(1) \ne 0$ or $\Lambda'(1) \ne 0$ numerically but cannot certify an exact zero, and the only known bridge from $L$-values to rational points, the Heegner point construction, produces at most one independent point. This is why milestone 4 stops at order $\le 1$ and the conjecture is not known for a single curve of rank $\ge 2$. Iwasawa theory (Kato, Skinner–Urban) relates $p$-adic $L$-functions to Selmer groups but yields $p$-adic, not Archimedean, orders of vanishing.

The formalization adds its own obstacles: milestone 1 needs heights and the weak Mordell–Weil theorem (Kummer theory over number fields, finiteness of class groups and units); milestone 2 needs Hasse's bound, i.e. the degree of the Frobenius endomorphism; milestones 3 and 4 rest on modularity, Galois representations, modular curves and Euler systems.

Formalization scope

• $E$ is any WeierstrassCurve ℚ with IsElliptic ($\Delta \ne 0$); no minimality or integrality of the model is assumed. Mathlib's $L$-series passes to a minimal model at each prime internally, and the point group depends only on the curve, so every statement is invariant under change of Weierstrass equation.
• The rank is Module.finrank ℤ W.toAffine.Point: for a finitely generated abelian group, the $r$ in $\mathbb{Z}^r \oplus T$; for a group of infinite rank Mathlib's finrank is $0$, a case milestone 1 excludes.
• The $L$-series is Mathlib's WeierstrassCurve.LSeries, with all Euler factors including the bad primes, and junk value $0$ where the Dirichlet series diverges. BSD.IsLFunction constrains $\Lambda$ only on $\operatorname{Re} s > 3/2$; milestone 2 shows the series is genuine there, and the bridging lemma shows $\Lambda$ is then unique.
• The order of vanishing is analyticOrderAt Λ 1 : ℕ∞; equating it with a natural number asserts in particular that $\Lambda \not\equiv 0$ near $1$.

No trivializing formalization. The existential $\Lambda$ cannot be chosen freely: it must agree with the honest, non-zero Dirichlet series on a half-plane, so it is unique, and $\Lambda \equiv 0$ is excluded by the finite value of the rank. Without IsElliptic the statements would concern singular cubics, whose point group is $\mathbb{Q}$ or $\mathbb{Q}^\times$; the hypothesis is required, not decorative.

Out of scope. The refined conjecture (the leading coefficient in terms of Ш$(E)$, the regulator, the real period and the Tamagawa numbers), the finiteness of Ш$(E)$, number fields and abelian varieties, and the functional equation of $L(E,s)$.

Infrastructure needed and welcome contributions. Heights on $E(\mathbb{Q})$ and the weak Mordell–Weil theorem; Hasse's bound and the multiplicativity of $a_n$; a bridge from Mathlib's WeierstrassCurve.LSeries to the $L$-series of a weight-two newform, so that existing modularity results yield milestone 3; Heegner points and Kolyvagin's Euler system for milestone 4; and the bridging lemma, provable now from the identity theorem. Decompositions of every milestone and lemmas about WeierstrassCurve.LFunction (its values at primes, multiplicativity, independence of the model) are welcome.

Selected references

• A. Wiles, The Birch and Swinnerton-Dyer Conjecture, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdf
• B. J. Birch, H. P. F. Swinnerton-Dyer, Notes on elliptic curves II, Journal für die reine und angewandte Mathematik 218 (1965), 79–108. https://doi.org/10.1515/crll.1965.218.79
• L. J. Mordell, On the rational solutions of the indeterminate equations of the third and fourth degrees, Proceedings of the Cambridge Philosophical Society 21 (1922), 179–192.
• J. Coates, A. Wiles, On the conjecture of Birch and Swinnerton-Dyer, Inventiones Mathematicae 39 (1977), 223–251. https://doi.org/10.1007/BF01402975
• B. H. Gross, D. B. Zagier, Heegner points and derivatives of L-series, Inventiones Mathematicae 84 (1986), 225–320. https://doi.org/10.1007/BF01388809
• V. A. Kolyvagin, Finiteness of $E(\mathbb{Q})$ and Ш$(E,\mathbb{Q})$ for a subclass of Weil curves, Mathematics of the USSR-Izvestiya 32 (1989), 523–541. https://doi.org/10.1070/IM1989v032n03ABEH000779
• A. Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 443–551. https://doi.org/10.2307/2118559
• R. Taylor, A. Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572. https://doi.org/10.2307/2118560
• C. Breuil, B. Conrad, F. Diamond, R. Taylor, On the modularity of elliptic curves over $\mathbb{Q}$: wild 3-adic exercises, Journal of the American Mathematical Society 14 (2001), 843–939. https://doi.org/10.1090/S0894-0347-01-00370-8
• J. B. Tunnell, A classical Diophantine problem and modular forms of weight 3/2, Inventiones Mathematicae 72 (1983), 323–334. https://doi.org/10.1007/BF01389327
• M. Bhargava, C. Skinner, W. Zhang, A majority of elliptic curves over $\mathbb{Q}$ satisfy the Birch and Swinnerton-Dyer conjecture, 2014. https://arxiv.org/abs/1407.1826
• J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., Graduate Texts in Mathematics 106, Springer, 2009. https://doi.org/10.1007/978-0-387-09494-6

Motivation

The incompressible Navier–Stokes equations are the standard model for the motion of a viscous fluid such as water or air, used daily in engineering, meteorology and oceanography. Yet the most basic mathematical question about them is open: starting from smooth initial data in three dimensions, does a smooth solution exist for all time? This is one of the seven Millennium Prize Problems of the Clay Mathematics Institute. Its official formulation is Charles Fefferman's problem description, Existence and smoothness of the Navier–Stokes equation (2000), which offers a prize for a proof of any one of four statements: global existence and smoothness on $\mathbb{R}^3$ (statement (A)) or on the torus $\mathbb{R}^3/\mathbb{Z}^3$ (statement (B)), or a counterexample to either (statements (C) and (D)). This mission formalizes statement (A), together with the classical partial results that Fefferman lists as known.

Timeline.

• 1822–1845: Navier and Stokes write down the equations of a viscous incompressible fluid.
• 1934: Jean Leray, Sur le mouvement d'un liquide visqueux emplissant l'espace (Acta Math. 63), proves on $\mathbb{R}^3$ that smooth solutions exist for a positive time depending on the data, that they exist for all time when the data is small compared with the viscosity, and that global weak solutions with finite energy always exist. Their smoothness and uniqueness are left open.
• 1933–1969: the two-dimensional problem is settled (Leray for the plane; Olga Ladyzhenskaya's monograph The Mathematical Theory of Viscous Incompressible Flow, 2nd ed. 1969, for bounded domains): smooth solutions exist for all time and are unique.
• 1984: Tosio Kato, Strong $L^p$-solutions of the Navier–Stokes equation in $\mathbb{R}^m$ (Math. Z. 187), gives global solutions for initial data small in $L^3(\mathbb{R}^3)$.
• 1976–1998: partial regularity. Scheffer, then Caffarelli, Kohn and Nirenberg (Comm. Pure Appl. Math. 35, 1982), show that the singular set of a suitable weak solution has one-dimensional parabolic Hausdorff measure zero.
• 2000: the Clay Mathematics Institute adopts Fefferman's formulation as a Millennium Prize Problem. It remains open.

Setting

Fix a dimension $n \ge 1$ and write $\mathbb{R}^n$ for Euclidean $n$-space with its Euclidean norm $|x|$; in Lean this is NavierStokes.Vec n. A velocity field assigns to each time $t \in \mathbb{R}$ and point $x \in \mathbb{R}^n$ a vector $u(x,t) \in \mathbb{R}^n$; in Lean $u\,t$ is the field at time $t$ and $u\,t\,x$ is Fefferman's $u(x,t)$. A pressure is a real function $p(x,t)$. The viscosity $\nu$ is a positive constant. The external force of Fefferman's equation (1) is identically zero throughout, as in statement (A).

For a vector field $v : \mathbb{R}^n \to \mathbb{R}^n$ the divergence is

in Lean NavierStokes.div, computed from the Fréchet derivative $Dv(x)$ as $\sum_i (Dv(x)\,e_i)_i$. The Laplacian $\Delta v = \sum_i \partial^2 v/\partial x_i^2$ acts componentwise (Mathlib's Laplacian on inner product spaces). The gradient $\nabla p$ is Mathlib's gradient. The convective term $\sum_j u_j\,\partial u/\partial x_j$ is the derivative of $u(\cdot,t)$ at $x$ in the direction $u(x,t)$. Finally $|\nabla v|^2 = \sum_{i,j} (\partial v_i/\partial x_j)^2$ is NavierStokes.gradNormSq.

Admissible initial data (Fefferman's condition (4), NavierStokes.IsInitialData): a $C^\infty$, divergence-free vector field $u^0$ that decays together with all its derivatives faster than any power,

In Lean the bound is $(1+|x|)^K\,\|D^k u^0(x)\| \le C_{kK}$ on the $k$-th Fréchet derivative, an equivalent family of conditions. These are exactly the divergence-free Schwartz functions.

A physically reasonable solution on a set $S$ of times (NavierStokes.IsSolutionOn; $S = [0,\infty)$ for NavierStokes.IsSolution) is a pair $(u,p)$ such that

1. (Fefferman (6)) $u$ and $p$ are $C^\infty$ on $S \times \mathbb{R}^n$, up to the boundary of $S$;
2. (Fefferman (1), $f \equiv 0$) for every $t \in S$ with $t > 0$ and every $x$,

3. (Fefferman (2)) $\operatorname{div} u(\cdot,t) = 0$ for every $t \in S$;
4. (Fefferman (3)) $u(x,0) = u^0(x)$;
5. (Fefferman (7), bounded energy) $\int_{\mathbb{R}^n} |u(x,t)|^2\,dx < C$ for all $t \in S$, for some constant $C$.

Formalization targets

Goal: Fefferman's statement (A)

Take $\nu > 0$ and $n = 3$. For every admissible initial datum $u^0$ there exist a velocity field $u$ and a pressure $p$ forming a physically reasonable solution on $\mathbb{R}^3 \times [0,\infty)$:

This is NavierStokes.existence_and_smoothness_R3. It is open; a proof would settle the Millennium Prize Problem in the affirmative.

Milestones: what Fefferman lists as known

1. Local existence (NavierStokes.local_existence_R3): for $n = 3$ and every admissible $u^0$ there are $T > 0$ and a physically reasonable solution on $\mathbb{R}^3 \times [0,T)$. Fefferman: "(A) and (B) hold ... if the time interval $[0,\infty)$ is replaced by a small time interval $[0,T)$, with $T$ depending on the initial data."
2. Global existence for small data (NavierStokes.small_data_global_existence_R3): there is an absolute constant $c > 0$ such that, for $n = 3$, (A) holds for every admissible $u^0$ with

Fefferman: "(A) and (B) hold provided the initial velocity $u^0$ satisfies a smallness condition." The scale-invariant product is Leray's form of the condition; it implies smallness of $\|u^0\|_{L^3}/\nu$, so Kato's theorem also applies. 3. The two-dimensional case (NavierStokes.existence_and_smoothness_R2): statement (A) with $n = 2$. Fefferman: "In two dimensions, the analogues of assertions (A) and (B) have been known for a long time (Ladyzhenskaya)."

A bridging lemma, NavierStokes.isInitialData_iff_schwartz, identifies the admissible data with the divergence-free elements of Mathlib's Schwartz space.

Significance

The result itself. Statement (A) asks whether the basic model of viscous flow is well posed in the classical sense, i.e. whether smooth finite-energy flows can develop singularities in finite time. A positive answer shows the equations never leave the classical regime; a negative one shows the model predicts its own breakdown. Fefferman: "since we don't even know whether these solutions exist, our understanding is at a very primitive level."

Formalizing it. None of the results in this mission has a machine-checked proof, and Mathlib contains no theory of the Navier–Stokes or Euler equations. The milestones are all proved in the literature; formalizing them requires building, on Mathlib's calculus, measure theory and Schwartz space, the heat semigroup on $\mathbb{R}^n$, the pressure equation $\Delta p = -\sum_{i,j} \partial_i\partial_j(u_i u_j)$ or the Leray projection, energy estimates, and a fixed-point construction of solutions, most of which is reusable for other evolution equations. The goal is open and expected to remain so; its role is to fix in Lean the exact statement the prize asks for, so partial results are formalized against it.

Difficulty

The energy identity $\frac{d}{dt}\int|u|^2 = -2\nu\int|\nabla u|^2$ controls $u$ in $L^2$ and $\nabla u$ in $L^2_{t,x}$, but in three dimensions this control is supercritical: under the scaling $u_\lambda(x,t) = \lambda u(\lambda x, \lambda^2 t)$ that preserves the equations, the energy of $u_\lambda$ shrinks as $\lambda \to \infty$, so bounded energy does not prevent concentration at small scales. Every known continuation criterion (Leray, Prodi–Serrin, Beale–Kato–Majda, Escauriaza–Seregin–Šverák) needs a quantity at or above critical scaling, none of which the energy controls. The obvious first idea, an ordinary differential inequality for $\|\nabla u(t)\|_{L^2}$, gives $\frac{d}{dt}\|\nabla u\|_{L^2}^2 \le C\nu^{-3}\|\nabla u\|_{L^2}^6$, which closes only for small data or short time. That is exactly why milestones 1 and 2 are theorems and the goal is not.

The formalization adds a second difficulty: the solutions of the literature live in Sobolev or Besov spaces, with pointwise smoothness of $u$ and $p$ recovered afterwards by regularity theory, and Mathlib has neither Sobolev spaces on $\mathbb{R}^n$ nor the heat semigroup in usable form.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure; the dimension is a parameter, the goal fixes $n = 3$ and the 2D milestone $n = 2$.
• A velocity field is a function of all real times, but every condition is imposed only on the time set $S$; values at negative times are unconstrained.
• Smoothness on $\mathbb{R}^n \times [0,\infty)$ is Mathlib's ContDiffOn of the uncurried map on the closed half-space, i.e. all derivatives extend continuously to $t = 0$. The momentum equation is imposed at interior times $t > 0$ with two-sided derivatives; by continuity of the derivatives this is equivalent to Fefferman's "$t \ge 0$".
• Derivatives are Mathlib's total functions (fderiv, deriv, iteratedFDeriv, gradient, Laplacian) with junk value $0$ at non-differentiable points; the smoothness hypotheses make every derivative in the statements honest.
• The energy is a Lebesgue integral in $[0,\infty]$, equal to $\infty$ when $u(\cdot,t) \notin L^2$, so bounded energy cannot hold vacuously. The $L^2$ norms in the small-data hypothesis are Bochner integrals, genuine for Schwartz data.
• No normalization is imposed on the pressure, as in Fefferman's text.

No trivializing formalization. The zero field solves the equations only for $u^0 = 0$; for any other admissible $u^0$ the initial condition, smoothness, the equation on $t > 0$ and bounded energy must all hold.

Infrastructure needed and welcome contributions. The heat kernel on $\mathbb{R}^n$ with Schwartz bounds; the Riesz-transform representation of the pressure or the Leray projection; energy identities for smooth decaying solutions; local existence by Picard iteration; the two-dimensional vorticity equation and its maximum principle. Theorems in the NavierStokes namespace, decompositions of the milestones, and Mathlib lemmas about ContDiffOn on half-spaces are all welcome. Statements (B), (C), (D) and the Euler equations ($\nu = 0$) are out of scope.

Selected references

• C. L. Fefferman, Existence and smoothness of the Navier–Stokes equation, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf
• J. Leray, Sur le mouvement d'un liquide visqueux emplissant l'espace, Acta Mathematica 63 (1934), 193–248. https://doi.org/10.1007/BF02547354
• O. A. Ladyzhenskaya, The Mathematical Theory of Viscous Incompressible Flow, 2nd ed., Gordon and Breach, 1969. https://archive.org/details/mathematicaltheo0000lady
• T. Kato, Strong $L^p$-solutions of the Navier–Stokes equation in $\mathbb{R}^m$, with applications to weak solutions, Mathematische Zeitschrift 187 (1984), 471–480. https://doi.org/10.1007/BF01174182
• L. Caffarelli, R. Kohn, L. Nirenberg, Partial regularity of suitable weak solutions of the Navier–Stokes equations, Communications on Pure and Applied Mathematics 35 (1982), 771–831. https://doi.org/10.1002/cpa.3160350604
• A. J. Majda, A. L. Bertozzi, Vorticity and Incompressible Flow, Cambridge University Press, 2002. https://doi.org/10.1017/CBO9780511613203
• J. C. Robinson, J. L. Rodrigo, W. Sadowski, The Three-Dimensional Navier–Stokes Equations: Classical Theory, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781139095143