Skip to content

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
LeanWeierstrassCurve.Affine.NumberField.weakBSD · WeierstrassCurve.Affine.NumberField.strongBSD · WeierstrassCurve.Affine.Rat.weakBSD · WeierstrassCurve.Affine.Rat.strongBSD

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 → ℝ^n denotes the initial velocity, while v : ℝ^n → ℝ → ℝ^n denotes the solution velocity. The curried order v x t, p x t, and f x t keeps 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 derivWithin relative to Set.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.

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.

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.

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.

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
LeanNavierStokes.navier_stokes_existence_and_smoothness_R3 · NavierStokes.navier_stokes_existence_and_smoothness_periodic · NavierStokes.navier_stokes_breakdown_R3 · NavierStokes.navier_stokes_breakdown_periodic

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
LeanPoincareConjecture.poincare_conjecture · PoincareConjecture.poincare_conjecture.variants.dimension_two · PoincareConjecture.poincare_conjecture.variants.dimension_ge_five · PoincareConjecture.poincare_conjecture.variants.dimension_four · PoincareConjecture.poincare_conjecture.variants.smooth_for_three · PoincareConjecture.poincare_conjecture.variants.smooth_implication · PoincareConjecture.poincare_conjecture.variants.smooth_known_cases · PoincareConjecture.poincare_conjecture.variants.smooth_dimension_four · PoincareConjecture.poincare_conjecture.variants.smooth_other_cases

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
LeanComplexityTheory.P_ne_NP · ComplexityTheory.NP_ne_coNP · ComplexityTheory.P_eq_BPP · ComplexityTheory.coP_eq_P · ComplexityTheory.P_subset_NP · ComplexityTheory.P_subset_coNP · ComplexityTheory.P_subset_BPP

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.dedekindZeta is the naive Dirichlet series (LSeries), not a meromorphic continuation; outside the region of absolute convergence tsum returns junk 0, 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 RiemannHypothesis type 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
LeanRiemannHypothesis.riemannHypothesis · GRH.generalized_riemann_hypothesis

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.