Millennium problems
The 5 problem files in FormalConjectures/Millennium that state a research or textbook statement, at commit 2055e5ad, one article each.
Their docstrings and Lean statements are quoted from Formal Conjectures (Google DeepMind) at that commit, under its Apache-2.0 license.
TheoremThe Birch and Swinnerton-Dyer (BSD) Conjecture#
References
- The Clay Institute, official problem description by Andrew Wiles: claymath.org
- [BSD1965] B. J. Birch and H. P. F. Swinnerton-Dyer. "Notes on elliptic curves. II." Journal fur die reine und angewandte Mathematik 218 (1965), 79-108, doi
- [Tate1966] John Tate. "On the conjectures of Birch and Swinnerton-Dyer and a geometric analog." Seminaire Bourbaki, Vol. 9, Exp. No. 306 (1966), 415-440, numdam
- [Gross2011] Benedict H. Gross. "Lectures on the conjecture of Birch and Swinnerton-Dyer." Arithmetic of L-functions, IAS/Park City Math. Ser. 18, AMS (2011), 169-209, math.harvard.edu
- [Ang2025] David Kurniadi Angdinata. "L-functions of Dirichlet twists of elliptic curves: computations and congruences." PhD thesis, University College London (2025), discovery.ucl.ac.uk
- [Ada] Tom Adamczewski. "Autoformalized conjectures", Birch and Swinnerton-Dyer
- [DD2010] Tim Dokchitser and Vladimir Dokchitser. "On the Birch-Swinnerton-Dyer quotients modulo squares." Annals of Mathematics 172 (2010), 567-596, Conjecture 2.1, annals
Quoted from FormalConjectures/Millennium/BSD.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 4 research or textbook statements: 4 open. It also has 1 API statement, counted here but not shown.
WeierstrassCurve.Affine.NumberField.weakBSD
Open: stated without proof.
The weak Birch and Swinnerton-Dyer conjecture ([DD2010], Conjecture 2.1 (1); the order statement on its own is [Tate1966], Conjecture (A)).
theorem weakBSD [E.IsElliptic] : WeakBSD E
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Millennium/BSD.lean, line 91.
WeierstrassCurve.Affine.NumberField.strongBSD
Open: stated without proof.
The strong Birch and Swinnerton-Dyer conjecture ([DD2010], Conjecture 2.1).
theorem strongBSD [E.IsElliptic] : StrongBSD E
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Millennium/BSD.lean, line 96.
WeierstrassCurve.Affine.Rat.weakBSD
Open: stated without proof.
The weak Birch and Swinnerton-Dyer conjecture over
ℚ, a Clay Millennium Prize Problem.
theorem weakBSD : NumberField.WeakBSD E
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Millennium/BSD.lean, line 113.
WeierstrassCurve.Affine.Rat.strongBSD
Open: stated without proof.
The strong Birch and Swinnerton-Dyer conjecture over
ℚ.
theorem strongBSD : NumberField.StrongBSD E
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Millennium/BSD.lean, line 118.
Sources
TheoremExistence And Smoothness Of The Navier–Stokes Equation#
This file formalizes the Clay Mathematics Institute millennium problem concerning the existence and smoothness of solutions to the Navier-Stokes equations in three spatial dimensions. While the definitions are generalized to arbitrary dimension n, the millennium problem specifically concerns the case n = 3.
References
Main Theorems (Clay Millennium Problem for n = 3)
The Clay Millennium Problem asks for a proof of one of the following four statements:
navier_stokes_existence_and_smoothness_R3: (A) Global existence on ℝ³navier_stokes_existence_and_smoothness_periodic: (B) Global existence on ℝ³/ℤ³navier_stokes_breakdown_R3: (C) Existence of breakdown scenario on ℝ³navier_stokes_breakdown_periodic: (D) Existence of breakdown scenario on ℝ³/ℤ³In September 2026, an internal OpenAI model proved alternatives (C) and (D) by constructing solutions that develop finite-time singularities under smooth forcing.
Variable conventions
Fefferman writes the velocity as \(u(x,t)\), the initial velocity as \(u^\circ(x)\), the pressure as \(p(x,t)\), the force as \(f(x,t)\), and the viscosity as \(\nu\). In Lean,
u₀ : ℝ^n → ℝ^ndenotes the initial velocity, whilev : ℝ^n → ℝ → ℝ^ndenotes the solution velocity. The curried orderv x t,p x t, andf x tkeeps the source convention that position comes before time.Since the Clay statement gives equation (1) on the closed time half-line \(t \ge 0\), the time derivative is encoded with
derivWithinrelative toSet.Ici 0. The Clay PDF also includes errata; in particular, we include spatial 1-periodicity of the pressure in the periodic case. The sign correction to the weak-solution identity in the errata is not represented here, since this file formalizes the four prize alternatives rather than the later weak-solution discussion.
Quoted from FormalConjectures/Millennium/NavierStokes.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 4 research or textbook statements: 2 open and 2 solved. It also has 5 API statements, counted here but not shown.
NavierStokes.navier_stokes_existence_and_smoothness_R3
Open: stated without proof.
(A) Existence and smoothness of (unforced) Navier–Stokes solutions on ℝ³.
theorem navier_stokes_existence_and_smoothness_R3 (nu : ℝ) (hnu : nu > 0)
(u₀ : ℝ³ → ℝ³) (hu₀ : InitialVelocityConditionDecay u₀) :
∃ v p, NavierStokesExistenceAndSmoothnessRn nu u₀ (f := 0) v p
Category research open; AMS 35 Partial differential equations. Declared in FormalConjectures/Millennium/NavierStokes.lean, line 274.
NavierStokes.navier_stokes_existence_and_smoothness_periodic
Open: stated without proof.
(B) Existence and smoothness of (unforced) Navier–Stokes solutions in ℝ³/ℤ³.
theorem navier_stokes_existence_and_smoothness_periodic (nu : ℝ) (hnu : nu > 0)
(u₀ : ℝ³ → ℝ³) (hu₀ : InitialVelocityConditionPeriodic u₀) :
∃ v p, NavierStokesExistenceAndSmoothnessPeriodic nu u₀ (f := 0) v p
Category research open; AMS 35 Partial differential equations. Declared in FormalConjectures/Millennium/NavierStokes.lean, line 281.
NavierStokes.navier_stokes_breakdown_R3
Solved: stated here; a Lean proof is at https://github.com/openai/NavierStokesAndEuler/commit/8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538.
(C) Breakdown of (forced) Navier–Stokes solutions on ℝ³.
This was proven by an internal OpenAI model in September 2026.
theorem navier_stokes_breakdown_R3 (nu : ℝ) (hnu : nu > 0) :
∃ (u₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³),
InitialVelocityConditionDecay u₀ ∧ ForceConditionDecay f ∧
¬ (∃ v p, NavierStokesExistenceAndSmoothnessRn nu u₀ f v p)
Category research solved; AMS 35 Partial differential equations. Declared in FormalConjectures/Millennium/NavierStokes.lean, line 295.
NavierStokes.navier_stokes_breakdown_periodic
Solved: stated here; a Lean proof is at https://github.com/openai/NavierStokesAndEuler/commit/8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538.
(D) Breakdown of (forced) Navier–Stokes solutions on ℝ³/ℤ³.
This was proven by an internal OpenAI model in September 2026.
theorem navier_stokes_breakdown_periodic (nu : ℝ) (hnu : nu > 0) :
∃ (u₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³),
InitialVelocityConditionPeriodic u₀ ∧ ForceConditionPeriodic f ∧
¬ (∃ v p, NavierStokesExistenceAndSmoothnessPeriodic nu u₀ f v p)
Category research solved; AMS 35 Partial differential equations. Declared in FormalConjectures/Millennium/NavierStokes.lean, line 310.
Sources
TheoremThe Poincaré Conjecture#
References: - Miln2022 - Wang2017. - mo296171 - mathlib4
The formalisations in this file are based on the ones written by Junyan Xu in Mathlib4.
Quoted from FormalConjectures/Millennium/Poincare.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 9 research or textbook statements: 2 open, 2 solved and 5 textbook results.
PoincareConjecture.poincare_conjecture
Solved: stated here without proof.
The Millennium Problem, solved by Grigori Perelman in 2003: the Poincaré Conjecture holds.
theorem poincare_conjecture : ConjectureFor 3
Category research solved; AMS 54 General topology, 57 Manifolds and cell complexes. Declared in FormalConjectures/Millennium/Poincare.lean, line 52.
PoincareConjecture.poincare_conjecture.variants.dimension_two
Textbook result, stated without proof.
The Generalized Poincaré Conjecture holds for surfaces.
theorem poincare_conjecture.variants.dimension_two : ConjectureFor 2
Category textbook; AMS 54 General topology, 57 Manifolds and cell complexes. Declared in FormalConjectures/Millennium/Poincare.lean, line 59.
PoincareConjecture.poincare_conjecture.variants.dimension_ge_five
Textbook result, stated without proof.
The Generalized Poincaré Conjecture holds for dimensions at least 5.
theorem poincare_conjecture.variants.dimension_ge_five (n : ℕ) (hn : 5 ≤ n) : ConjectureFor n
Category textbook; AMS 54 General topology, 57 Manifolds and cell complexes. Declared in FormalConjectures/Millennium/Poincare.lean, line 66.
PoincareConjecture.poincare_conjecture.variants.dimension_four
Textbook result, stated without proof.
The Generalized Poincaré Conjecture holds in dimension 4.
theorem poincare_conjecture.variants.dimension_four : ConjectureFor 4
Category textbook; AMS 54 General topology, 57 Manifolds and cell complexes. Declared in FormalConjectures/Millennium/Poincare.lean, line 73.
PoincareConjecture.poincare_conjecture.variants.smooth_for_three
Textbook result, stated without proof.
A reformulation of the Millennium Problem in terms of smooth 3-folds.
theorem poincare_conjecture.variants.smooth_for_three : SmoothConjectureFor 3
Category textbook; AMS 54 General topology, 57 Manifolds and cell complexes. Declared in FormalConjectures/Millennium/Poincare.lean, line 87.
PoincareConjecture.poincare_conjecture.variants.smooth_implication
Textbook result, stated without proof.
The smooth formulation of the Millennium Problem implies the general case. This follows from the fact that every topological 3-fold admits a smooth structure [mo296171].
theorem poincare_conjecture.variants.smooth_implication (H : SmoothConjectureFor 3) :
ConjectureFor 3
Category textbook; AMS 54 General topology, 57 Manifolds and cell complexes. Declared in FormalConjectures/Millennium/Poincare.lean, line 93.
PoincareConjecture.poincare_conjecture.variants.smooth_known_cases
Solved: stated here without proof.
The smooth version of the Poincaré conjecture is known to hold in dimensions \(1, 2, 3, 5, 6, 12, 56, 61\). See [Wang2017].
theorem poincare_conjecture.variants.smooth_known_cases (n : ℕ) (hn : n ∈ SmoothTrueValues) :
SmoothConjectureFor n
Category research solved; AMS 54 General topology, 57 Manifolds and cell complexes. Declared in FormalConjectures/Millennium/Poincare.lean, line 103.
PoincareConjecture.poincare_conjecture.variants.smooth_dimension_four
Open: stated without proof.
The four dimensional case of the smooth version of the conjecture is still open. See [Wang2017].
theorem poincare_conjecture.variants.smooth_dimension_four : SmoothConjectureFor 4
Category research open; AMS 54 General topology, 57 Manifolds and cell complexes. Declared in FormalConjectures/Millennium/Poincare.lean, line 110.
PoincareConjecture.poincare_conjecture.variants.smooth_other_cases
Open: stated without proof.
It is conjectured that the only values of \(n > 4\) for which the smooth version of the conjecture holds are \(n = 5, 6, 12, 56, 61\). See Conjecture 1.17 in [Wang2017].
theorem poincare_conjecture.variants.smooth_other_cases (n : ℕ) (hn : n > 4)
(hn' : n ∉ SmoothTrueValues) : ¬ SmoothConjectureFor n
Category research open; AMS 54 General topology, 57 Manifolds and cell complexes. Declared in FormalConjectures/Millennium/Poincare.lean, line 116.
Sources
TheoremConjectures in Complexity Theory#
This file contains formal statements of some of the main open conjectures in complexity theory, including
- the P vs NP problem
- the NP vs coNP problem
- the P vs BPP problem
References: - Wikipedia - The Clay Institute
Quoted from FormalConjectures/Millennium/PvsNP.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 7 research or textbook statements: 3 open and 4 textbook results.
ComplexityTheory.P_ne_NP
Open: stated without proof.
P ≠ NP:
The conjecture that the complexity classes P and NP are not equal.
theorem P_ne_NP : P ≠ NP
Category research open; AMS 68 Computer science. Declared in FormalConjectures/Millennium/PvsNP.lean, line 45.
ComplexityTheory.NP_ne_coNP
Open: stated without proof.
NP ≠ coNP:
The conjecture that the complexity classes NP and coNP are not equal.
theorem NP_ne_coNP : NP ≠ coNP
Category research open; AMS 68 Computer science. Declared in FormalConjectures/Millennium/PvsNP.lean, line 53.
ComplexityTheory.P_eq_BPP
Open: stated without proof.
P = BPP:
The conjecture that the complexity classes P and BPP are equal.
theorem P_eq_BPP : P = BPP
Category research open; AMS 68 Computer science. Declared in FormalConjectures/Millennium/PvsNP.lean, line 61.
ComplexityTheory.coP_eq_P
Textbook result, stated without proof.
The theorem that the set of complements of languages in P is itself P.
This can be proven by observing that the boolean negation function is computable in polynomial time, and that compositions of poly-time computable functions are also poly-time computable.
theorem coP_eq_P :
{ L | Lᶜ ∈ P } = P
Category textbook; AMS 68 Computer science. Declared in FormalConjectures/Millennium/PvsNP.lean, line 70.
ComplexityTheory.P_subset_NP
Textbook result, stated without proof. A Lean proof is at https://github.com/AItoBit/p-subset-np/blob/beaeee15c37af6efac518426e117861c00ff3acc/PSubsetNP.lean#L358.
The theorem that P is a subset of NP.
This can be proven by observing that for any language in P, we can construct a verifier that ignores the witness and simply runs the poly-time decider for the language.
theorem P_subset_NP :
P ⊆ NP
Category textbook; AMS 68 Computer science. Declared in FormalConjectures/Millennium/PvsNP.lean, line 83.
ComplexityTheory.P_subset_coNP
Textbook result, proved here.
The theorem that P is a subset of coNP.
theorem P_subset_coNP :
P ⊆ coNP
Category textbook; AMS 68 Computer science. Declared in FormalConjectures/Millennium/PvsNP.lean, line 91.
ComplexityTheory.P_subset_BPP
Textbook result, stated without proof.
The theorem that P is a subset of BPP.
This can be proven by observing that for any language in P, we can construct a randomized decider that ignores the random bits and simply runs the poly-time decider for the language.
theorem P_subset_BPP :
P ⊆ BPP
Category textbook; AMS 68 Computer science. Declared in FormalConjectures/Millennium/PvsNP.lean, line 106.
Sources
TheoremRiemann Hypothesis and its generalizations#
The Riemann Hypothesis asserts that all non-trivial zeros of the Riemann zeta function \(\zeta(s)\) have real part \(\frac{1}{2}\). The trivial zeros are the negative even integers \(-2, -4, -6, \ldots\). The hypothesis is one of the seven Millennium Prize Problems posed by the Clay Mathematics Institute.
The Generalized Riemann Hypothesis extends this to Dirichlet \(L\)-functions of primitive Dirichlet characters.
Note: the Extended Riemann Hypothesis (ERH) for Dedekind zeta functions is intentionally not stated here. Mathlib's
NumberField.dedekindZetais the naive Dirichlet series (LSeries), not a meromorphic continuation; outside the region of absolute convergencetsumreturns junk0, producing spurious zeros that make the naive foramlisation of the conjecture provably false. The ERH should be added once Mathlib provides a meromorphic continuation of the Dedekind zeta function.References: - The Clay Institute - Wikipedia: Riemann hypothesis - Wikipedia: Generalized Riemann hypothesis - Wikipedia: Dedekind zeta function - J. Neukirch, Algebraic Number Theory, Springer (Grundlehren 322), 1999, Chapter VII, §5. - D. A. Marcus, Number Fields, Springer (GTM 81), 1977, Chapter VII.
Quoted from FormalConjectures/Millennium/RiemannHypothesis.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 2 research or textbook statements: 2 open. It also has 1 test statement, counted here but not shown.
RiemannHypothesis.riemannHypothesis
Open: stated without proof.
The Riemann Hypothesis: all non-trivial zeros of the Riemann zeta function have real part \(\frac{1}{2}\). That is, if \(\zeta(s) = 0\), \(s \neq 1\), and \(s\) is not a trivial zero \(-2(n+1)\) for some \(n \in \mathbb{N}\), then \(\operatorname{Re}(s) = \frac{1}{2}\).
This is the official Millennium Prize Problem as posed by the Clay Mathematics Institute.
This uses the
RiemannHypothesistype from Mathlib, which is defined as∀ (s : ℂ), riemannZeta s = 0 → (¬∃ n : ℕ, s = -2 * (n + 1)) → s ≠ 1 → s.re = 1 / 2.
theorem riemannHypothesis : RiemannHypothesis
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Millennium/RiemannHypothesis.lean, line 61.
GRH.generalized_riemann_hypothesis
Open: stated without proof.
The Generalized Riemann Hypothesis asserts that all the non-trivial zeros of the Dirichlet \(L\)-function \(L(\chi, s)\) of a primitive Dirichlet character \(\chi\) have real part \(\frac{1}{2}\).
theorem generalized_riemann_hypothesis (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q)
(hχ : χ.IsPrimitive) (s : ℂ) (hs : χ.LFunction s = 0)
(hs_nontrivial : s ∉ Int.cast '' trivialZeros χ) :
s.re = 1 / 2
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Millennium/RiemannHypothesis.lean, line 83.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.