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

$$S_{\eta,q_0}(x,\alpha) \;:=\; \sum_{n} \Lambda(n)\,e(\alpha n)\, \mathbf{1}_{(n,q_0)=1}\,\eta(n/x).$$

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

$$\eta_0(t) := 4\big(\log 2 - |\log 2t|\big)_+$$

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

$$\eta_1(t) := \big(1 - 10\,\mathrm{dist}(t,[0.2,0.8])\big)_+$$

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)

$$\forall n \text{ odd},\ n > 1 \;\Longrightarrow\; \exists\, p_1,\dots,p_k \text{ prime},\ k \le 5,\ n = p_1 + \cdots + p_k.$$

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

$$\operatorname{Ord}_u(x_0)=\frac{m}{k}, \qquad k\mid |W|.$$

If the building has rank one, prove the sharper form

$$\operatorname{Ord}_u(x_0)=\frac{m}{2} \qquad\text{for some integer }m\ge 2.$$

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

$$\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

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

$$E :\ y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6, \qquad a_i \in \mathbb{Q},$$

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

$$L_p(E,s) = \begin{cases} (1 - a_p p^{-s} + p^{1-2s})^{-1} & \text{good reduction,}\\ (1 - p^{-s})^{-1} & \text{split multiplicative reduction,}\\ (1 + p^{-s})^{-1} & \text{non-split multiplicative reduction,}\\ 1 & \text{additive reduction,}\end{cases}$$

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

$$\operatorname{ord}_{s=1} \Lambda = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{Q}).$$

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

$$\operatorname{div} v = \sum_{i=1}^n \frac{\partial v_i}{\partial x_i},$$

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,

$$|\partial_x^\alpha u^0(x)| \le C_{\alpha K}\,(1+|x|)^{-K} \quad \text{on } \mathbb{R}^n, \text{ for every } \alpha \text{ and } K.$$

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$,

$$\frac{\partial u}{\partial t} + \sum_{j=1}^n u_j \frac{\partial u}{\partial x_j} = \nu\,\Delta u - \nabla p;$$

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)$:

$$\forall\, \nu > 0,\ \forall\, u^0 \text{ satisfying (4)},\ \exists\, (u,p) \text{ satisfying (1), (2), (3), (6), (7) 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

$$\|u^0\|_{L^2}^2\,\|\nabla u^0\|_{L^2}^2 \le c\,\nu^4.$$

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

Why holomorphic functions of several variables

Several complex variables studies functions of $z = (z_1, \dots, z_n) \in \mathbb{C}^n$ that are holomorphic in every coordinate. It underlies complex geometry, the theory of analytic spaces, and parts of mathematical physics and harmonic analysis. Every later topic of the subject (domains of holomorphy, pseudoconvexity, the $\bar\partial$-problem, the Bergman kernel, analytic varieties) starts from the same foundation: a function that is holomorphic in each variable separately and locally bounded is jointly smooth and is locally the sum of a convergent power series. This mission formalizes that foundation as it appears in the first chapter of Jiří Lebl's textbook Tasty Bits of Several Complex Variables (jirka.org/scv).

Historically, the step from separate to joint regularity is due to Osgood (1899), who showed that a continuous (later: locally bounded) function that is holomorphic in each variable separately is holomorphic; Hartogs (1906) later removed the boundedness assumption altogether, a much harder theorem not covered here.

Setting

Points of $\mathbb{C}^n$ are $z = (z_1, \dots, z_n)$. For a center $a \in \mathbb{C}^n$ and a polyradius $\rho = (\rho_1, \dots, \rho_n)$ with every $\rho_k > 0$, the polydisc is

$$\Delta_\rho(a) = \{ z \in \mathbb{C}^n : |z_k - a_k| < \rho_k,\ k = 1, \dots, n \},$$

a product of open discs $\Delta_1 \times \cdots \times \Delta_n$. Its distinguished boundary is the torus $\Gamma = \partial\Delta_1 \times \cdots \times \partial\Delta_n = \{ |\zeta_k - a_k| = \rho_k \text{ for all } k \}$, and $\overline{\Delta}$ denotes the closed polydisc.

A function $f$ on an open set $U \subset \mathbb{C}^n$ is holomorphic (the book's Definition 1.1.2) if it is locally bounded (every point of $U$ has a neighborhood on which $f$ is bounded) and complex-differentiable in each variable separately: for every $z \in U$ and every $k$, the one-variable limit

$$\lim_{\xi \to 0} \frac{f(z_1, \dots, z_k + \xi, \dots, z_n) - f(z)}{\xi}$$

exists. A map $f = (f_1, \dots, f_m) : U \to \mathbb{C}^m$ is holomorphic if every component is.

A multi-index is $\alpha = (\alpha_1, \dots, \alpha_n) \in \mathbb{N}_0^n$, with $\alpha! = \alpha_1! \cdots \alpha_n!$, $(z-a)^\alpha = \prod_k (z_k - a_k)^{\alpha_k}$ and $\rho^\alpha = \prod_k \rho_k^{\alpha_k}$. A power series $\sum_\alpha c_\alpha (z-a)^\alpha$ is summed over all multi-indices; since $\mathbb{N}_0^n$ has no natural order, convergence means absolute convergence, and the series converges uniformly absolutely on a set $X$ when $\sum_\alpha |c_\alpha (z-a)^\alpha|$ converges uniformly for $z \in X$. The Wirtinger derivative is $\partial/\partial z_k = \tfrac12(\partial/\partial x_k - i\,\partial/\partial y_k)$ for $z_k = x_k + i y_k$, and $\partial^{|\alpha|}/\partial z^\alpha$ applies $\partial/\partial z_k$ exactly $\alpha_k$ times for each $k$.

Formalization targets

Goal: Theorem 1.2.1 (power series on a polydisc)

Let $\Delta = \Delta_\rho(a)$ be a polydisc. If $f : \overline{\Delta} \to \mathbb{C}$ is continuous and holomorphic in $\Delta$, then there are coefficients $c_\alpha$ with

$$f(z) = \sum_\alpha c_\alpha (z-a)^\alpha \qquad (z \in \Delta),$$

the series converging uniformly absolutely on every compact subset of $\Delta$. Conversely, a function defined on $\Delta$ by such a series is holomorphic on $\Delta$. Both directions are part of the goal.

Milestones

In attack order:

1. Proposition 1.1.3. A holomorphic function on an open $U$ is $C^\infty$, and every $\partial f/\partial z_k$ is again holomorphic.
2. Theorem 1.1.4 (Cauchy integral formula). For $f$ continuous on $\overline{\Delta}$ and holomorphic in $\Delta$, and $z \in \Delta$,

$$f(z) = \frac{1}{(2\pi i)^n} \int_\Gamma \frac{f(\zeta)}{(\zeta_1 - z_1)\cdots(\zeta_n - z_n)}\, d\zeta_1 \wedge \cdots \wedge d\zeta_n.$$

3. Proposition 1.2.2. The derivative formula $\frac{\partial^{|\alpha|} f}{\partial z^\alpha}(z) = \frac{1}{(2\pi i)^n}\int_\Gamma \frac{\alpha!\, f(\zeta)}{(\zeta - z)^{\alpha+1}}\,d\zeta$, the coefficient formula $c_\alpha = \frac{1}{\alpha!}\frac{\partial^{|\alpha|} f}{\partial z^\alpha}(a)$, and the Cauchy estimates $|c_\alpha| \le \|f\|_\Gamma / \rho^\alpha$.
4. Proposition 1.2.3. A limit, uniform on compact subsets, of holomorphic functions is holomorphic, and all derivatives $\partial^{|\alpha|}/\partial z^\alpha$ converge uniformly on compact subsets.
5. Theorem 1.2.7 (identity theorem). On a domain, a holomorphic function vanishing on a nonempty open subset vanishes identically.
6. Theorem 1.2.8 (maximum principle). On a domain, if $|f|$ has a local maximum at $a$, then $f \equiv f(a)$.
7. Theorem 1.3.5. Compositions of holomorphic mappings are holomorphic.
8. Proposition 1.3.7. For holomorphic $f : U \to \mathbb{C}^n$, $|\det Df(p)|^2 = \det D_{\mathbb{R}} f(p)$.

Significance

Theorem 1.2.1 is the statement that makes the theory of several complex variables possible: it identifies the book's elementary, one-variable-at-a-time definition of holomorphy with local representability by power series. Uniqueness of the coefficients, the Cauchy estimates, the identity theorem, the maximum principle, and holomorphy of compositions and of implicit functions all follow from it, and every later chapter of the book (Hartogs figures, pseudoconvexity, the Bergman kernel, Weierstrass preparation) uses it without comment.

Mathlib already develops complex analysis in several variables for Fréchet-differentiable maps: analyticity of DifferentiableOn ℂ functions, torusIntegral, Cauchy integrals over circles, and Osgood-type regularity for maps on $\mathbb{C}^n$ are available or published on the platform. What this mission adds is the bridge from the weaker separate notion of holomorphy, with local boundedness, to these results, stated with multi-index power series and uniform absolute convergence on compact sets exactly as in the textbook. The results are classical and fully proved in the book; none has a machine-checked proof in this form.

Difficulty

The hypothesis controls $f$ only along complex lines parallel to the coordinate axes, plus a bound. Nothing in the definition says that $f$ is continuous, let alone jointly differentiable, so no joint limit, Fréchet derivative, or change of the order of integration is available at the start. Every tool that the one-variable theory and Mathlib's multivariable library supply presupposes joint regularity; the obstacle is to obtain it from separate information.

A second difficulty is bookkeeping: power series over $\mathbb{N}_0^n$ have no natural order, so convergence must be handled as unconditional summation with a uniformity statement over compact sets, and iterated Wirtinger derivatives must be related to derivatives of the series term by term.

Formalization scope

• $\mathbb{C}^n$ is Fin n → ℂ; multi-indices are Fin n → ℕ. A polyradius is ρ : Fin n → ℝ with the hypothesis ∀ k, 0 < ρ k; the polydisc is defined coordinatewise (not Metric.ball, which only gives equal radii).
• Holomorphy is the book's Definition 1.1.2, IsHolomorphicOn f U: local boundedness plus complex differentiability at $\xi = 0$ of $\xi \mapsto f(z_1, \dots, z_k + \xi, \dots, z_n)$ (via Function.update). Openness of $U$ is a hypothesis wherever the book says "open". Maps into $\mathbb{C}^m$ are holomorphic componentwise.
• Ruled out: defining holomorphy as Mathlib's DifferentiableOn ℂ. That makes Proposition 1.1.3 and the first half of the goal off-target (they would follow from existing library results) and is not the book's definition.
• The closed polydisc is closure (polydisc a ρ); "continuous on $\overline{\Delta}$, holomorphic in $\Delta$" keeps both hypotheses.
• Power series: HasSum (unconditional summation) of the terms $c_\alpha (z-a)^\alpha$ to $f(z)$, and uniform absolute convergence on a set $X$ means the finite partial sums of $|c_\alpha (z-a)^\alpha|$, directed by inclusion, converge uniformly on $X$. Mathlib's HasFPowerSeriesOnBall is not used: its balls for the sup norm are equiradial polydiscs only.
• The integral over $\Gamma$ is torusIntegral, whose parametrization $\zeta_k = a_k + \rho_k e^{i\theta_k}$ includes the Jacobian $\prod_k i\rho_k e^{i\theta_k}$ and orients each circle positively. The integrands are continuous on the compact torus, so no integrability hypothesis is needed.
• $\partial/\partial z_k$ is defined from real partial derivatives (deriv along $t \mapsto z_k + t$ and $t \mapsto z_k + it$); $\partial^{|\alpha|}/\partial z^\alpha$ iterates it. $\det D_{\mathbb{R}} f(p)$ is LinearMap.det of the real Fréchet derivative, which is basis independent.
• The Cauchy estimate is stated for every bound $M$ of $|f|$ on $\Gamma$, which is equivalent to the book's $\|f\|_\Gamma$ form.

A complete development needs the one-variable Cauchy integral formula (in Mathlib), iterated circle integrals and torusIntegral, and summation over Fin n → ℕ. The regularity bridge from separate to joint holomorphy and the multi-index power-series API are reusable across the whole series of missions on this book; contributions of either as standalone lemmas are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables, version 4.4, 2026, Chapter 1, §§1.1–1.3. https://www.jirka.org/scv/scv.pdf
• W. F. Osgood, "Note über analytische Functionen mehrerer Veränderlichen", Mathematische Annalen 52 (1899), 462–464.
• L. Hörmander, An Introduction to Complex Analysis in Several Variables, 3rd ed., North-Holland, 1990, Chapter II.

Motivation and history

Compressing an operator to a closed subspace keeps the information visible within that subspace but can discard interactions with its orthogonal complement. The compression-rigidity question asks whether a particular equality detects that no such interactions were present. Its inputs are two commuting positive contractions and an ordinary strictly convex function of two real variables. The issue is the equality case, not the existence of a general operator inequality for every convex function.

The question was contributed by Boris Bilich to the CUHK-Shenzhen AI Math Problems collection and added on June 1, 2026. The original problem asks about operators on a Hilbert space without imposing finite dimension. The first formal target in this mission treated matrices with supplied joint spectral data. That finite-dimensional declaration has a verified proof on Prove2Me, but it does not settle the unrestricted Hilbert-space question. The September 2026 correction restores arbitrary complex Hilbert spaces as the main target and preserves the earlier result as a supporting artifact.

Setting

Let $H$ be a complete complex Hilbert space, and let $\mathcal B(H)$ be its algebra of bounded complex-linear operators. The multiplication $AB$ means composition, with $B$ acting first, and $A^*$ denotes the adjoint. A positive contraction $A$ is self-adjoint, satisfies $\operatorname{Re}\langle v,Av\rangle\geq0$ for every $v\in H$, and has operator norm at most one. Both zero and the identity are permitted.

Write $S=[0,1]^2$. Let $X,Y\in\mathcal B(H)$ be positive contractions satisfying $XY=YX$. Their joint continuous functional calculus assigns an operator $g(X,Y)$ to each continuous real function $g$ on $S$. It is characterized as a continuous unital real star-algebra homomorphism from $C(S,\mathbb R)$ to $\mathcal B(H)$ that maps the two coordinate functions to $X$ and $Y$. The domain has the uniform norm and the codomain the operator norm. The existence and uniqueness of this calculus follow from the standard joint spectral theorem; the relevant source is Dereziński, Lemma 6.6, printed page 43.

An orthogonal projection is an operator $P$ satisfying $P^*=P$ and $P^2=P$. The compressed operators $PXP$ and $PYP$ are still viewed as operators on the original space $H$, not as operators on a separately chosen finite-dimensional range. The question includes the additional hypothesis that these compressed operators commute. The original commutation of $X$ and $Y$ does not remove the need to state this hypothesis.

Formalization targets

The main target is the entire compression implication from the source. Let $f:S\to\mathbb R$ be continuous and strictly convex: for distinct $x,y\in S$ and $0<t<1$, its value at $tx+(1-t)y$ is strictly less than $t f(x)+(1-t)f(y)$. For $X,Y,P$ as above, the question is whether

$$P f(X,Y)P=P f(PXP,PYP)P \quad\Longrightarrow\quad PX=XP\ \text{and}\ PY=YP.$$

Both outer projections on the right are part of the original assertion. There is no hypothesis that $f(0,0)=0$. Commutation of $P$ with each coordinate operator is exactly the reducing-subspace conclusion asked for in the source.

The accompanying standard infrastructure target asserts that, for every commuting pair of positive contractions on $H$,

$$\exists!\,\Phi:C(S,\mathbb R)\longrightarrow\mathcal B(H),\qquad \Phi(x\mapsto x_0)=X,\quad\Phi(x\mapsto x_1)=Y,$$

where $\Phi$ is continuous, unital, real-linear, multiplicative and star-preserving. This is the unit-square, real-valued-function specialization of Lemma 6.6, not a claim that this known theorem is a new research conjecture. Its Lean proof is a separate supporting obligation. The earlier two-dimensional milestone and the proved finite-dimensional capstone remain available; neither replaces the new main target.

Significance

A positive resolution would show that exact preservation of one strictly convex functional-calculus value, under the specified commuting-compression hypothesis, forces both operators to preserve the projection's range and its orthogonal complement. A negative resolution would require an actual Hilbert space, operators and strictly convex function satisfying every hypothesis while at least one of the two reducing identities fails.

The formal development separates this research question from the standard spectral infrastructure needed to express it. The new main declaration is an open proof obligation. The joint-calculus existence-and-uniqueness declaration is also unproved in this contribution, although mathematically standard. Local compilation and server publication check the declarations' well-formedness; they are not proofs of either statement. Only the earlier finite-dimensional result is being reported here as already proved.

Difficulty

Arbitrary bounded commuting self-adjoint operators need not have a joint eigenbasis. Consequently a matrix formulation that records finitely many joint spectral atoms cannot serve as the general operator model. The compressed pair may also have different spectral data from the original pair. The equality involves these two different functional calculi, with a projection on either side of each value.

Strict convexity in this question is ordinary scalar strict convexity on the square. Operator convexity, finite rank of the projection, compactness of the coordinate operators, and a multivariable operator Jensen inequality are not additional assumptions. Introducing any of them would change the requested question. The general formulation must also retain boundary cases rather than exclude them to simplify an argument.

Formalization scope

The Lean model uses actual bounded complex-linear maps on an arbitrary complete inner-product space. It imposes no finite-dimensionality, separability, common-eigenbasis or nonzero-space assumption. It includes $P=0$, $P=I_H$ and the zero Hilbert space. The scalar field convention is complex; a real-Hilbert-space transfer is not separately formalized here.

The function is stored on the ambient real plane, but continuity, strict convexity and evaluation use only its restriction to $S$. Values outside $S$ are irrelevant, and continuity outside the square is not required. Thus storing an ambient function does not exclude any continuous function originally defined only on the square.

Joint evaluation is a total definition. If a representing continuous unital real star-algebra homomorphism exists, it chooses one for the operator pair and then evaluates the supplied function. Otherwise it returns zero. The separate existence-and-uniqueness target establishes that this fallback is inapplicable to commuting positive contractions and that the choice is immaterial. No field in the model assumes the compression-rigidity conclusion. The supporting standard theorem must also apply to the compressed pair using the original projection and positivity hypotheses, without adding representation existence as a new restriction on the main question.

The replacement definition and both statements were built at Lean 4.30.0 with supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, and their final versions received independent blind readbacks. Published older declarations and their proof identities are preserved. They should be cited with their finite-dimensional scope, not described as a solution of the arbitrary-Hilbert-space target.

Selected references

• Boris Bilich, Equality case for compressed convex functional calculus, CUHK-Shenzhen AI Math Problems, Problem 2, added June 1, 2026. Original statement.
• Jan Dereziński, Bounded operators, Warsaw University lecture notes, January 2007, Lemma 6.6, printed page 43. Joint continuous functional calculus.

Motivation

A holomorphic function on an open set of $\mathbb{C}^n$ restricts to a real hypersurface $M$ as a function that satisfies the tangential Cauchy–Riemann equations: it is annihilated by every antiholomorphic vector tangent to $M$. Functions on $M$ with this property are called CR functions, and they are the boundary values that several complex variables studies whenever a domain is approached through its boundary. The basic question is the converse: when is a CR function locally the restriction of a holomorphic function? For smooth data the answer is "not always" (the book's Example 3.2.7 gives a smooth CR function on the hyperplane $\operatorname{Im} z_2 = 0$ that is no such restriction). For real-analytic data the answer is "always", and that is Severi's theorem, the goal of this mission.

The mission follows Chapter 3 of Jiří Lebl's open textbook Tasty Bits of Several Complex Variables (version 4.4, 2026), where Severi's theorem is proved by complexification: a real-analytic function of $z$ and $\bar z$ is treated as a holomorphic function of two independent variables $(z, \zeta)$ restricted to the diagonal $\zeta = \bar z$. The milestones are the steps of that route: uniqueness on totally real slices, the two complexification propositions, the fact that restrictions of holomorphic functions are CR, and the normal form $\bar w = \Phi(z, \bar z, w)$ of a real-analytic hypersurface.

Setting

Write $\mathbb{C}^n \cong \mathbb{R}^{2n}$ with $z_k = x_k + i y_k$. A function on an open subset of $\mathbb{R}^N$ is real-analytic if near each point it equals a convergent power series in the real coordinates. A set $M \subset \mathbb{C}^n$ is a real-analytic hypersurface if near each of its points, after choosing one real coordinate $y$ among the $2n$ and collecting the other $2n-1$ as $x$, it is the graph $y = \varphi(x)$ of a real-analytic function $\varphi$.

A function $f$ on an arbitrary set $X \subset \mathbb{C}^n$ is smooth (respectively real-analytic) if near each point of $X$ it agrees on $X$ with a smooth (respectively real-analytic) function $F$ defined on an open neighbourhood. A defining function of $M$ at $p$ is a smooth real function $r$ on an open $V \ni p$ with nonvanishing derivative and $M \cap V = \{r = 0\}$; $M$ is a smooth real hypersurface if it has one at every point.

With the Wirtinger derivative $\partial/\partial\bar z_k = \tfrac12(\partial/\partial x_k + i\,\partial/\partial y_k)$, the space of antiholomorphic tangent vectors of $M$ at $p$ is

$$T^{(0,1)}_p M = \Big\{ \textstyle\sum_{k} a_k \frac{\partial}{\partial \bar z_k}\big|_p : \sum_k a_k \frac{\partial r}{\partial \bar z_k}(p) = 0 \Big\}.$$

A smooth $f : M \to \mathbb{C}$ is a CR function if $X_p f = 0$ for all $p \in M$ and $X_p \in T^{(0,1)}_pM$, where $X_p f$ is computed on any smooth local extension of $f$. A real-analytic CR function is a CR function that is real-analytic on $M$.

In Lean, $\mathbb{C}^n$ is Fin n → ℂ, and these notions are the definitions IsRealAnalyticOn, IsRealAnalyticHypersurface, IsSmoothHypersurface, IsSmoothOnSet / IsRealAnalyticOnSet, antiholTangent and IsSmoothCRFunction / IsRealAnalyticCRFunction of the namespace LeblSCV.CR.

Formalization targets

Goal: Severi's theorem (Theorem 3.2.9)

Let $M \subset \mathbb{C}^n$ be a real-analytic hypersurface, $p \in M$, and $f : M \to \mathbb{C}$ a real-analytic CR function. Then there are an open neighbourhood $U$ of $p$ and $F \in \mathcal{O}(U)$ with

$$F(q) = f(q) \qquad \text{for all } q \in M \cap U.$$

Milestones

1. Lemma 3.1.2. Holomorphic functions on a domain $V \subset \mathbb{C}^n$ that agree on $V \cap \mathbb{R}^n \neq \emptyset$ agree on $V$.
2. Proposition 3.1.3. A real-analytic function on a domain $U \subset \mathbb{R}^n$ extends to a unique holomorphic function on some domain $V \supset U$ of $\mathbb{C}^n$.
3. Lemma 3.1.4. Holomorphic functions on a domain $V \subset \mathbb{C}^n \times \mathbb{C}^n$ that agree on $V \cap \{\zeta = \bar z\} \neq \emptyset$ agree on $V$.
4. Proposition 3.1.5. A real-analytic $f$ on a domain $U \subset \mathbb{C}^n$ has a unique holomorphic $F$ on a domain $V \supset \{(z, \bar z) : z \in U\}$ with $F(z, \bar z) = f(z)$.
5. Proposition 3.2.6. The restriction of a holomorphic function to a smooth (respectively real-analytic) hypersurface is a smooth (respectively real-analytic) CR function.
6. Proposition 3.2.8. After a translation and a unitary rotation taking $p$ to $0$, a real-analytic hypersurface is locally $\bar w = \Phi(z, \bar z, w)$ with $\Phi$ holomorphic, $\Phi$, $\partial\Phi/\partial z_k$, $\partial\Phi/\partial\zeta_k$ vanishing at $0$, and $w = \bar\Phi(\zeta, z, \Phi(z, \zeta, w))$.

Significance

Severi's theorem identifies the real-analytic CR functions on a real-analytic hypersurface with the local traces of holomorphic functions. Together with Proposition 3.2.6 it shows that, in the real-analytic category, the tangential Cauchy–Riemann equations are exactly the obstruction to holomorphic extension. It is the model for the later extension theorems of the chapter: the Baouendi–Trèves approximation theorem (Theorem 3.3.1) and the Lewy extension theorem (Theorem 3.4.1), which replace real-analyticity with smoothness and pay for it with one-sided extension or approximation. Complexification (Propositions 3.1.3 and 3.1.5) is also a tool in its own right, used for the composition of real-analytic maps (Proposition 3.1.10) and for pluriharmonic functions.

All results here are classical and proved in the book; none of them is formalized in Lean or Mathlib as far as a search of the Prove2Me corpus and Mathlib shows. Mathlib has real and complex analyticity (AnalyticOnNhd), the one-variable and several-variable identity theorems for analytic functions, and the holomorphic implicit function theorem is within reach, but it has no notion of real hypersurface, CR vector or CR function. The mission produces that layer and a checked proof of the first extension theorem for CR functions.

Difficulty

The obvious idea is to take a real-analytic extension of $f$, complexify it to a holomorphic function $f(z, w, \zeta, \omega)$ of $2n$ variables, and substitute $\omega = \Phi(z, \zeta, w)$ to remove $\bar w$. That produces a holomorphic function of $(z, w, \zeta)$, not of $(z, w)$; showing that it does not depend on $\zeta$ requires transporting the CR equations, which hold only on $M$, to the whole complexified hypersurface. That transport is a uniqueness statement for the complexification, and it rests on the normal form of Proposition 3.2.8, itself an application of the holomorphic implicit function theorem to the complexified defining function together with its reality symmetry. On the Lean side, the diagonal $\{\zeta = \bar z\}$ is not a complex submanifold, so identity theorems along it (Lemmas 3.1.2 and 3.1.4) do not follow from the standard identity theorem for open sets.

Formalization scope

• $\mathbb{C}^n$ is Fin n → ℂ, with 0-based indices; $\mathbb{C}^n \times \mathbb{C}^n$ is the product type. The sup norm of Fin n → ℂ never enters a statement: no ball, norm or distance occurs.
• Holomorphic on an open set is DifferentiableOn ℂ, which is equivalent to the book's Definition 1.1.2 there. A domain is an open connected (hence nonempty) set.
• Real-analytic is Mathlib's AnalyticOnNhd ℝ on an open set, applied to $\mathbb{C}^n$ as a real vector space, which is the book's power series in $x, y$ (equivalently in $z, \bar z$).
• A real-analytic hypersurface is a local graph over one of the $2n$ real coordinates (Definition 3.1.9), not the zero set of a real-analytic function.
• Functions on $M$ are functions on $\mathbb{C}^n$ of which only the values on $M$ are read. "Smooth on $M$" means locally the restriction of a $C^\infty$ function (Definition 3.2.1). The CR condition is imposed for every defining function and every smooth local extension, which is equivalent to one choice because both are independent of the choice.
• Proposition 3.2.8 is stated for $n = m + 1$, with the unitary change of coordinates $q \mapsto U(q - p)$ and every "near the origin" made an explicit open set. Only its displayed statement is a target; the remarks that follow it on the page are not.
• The goal cannot be satisfied by an empty hypothesis: real-analytic hypersurfaces exist (a sorry-free check shows $\{\operatorname{Im} z_1 = 0\}$ qualifies), and by Proposition 3.2.6 every restriction of a holomorphic function is a real-analytic CR function. The CR condition is the intrinsic one on $T^{(0,1)}_pM$; replacing it with "restriction of a holomorphic function" would make the goal a tautology and is ruled out.
• Needed infrastructure: the several-variable identity theorem, holomorphic implicit functions, power series in $2n$ variables, and the chain rule for Wirtinger derivatives. The definitions of real-analytic hypersurface and CR function are reusable by the later extension theorems of Chapter 3. Contributions of any milestone, of a proof that $T^{(0,1)}_pM$ is independent of the defining function, or of Exercise 3.2.3 (independence of the extension) are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables, version 4.4, 2026, Chapter 3. https://www.jirka.org/scv/
• Mathlib documentation, Mathlib.Analysis.Analytic.Basic (analytic functions, AnalyticOnNhd). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Analytic/Basic.html