Elliott–Halberstam conjecture to Gap conjecture
TheoremElliott–Halberstam conjecture#
References: - Wikipedia - [EH68] Elliott, Peter D. T. A. and Halberstam, Heini, A conjecture in prime number theory, Symposia Mathematica, Vol. IV (INDAM, Rome, 1968/69), 59–72. - [FG89] Friedlander, John and Granville, Andrew, Limitations to the equi-distribution of primes I, Ann. of Math. (2) 129 (1989), no. 2, 363–382.
Quoted from FormalConjectures/Wikipedia/ElliottHalberstamConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 1 open and 2 solved.
ElliottHalberstamConjecture.elliott_halberstam
Open: stated without proof.
The Elliott–Halberstam conjecture: for every \(\theta < 1\) and \(A > 0\) there exists a constant \(C > 0\) such that
\[\sum_{1 \le q \le x^{\theta}} E(x; q) \le \frac{C x}{\log^A x}\]for all \(x > 2\).
theorem elliott_halberstam (θ : ℝ) (hθ : θ < 1) (A : ℝ) (hA : 0 < A) :
∃ C > (0 : ℝ), ∀ x : ℕ, 2 < x →
∑ q ∈ Finset.Icc 1 ⌊(x : ℝ) ^ θ⌋₊, E x q ≤ C * x / Real.log x ^ A
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ElliottHalberstamConjecture.lean, line 57.
ElliottHalberstamConjecture.elliott_halberstam.variants.bombieri_vinogradov
Solved: stated here without proof.
The Bombieri–Vinogradov theorem: the Elliott–Halberstam conjecture holds for every \(\theta < 1/2\). This result may be regarded as an averaged form of the generalized Riemann hypothesis.
theorem elliott_halberstam.variants.bombieri_vinogradov (θ : ℝ) (hθ : θ < 1 / 2) (A : ℝ)
(hA : 0 < A) :
∃ C > (0 : ℝ), ∀ x : ℕ, 2 < x →
∑ q ∈ Finset.Icc 1 ⌊(x : ℝ) ^ θ⌋₊, E x q ≤ C * x / Real.log x ^ A
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ElliottHalberstamConjecture.lean, line 68.
ElliottHalberstamConjecture.elliott_halberstam.variants.friedlander_granville
Solved: stated here without proof.
The Elliott–Halberstam conjecture fails at the endpoint \(\theta = 1\), as shown by Friedlander and Granville [FG89].
theorem elliott_halberstam.variants.friedlander_granville :
¬ ∀ A : ℝ, 0 < A → ∃ C > (0 : ℝ), ∀ x : ℕ, 2 < x →
∑ q ∈ Finset.Icc 1 x, E x q ≤ C * x / Real.log x ^ A
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ElliottHalberstamConjecture.lean, line 79.
Sources
TheoremSome conjectures about ranks of elliptic curves over ℚ#
References: - [PPVW2016] Jennifer Park, Bjorn Poonen, John Voight, and Melanie Matchett Wood. A heuristic for boundedness of ranks of elliptic curves, https://ems.press/journals/jems/articles/16228 - [BS2013] Manjul Bhargava and Arul Shankar. The average size of the 5-Selmer group of elliptic curves is 6, and the average rank is less than 1, https://arxiv.org/pdf/1312.7859 - [Goldfeld1979] Dorian Goldfeld. Conjectures on elliptic curves over quadratic fields, Number Theory Carbondale 1979, Lecture Notes in Math. 751, 108-118, https://doi.org/10.1007/BFb0062705 - [Smith2025] Alexander Smith. The Birch and Swinnerton-Dyer conjecture implies Goldfeld's conjecture, https://arxiv.org/abs/2503.17619 - Wikipedia - ICARM - [Stoll] Michael Stoll. EllipticCurves, a Lean 4 formalization of the Mordell–Weil theorem and explicit 2-descent, https://github.com/MichaelStollBayreuth/EllipticCurves
Quoted from FormalConjectures/Wikipedia/EllipticCurveRank.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 23 research or textbook statements: 12 open, 10 solved and 1 textbook result. It also has 6 test statements and 4 API statements, counted here but not shown.
EllipticCurveRank.mordell_weil
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/e58a03a23e0efb40f891f34d3afceca2ce4ccf9b/FormalConjectures/Wikipedia/EllipticCurveRank.lean#L64.
The rank of an elliptic curve over a number field is always finite by the Mordell–Weil theorem. Consequently, the rank is always finite, so
finrank ℤ E⟮K⟯ = 0really means that the group of rational points is torsion, not that it is of infinite rank.The proof linked via
formal_proofis Michael Stoll's formalization of the Mordell–Weil theorem [Stoll]
theorem mordell_weil {K} [Field K] [NumberField K] [DecidableEq K] (E : Affine K) [E.IsElliptic] :
Module.Finite ℤ E.Point
Category research solved; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 68.
EllipticCurveRank.RatEllipticCurve.card_heightLE_div_pow_five_div_six_tensto
Textbook result, stated without proof.
Formula (5.1.1) of [PPVW2016]: The number of elliptic curves over ℚ with naïve height at most
His asymptotically2^(4/3)*3^(-3/2)/ζ(10) * H^(5/6).
theorem card_heightLE_div_pow_five_div_six_tensto :
atTop.Tendsto (fun H ↦ (heightLE H).ncard / (H : ℝ) ^ (5 / 6 : ℝ))
(𝓝 (2 ^ (4 / 3 : ℝ) * 3 ^ (-3 / 2 : ℝ) / (riemannZeta 10).re))
Category textbook; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 100.
EllipticCurveRank.RatEllipticCurve.half_rank_zero_and_half_rank_one
Open: stated without proof.
Conjecture by Goldfeld and Katz–Sarnak: if elliptic curves over ℚ are ordered by their heights, then 50% of the curves have rank 0 and 50% have rank 1. See p. 28 of https://people.maths.bris.ac.uk/~matyd/BSD2011/bsd2011-Bhargava.pdf.
theorem half_rank_zero_and_half_rank_one (r : ℕ) (hr : r = 0 ∨ r = 1) :
atTop.Tendsto
(fun H ↦ ({E ∈ heightLE H | E.rank = r}.ncard / (heightLE H).ncard : ℝ)) (𝓝 (1 / 2))
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 109.
EllipticCurveRank.RatEllipticCurve.avg_rank_lt_0885
Solved: stated here without proof.
Theorem 3 of [BS2013]: when elliptic curves over ℚ are ordered by height, their average rank is < .885.
theorem avg_rank_lt_0885 :
atTop.limsup (fun H ↦ ((∑ᶠ E : heightLE H, E.1.rank) / (heightLE H).ncard : ℝ)) < 0.885
Category research solved; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 117.
EllipticCurveRank.RatEllipticCurve._08375_le_density_rank_zero_one
Solved: stated here without proof.
Theorem 4 of [BS2013]: when elliptic curves over ℚ are ordered by height, a density of at least 83.75% have rank 0 or 1.
theorem _08375_le_density_rank_zero_one : 0.8375 ≤ atTop.liminf
fun H ↦ ({E ∈ heightLE H | E.rank = 0 ∨ E.rank = 1}.ncard / (heightLE H).ncard : ℝ)
Category research solved; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 125.
EllipticCurveRank.RatEllipticCurve._02062_le_density_rank_zero
Solved: stated here without proof.
Theorem 5 of [BS2013]: when elliptic curves over ℚ are ordered by height, a density of at least 20.62% have rank 0.
theorem _02062_le_density_rank_zero : 0.2062 ≤ atTop.liminf
fun H ↦ ({E ∈ heightLE H | E.rank = 0}.ncard / (heightLE H).ncard : ℝ)
Category research solved; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 132.
EllipticCurveRank.RatEllipticCurve.goldfeld_conjecture
Open: stated without proof.
Goldfeld's conjecture ([Goldfeld1979], Conjecture B), in the form stated in the introduction of [Smith2025]: when the quadratic twists \(E^d\) of an elliptic curve \(E\) over \(\mathbb{Q}\) are ordered by \(|d|\), 50% of them have rank \(0\) and 50% have rank \(1\). See
goldfeld_conjecture.variants.two_lefor the remaining case \(2 \leq r\).Goldfeld states the conjecture for the analytic rank of \(E^d\), which the Birch and Swinnerton-Dyer conjecture predicts is equal to the Mordell–Weil rank used here. Corollary 1.2 of [Smith2025] proves that the Birch and Swinnerton-Dyer conjecture for the quadratic twist family of \(E\) implies Goldfeld's conjecture for \(E\).
theorem goldfeld_conjecture (E : RatEllipticCurve) (r : ℕ) (hr : r = 0 ∨ r = 1) :
atTop.Tendsto
(fun H ↦ ({d ∈ twistIndexLE H | E.twistRank d = r}.ncard / (twistIndexLE H).ncard : ℝ))
(𝓝 (1 / 2))
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 193.
EllipticCurveRank.RatEllipticCurve.goldfeld_conjecture.variants.two_le
Solved: stated here without proof.
Goldfeld's conjecture ([Goldfeld1979], Conjecture B), in the form stated in the introduction of [Smith2025], in the case \(2 \leq r\): a density \(0\) of the quadratic twists \(E^d\) of an elliptic curve \(E\) over \(\mathbb{Q}\) have rank \(r\).
For the Mordell–Weil rank used here this is an unconditional theorem: by Theorem 1.1 of [Smith2025], \(100\%\) of the twists \(E^d\) have \(2^\infty\)-Selmer corank \(0\) or \(1\), and the Mordell–Weil rank is at most the \(2^\infty\)-Selmer corank (equation (1.1) there), so the twists of rank at least \(2\) have density \(0\). The corresponding statement for the analytic rank is open.
theorem goldfeld_conjecture.variants.two_le (E : RatEllipticCurve) (r : ℕ) (hr : 2 ≤ r) :
atTop.Tendsto
(fun H ↦ ({d ∈ twistIndexLE H | E.twistRank d = r}.ncard / (twistIndexLE H).ncard : ℝ))
(𝓝 0)
Category research solved; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 209.
EllipticCurveRank.RatEllipticCurve.goldfeld_conjecture.variants.squarefree
Open: stated without proof.
Goldfeld's conjecture with \(d\) restricted to squarefree integers, which is how it is usually stated informally: 50% of the quadratic twists of \(E\) have rank \(0\) and 50% have rank \(1\). The twist \(E^d\) only depends on the class of \(d\) modulo nonzero rational squares, and the squarefree integers are a system of representatives of these classes. (They need not give pairwise non-isomorphic curves: if \(B = 0\) then \(E^{-d} = E^d\).)
theorem goldfeld_conjecture.variants.squarefree (E : RatEllipticCurve) (r : ℕ)
(hr : r = 0 ∨ r = 1) :
atTop.Tendsto
(fun H ↦ ({d ∈ twistIndexLE H | Squarefree d ∧ E.twistRank d = r}.ncard /
{d ∈ twistIndexLE H | Squarefree d}.ncard : ℝ))
(𝓝 (1 / 2))
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 221.
EllipticCurveRank.RatEllipticCurve.unbounded_rank_conjecture
Open: stated without proof.
From [PPVW2016], Section 3.1: "from the mid-1960s to the present, it seems that most experts conjectured unboundedness."
theorem unbounded_rank_conjecture (n : ℕ) : ∃ E : RatEllipticCurve, n ≤ E.rank
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 232.
EllipticCurveRank.RatEllipticCurve.finite_twentyone_lt_finrank
Open: stated without proof.
From [PPVW2016], Section 8.2: "Our heuristic predicts (a) All but finitely many E ∈ ℰ satisfy rk E(ℚ) ≤ 21". In other words, there are only finitely many elliptic curves over ℚ (up to isomorphism) with rank greater than 21. Notice that this contradicts the previous conjecture.
theorem finite_twentyone_lt_finrank : {E : RatEllipticCurve | 21 < E.rank}.Finite
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 241.
EllipticCurveRank.RatEllipticCurve.rank_height_count_asymptotic
Open: stated without proof.
[PPVW2016] 8.2(b): for 1 ≤ r ≤ 20, the number of elliptic curves over ℚ with rank at least
rand naïve height at mostHis asymptoticallyH ^ ((21 - r) / 24 + o(1)). Note: ℰ_H in 8.2(b) should be ℰ_{≤H}, see the statement of Theorem 7.3.3. Whenr = 1, the exponent is20 / 24 = 5 / 6, which agrees with the exponent incard_heightLE_div_pow_five_div_six_tenstoand is consistent withhalf_rank_zero_and_half_rank_one. The equality is asserted only for largeH, matching theo(1)above: it cannot hold at smallH, becauseheightLE His empty forH ≤ 3(naiveHeight E ≤ 3forcesA = B = 0, which bothΔ_ne_zeroandreducedexclude) and consists only of the two rank-zero curvesy² = x³ ± xfor4 ≤ H ≤ 26, while the right hand side isReal.rpowand hence strictly positive.
theorem rank_height_count_asymptotic (r : ℕ) (h₁ : 1 ≤ r) (h₂ : r ≤ 20) :
∃ f : ℕ → ℝ, atTop.Tendsto f (𝓝 0) ∧
∀ᶠ H : ℕ in atTop,
{E ∈ heightLE H | r ≤ E.rank}.ncard = (H : ℝ) ^ ((21 - r) / 24 + f H)
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 256.
EllipticCurveRank.RatEllipticCurve.twentyone_le_rank_height_count_asymptotic
Open: stated without proof.
[PPVW2016] 8.2(c): the number of elliptic curves over ℚ with rank ≥ 21 and naïve height at most
His asymptotically at mostH ^ o(1).
theorem twentyone_le_rank_height_count_asymptotic :
∃ f : ℕ → ℝ, atTop.Tendsto f (𝓝 0) ∧
∀ H : ℕ, 1 < H → {E ∈ heightLE H | 21 ≤ E.rank}.ncard ≤ (H : ℝ) ^ f H
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 265.
EllipticCurveRank.RatEllipticCurve.exists_rank_ge_thirtyone
Solved: stated here without proof.
Is there an elliptic curve over ℚ of rank at least 31?
The answer is yes: such a curve was found by Claude, Levent Alpöge and Ava Howell in 2026. See https://elliptic-rank.icarm.cloud/curve/302 and
WeierstrassCurve.claudeAlpogeHowell31below.
theorem exists_rank_ge_thirtyone : ∃ E : RatEllipticCurve, 31 ≤ E.rank
Category research solved; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 276.
EllipticCurveRank.RatEllipticCurve.exists_rank_ge_thirtytwo
Open: stated without proof.
Is there an elliptic curve over ℚ of rank at least 32? The largest known rank of an elliptic curve over ℚ as of 2026 is at least 31 (and exactly 31 assuming the generalized Riemann hypothesis and Birch and Swinnerton-Dyer conjecture). See https://elliptic-rank.icarm.cloud/curve/302.
theorem exists_rank_ge_thirtytwo : ∃ E : RatEllipticCurve, 32 ≤ E.rank
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 284.
EllipticCurveRank.WeierstrassCurve.thirtyone_le_rank_claudeAlpogeHowell31
Solved: stated here without proof.
The rank of the Claude–Alpöge–Howell curve is at least 31.
theorem thirtyone_le_rank_claudeAlpogeHowell31 : 31 ≤ finrank ℤ claudeAlpogeHowell31.Point
Category research solved; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 321.
EllipticCurveRank.WeierstrassCurve.rank_claudeAlpogeHowell31
Open: stated without proof.
The rank of the Claude–Alpöge–Howell curve is exactly 31. It has rank exactly 31 assuming the generalized Riemann hypothesis and the Birch and Swinnerton-Dyer conjecture.
theorem rank_claudeAlpogeHowell31 : finrank ℤ claudeAlpogeHowell31.Point = 31
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 329.
EllipticCurveRank.WeierstrassCurve.thirty_le_rank_ranksunbounded30
Solved: stated here without proof.
The rank of the ranksunbounded curve is at least 30.
theorem thirty_le_rank_ranksunbounded30 : 30 ≤ finrank ℤ ranksunbounded30.Point
Category research solved; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 357.
EllipticCurveRank.WeierstrassCurve.rank_ranksunbounded30
Open: stated without proof.
The rank of the ranksunbounded curve is exactly 30.
theorem rank_ranksunbounded30 : finrank ℤ ranksunbounded30.Point = 30
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 362.
EllipticCurveRank.WeierstrassCurve.twentynine_le_rank_elkiesKlagsbrun29
Solved: stated here without proof.
The rank of the Elkies-Klagsbrun curve is at least 29.
theorem twentynine_le_rank_elkiesKlagsbrun29 : 29 ≤ finrank ℤ elkiesKlagsbrun29.Point
Category research solved; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 389.
EllipticCurveRank.WeierstrassCurve.rank_elkiesKlagsbrun29
Open: stated without proof.
The rank of the Elkies-Klagsbrun curve is exactly 29.
theorem rank_elkiesKlagsbrun29 : finrank ℤ elkiesKlagsbrun29.Point = 29
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 394.
EllipticCurveRank.WeierstrassCurve.twentyeight_le_rank_elkies28
Solved: stated here without proof.
The rank of the Elkies curve is at least 28.
theorem twentyeight_le_rank_elkies28 : 28 ≤ finrank ℤ elkies28.Point
Category research solved; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 420.
EllipticCurveRank.WeierstrassCurve.rank_elkies28
Open: stated without proof.
The rank of the Elkies curve is exactly 28.
theorem rank_elkies28 : finrank ℤ elkies28.Point = 28
Category research open; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/EllipticCurveRank.lean, line 425.
Sources
TheoremEmirps#
An emirp is a prime whose decimal reversal is a different prime. It is unknown whether there are infinitely many emirps.
References: * Wikipedia, Emirp * OEIS A006567
Quoted from FormalConjectures/Wikipedia/Emirp.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 8 test statements, counted here but not shown.
Emirp.infinitude_question
Open: stated without proof.
Wikipedia's article on emirps states: "It is not known whether there are infinitely many emirps."
theorem infinitude_question :
{p : ℕ | IsEmirp p}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Emirp.lean, line 79.
Sources
TheoremThe Erdős–Moser equation#
For positive integers \(k\) and \(m\), let
\[S_k(m)=1^k+2^k+\cdots+(m-1)^k.\]The Erdős–Moser conjecture says that \(S_k(m)=m^k\) has only the solution \((k,m)=(1,3)\).
References: * Wikipedia: Erdős–Moser equation * B. C. Kellner, On stronger conjectures that imply the Erdős–Moser conjecture
Quoted from FormalConjectures/Wikipedia/ErdosMoser.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 3 test statements, counted here but not shown.
ErdosMoser.erdos_moser_conjecture
Open: stated without proof.
The only positive solution of \(S_k(m)=m^k\) is \((k,m)=(1,3)\).
theorem erdos_moser_conjecture :
∀ k m : ℕ, 0 < k → 0 < m → powerSum k m = m ^ k → k = 1 ∧ m = 3
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ErdosMoser.lean, line 46.
Sources
TheoremThe Erdős–Ulam problem#
References: * Wikipedia * [Ul60] Ulam, S. M. (1960). A Collection of Mathematical Problems. Interscience, p. 40. * [SdZ10] Solymosi, J. and de Zeeuw, F. (2010). "On a question of Erdős and Ulam." Discrete Comput. Geom. 43, pp. 393--401. arXiv:0806.3095 * [Ta14] Tao, T. (2014). "The Erdős–Ulam problem, varieties of general type, and the Bombieri–Lang conjecture." Blog post, terrytao.wordpress.com * [AE45] Anning, N. H. and Erdős, P. (1945). "Integral distances." Bull. Amer. Math. Soc. 51, pp. 598--600.
Quoted from FormalConjectures/Wikipedia/ErdosUlamProblem.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 1 open and 2 solved. It also has 1 test statement, counted here but not shown.
ErdosUlamProblem.erdos_ulam_problem
Open: stated without proof.
The Erdős–Ulam problem (Ulam 1945).
Is there a dense subset of the plane whose points are at pairwise rational distances? Conjecturally, no such set exists. Solymosi and de Zeeuw [SdZ10] proved that if a rational-distance set has infinitely many points on a line or circle, all but finitely many points lie on that line or circle.
theorem erdos_ulam_problem :
∃ S : Set (EuclideanSpace ℝ (Fin 2)), Dense S ∧ PairwiseRationalDistances S
Category research open; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/ErdosUlamProblem.lean, line 56.
ErdosUlamProblem.erdos_ulam_problem.variants.anning_erdos
Solved: stated here without proof.
Infinite integer-distance sets are collinear (Anning–Erdős 1945).
Anning and Erdős proved that an infinite set of points in the plane with pairwise integer distances must be contained in a line.
Reference: [AE45].
theorem erdos_ulam_problem.variants.anning_erdos
(S : Set (EuclideanSpace ℝ (Fin 2))) (hinf : S.Infinite)
(hd : ∀ p ∈ S, ∀ q ∈ S, ∃ n : ℤ, dist p q = (n : ℝ)) :
∃ a b : EuclideanSpace ℝ (Fin 2), a ≠ b ∧
S ⊆ {x | ∃ t : ℝ, x = a + t • (b - a)}
Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/ErdosUlamProblem.lean, line 82.
ErdosUlamProblem.erdos_ulam_problem.variants.solymosi_de_zeeuw
Solved: stated here without proof.
If a plane set with pairwise rational distances has infinitely many points on a line or circle, all but finitely many of its points are contained in a line or circle. This is the finite-exception corollary of [SdZ10, Theorem 2.2], whose sharper bounds are four exceptions for a line and three for a circle.
theorem erdos_ulam_problem.variants.solymosi_de_zeeuw
(S : Set (EuclideanSpace ℝ (Fin 2))) (hd : PairwiseRationalDistances S)
(hstructure :
(∃ a b : EuclideanSpace ℝ (Fin 2), a ≠ b ∧
{x ∈ S | ∃ t : ℝ, x = a + t • (b - a)}.Infinite) ∨
(∃ (c : EuclideanSpace ℝ (Fin 2)) (ρ : ℝ), 0 < ρ ∧
{x ∈ S | dist x c = ρ}.Infinite)) :
(∃ a b : EuclideanSpace ℝ (Fin 2), a ≠ b ∧
{x ∈ S | ¬ ∃ t : ℝ, x = a + t • (b - a)}.Finite) ∨
(∃ (c : EuclideanSpace ℝ (Fin 2)) (ρ : ℝ), 0 < ρ ∧
{x ∈ S | dist x c ≠ ρ}.Finite)
Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/ErdosUlamProblem.lean, line 96.
Sources
TheoremEuclid Numbers conjecture#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/Euclid.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.
EuclidNumbers.infinite_prime_euclid_numbers
Open: stated without proof.
It is not known whether there is an infinite number of prime Euclid numbers.
theorem infinite_prime_euclid_numbers : {n | (Euclid n).Prime}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Euclid.lean, line 39.
EuclidNumbers.euclid_numbers_are_square_free
Open: stated without proof.
It is not known whether every Euclid number is a square-free number.
theorem euclid_numbers_are_square_free : (∀ n, Squarefree (Euclid n))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Euclid.lean, line 46.
Sources
TheoremOpen questions regarding the existence of Euler bricks#
References: - Wikipedia - stackexchange - [Sh12] Sharipov, Ruslan. Perfect cuboids and irreducible polynomials. https://arxiv.org/abs/1108.5348
Quoted from FormalConjectures/Wikipedia/EulerBrick.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: 5 open and 2 solved.
EulerBrick.perfect_euler_brick_existence
Open: stated without proof.
Is there a perfect Euler brick?
theorem perfect_euler_brick_existence :
∃ a b c : ℕ+, IsPerfectCuboid a b c
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/EulerBrick.lean, line 55.
EulerBrick.four_dim_euler_brick_existence
Open: stated without proof.
Is there an Euler brick in \(4\)-dimensional space?
theorem four_dim_euler_brick_existence :
∃ sides : Fin 4 → ℕ+, IsEulerHyperBrick 4 sides
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/EulerBrick.lean, line 63.
EulerBrick.n_dim_euler_brick_existence
Open: stated without proof.
Is there an Euler brick in \(n\)-dimensional space for any \(n > 3\)?
theorem n_dim_euler_brick_existence :
∀ n > 3, ∃ sides : Fin n → ℕ+, IsEulerHyperBrick n sides
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/EulerBrick.lean, line 71.
EulerBrick.cuboidOne
Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/34c93bbad127a9a5354b9d53478d338eb65edb88/FormalConjectures/Wikipedia/EulerBrick.lean#L1804.
The first Cuboid conjecture
The DeepMind prover agent has found a formal proof of this statement.
An (independent) informal solution can be found here: Reference: arxiv/2510.11768 Irreducibility of the Cuboid Polynomial P_{a,u}(t) via a Rank-Zero Elliptic Curve by Valery Asiryan
theorem cuboidOne : CuboidOne
Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/EulerBrick.lean, line 106.
EulerBrick.cuboidTwo
Open: stated without proof.
The second Cuboid conjecture
theorem cuboidTwo : CuboidTwo
Category research open; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/EulerBrick.lean, line 124.
EulerBrick.cuboidThree
Open: stated without proof.
The third Cuboid conjecture
theorem cuboidThree : CuboidThree
Category research open; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/EulerBrick.lean, line 146.
EulerBrick.cuboid_perfect_euler_brick
Solved: stated here without proof.
In [Sh12], Ruslan notes that a perfect Euler brick does not exist if all three Cuboid conjectures hold.
theorem cuboid_perfect_euler_brick (h₁ : CuboidOne) (h₂ : CuboidTwo) (h₃ : CuboidThree) :
¬ ∃ a b c : ℕ+, IsPerfectCuboid a b c
Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/EulerBrick.lean, line 152.
Sources
TheoremEuler's sum of powers conjecture#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/EulerSumOfPowers.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 1 open and 2 solved.
EulerSumOfPowers.eulers_sum_of_powers_conjecture
Open: stated without proof.
Euler's sum of powers conjecture states that for integers \(n > 1\) and \(k > 1\), if the sum of \(n\) positive integers each raised to the \(k\)-th power equals another integer raised to the \(k\)-th power, then \(n ≥ k\).
The conjecture is known to be false for \(k = 4\) and \(k = 5\), but remains open for \(k ≥ 6\).
theorem eulers_sum_of_powers_conjecture (n k b : ℕ) (hn : 1 < n) (hk : 5 < k) (a : Fin n → ℕ)
(ha : ∀ i, a i > 0) (hsum : ∑ i, (a i) ^ k = b ^ k) : k ≤ n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/EulerSumOfPowers.lean, line 39.
EulerSumOfPowers.eulers_sum_of_powers_conjecture.false_for_k4
Proved here.
Euler's sum of powers conjecture is false for \(k=4\) (counterexample exists).
theorem eulers_sum_of_powers_conjecture.false_for_k4 : ¬ (∀ (n b : ℕ) (_ : 1 < n)
(a: Fin n → ℕ) (_ : ∀ i, a i > 0) (_ : ∑ i, (a i) ^ 4 = b ^ 4), 4 ≤ n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/EulerSumOfPowers.lean, line 45.
EulerSumOfPowers.eulers_sum_of_powers_conjecture.false_for_k5
Proved here.
Euler's sum of powers conjecture is false for \(k=5\) (counterexample exists).
theorem eulers_sum_of_powers_conjecture.false_for_k5 : ¬ (∀ (n b : ℕ) (_ : 1 < n)
(a: Fin n → ℕ) (_ : ∀ i, a i > 0) (_ : ∑ i, (a i) ^ 5 = b ^ 5), 5 ≤ n)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/EulerSumOfPowers.lean, line 55.
Sources
TheoremExponentials conjectures and theorems#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/Exponentials.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.
Exponentials.four_exponentials_conjecture
Open: stated without proof.
Four exponentials conjecture Let \(x_0, x_1\) and \(y_0, y_1\) be \(\mathbb Q\)-linearly independent pairs of complex numbers, then some \(e^{x_i y_j}\) is transcendental.
theorem four_exponentials_conjecture (x : Fin 2 → ℂ) (y : Fin 2 → ℂ)
(h1 : LinearIndependent ℚ x) (h2 : LinearIndependent ℚ y) :
∃ i j : Fin 2, Transcendental ℚ (exp (x i * y j))
Category research open; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Exponentials.lean, line 38.
Exponentials.two_pow_three_pow_transcendental
Open: stated without proof.
The four exponential conjecture would imply that for any irrational number \(t\), at least one of the numbers \(2^t\) and \(3^t\) is transcendental.
theorem two_pow_three_pow_transcendental (t : ℝ) (h : Irrational t) :
Transcendental ℚ (2 ^ t : ℝ) ∨ Transcendental ℚ (3 ^ t : ℝ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Exponentials.lean, line 48.
Sources
TheoremFactorial primes#
A factorial prime is a prime that is one more or one less than a factorial. It is conjectured that there are infinitely many factorial primes.
References: - Wikipedia, Factorial prime - OEIS A088054
Quoted from FormalConjectures/Wikipedia/FactorialPrime.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 2 test statements, counted here but not shown.
FactorialPrime.infinitely_many_factorial_primes
Open: stated without proof.
There are infinitely many factorial primes.
theorem infinitely_many_factorial_primes :
Set.Infinite {p : ℕ | IsFactorialPrime p}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/FactorialPrime.lean, line 51.
Sources
LemmaFalconer's distance set conjecture#
If \(d \ge 2\) and \(E \subseteq \mathbb{R}^d\) is compact with \(\dim_H E > \frac{d}{2}\), then the distance set
\[\{ |x - y| \mid x, y \in E \}\]has positive Lebesgue measure. The restriction \(d \ge 2\) is needed; see
falconer_conjecture.References
- K. Falconer, On the Hausdorff dimensions of distance sets
- Wikipedia, Falconer's conjecture
- [OAI26a] OpenAI, The Falconer distance conjecture in all dimensions. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Falconer-distance-conjecture-in-all-dimensions-September-23-2026/paper.pdf
Quoted from FormalConjectures/Wikipedia/Falconer.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 solved.
Falconer.falconer_conjecture_two
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/MeasureTheory/Falconer/Main.lean#L50.
Falconer's distance set conjecture, \(d = 2\) case.
This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.
lemma falconer_conjecture_two (E : Set <| ℝ²) (hc : IsCompact E) (hd : 2 < 2 * dimH E ) :
0 < volume (image2 dist E E)
Category research solved; AMS 28 Measure and integration, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/Wikipedia/Falconer.lean, line 52.
Falconer.falconer_conjecture
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/MeasureTheory/Falconer/Campaign123PlanarFurstenbergProof.lean#L47.
Falconer's distance set conjecture in dimension \(d \ge 2\).
The hypothesis \(2 \le d\) excludes a degenerate case: the conclusion is false for \(d = 1\). The base-\(7\) Cantor set \(E = \{\sum_{n \ge 1} a_n 7^{-n} : a_n \in \{0, 1, 2\}\}\) is compact with \(\dim_H E = \log 3 / \log 7 > 1/2\), but \(E - E\) has digits in \(\{-2, \dots, 2\}\), so after fixing \(n\) digits it is covered by \(5^n\) intervals of length \(\frac{2}{3} 7^{-n}\) and is therefore null; its distance set is the image of \(E - E\) under \(|\cdot|\) and is null too.
This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.
lemma falconer_conjecture (d : ℕ) (h2d : 2 ≤ d) (E : Set <| ℝ^d) (hc : IsCompact E)
(hd : d < 2 * dimH E) :
0 < volume (image2 dist E E)
Category research solved; AMS 28 Measure and integration, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/Wikipedia/Falconer.lean, line 68.
Sources
TheoremFeit-Thompson conjecture on primes#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/FeitThompsonPrimeConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open.
FeitThompsonPrimeConjecture.feit_thompson_primes
Open: stated without proof.
There are no distinct primes \(p\) and \(q\) such that \(\frac{q^p - 1}{q - 1}\) divides \(\frac{p^q - 1}{p - 1}\)
theorem feit_thompson_primes (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (h : p < q) :
¬ (q ^ p - 1) / (q - 1) ∣ (p ^ q - 1) / (p - 1)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/FeitThompsonPrimeConjecture.lean, line 34.
Sources
TheoremOpen questions about Fermat numbers#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/Fermat.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.
Fermat.fermat_number_are_composite
Open: stated without proof.
Are Fermat numbers composite for all
n > 4?
theorem fermat_number_are_composite : ∀ n > 4, ¬Prime n.fermatNumber
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Fermat.lean, line 34.
Fermat.infinite_fermat_primes
Open: stated without proof.
Are there infinitely many Fermat primes?
theorem infinite_fermat_primes : Infinite {n : ℕ | Prime n.fermatNumber}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Fermat.lean, line 41.
Fermat.infinite_fermat_composite
Open: stated without proof.
Are there infinitely many composite Fermat numbers?
theorem infinite_fermat_composite : Infinite {n : ℕ | ¬Prime n.fermatNumber}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Fermat.lean, line 48.
Fermat.exists_fermat_not_squarefree
Open: stated without proof.
Does a Fermat number exist that is not square-free?
theorem exists_fermat_not_squarefree : ∃ n : ℕ, ¬Squarefree n.fermatNumber
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Fermat.lean, line 55.
Sources
TheoremFermat-Catalan conjecture#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/FermatCatalanConjecture.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: 1 open and 1 solved.
FermatCatalanConjecture.fermat_catalan
Open: stated without proof.
The Fermat–Catalan conjecture states that the equation \(a^m + b^n = c^k\) has only finitely many solutions \((a,b,c,m,n,k)\) with distinct triplets of values \((a^m, b^n, c^k)\) where \(a, b, c\) are positive coprime integers and \(m, n, k\) are positive integers satisfying \(\frac 1 m + \frac 1 n + \frac 1 k < 1\).
theorem fermat_catalan : fermatCatalanConjecture
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/FermatCatalanConjecture.lean, line 59.
FermatCatalanConjecture.fermat_catalan.variants.darmon_granville
Solved: stated here without proof.
By the Darmon-Granville theorem, for any fixed choice of positive integers m, n and k satisfying \(\frac 1 m + \frac 1 n + \frac 1 k < 1\), only finitely many coprime triples \((a, b, c)\) solving \(a^m + b^n = c^k\) exist.
theorem fermat_catalan.variants.darmon_granville
(m n k : ℕ) (hm : 0 < m) (hn : 0 < n) (hk : 0 < k)
(H : (1 / m : ℝ) + 1 / n + 1 / k < 1) :
{(a, b, c) : ℕ × ℕ × ℕ | 0 < a ∧ 0 < b ∧ 0 < c ∧ a^m + b^n = c^k ∧
({a, b, c} : Set _).Pairwise Nat.Coprime}.Finite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/FermatCatalanConjecture.lean, line 68.
Sources
TheoremFibonacci Primes#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/FibonacciPrimes.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.
FibonacciPrimes.fib_primes_infinite
Open: stated without proof.
There are infinitely many Fibonacci primes, i.e., Fibonacci numbers that are prime It is also a barrier to defining a benchmark from this paper: https://arxiv.org/html/2505.13938v1 (see Figure 8).
theorem fib_primes_infinite : {n : ℕ | (∃ m : ℕ, m.fib = n) ∧ n.Prime}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/FibonacciPrimes.lean, line 37.
FibonacciPrimes.fib_primes_infinite.variant
Open: stated without proof.
There are infinitely many indices \(i\), such that the \(i\)-th Fibonacci is prime.
theorem fib_primes_infinite.variant : {n : ℕ | n.fib.Prime}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/FibonacciPrimes.lean, line 44.
Sources
TheoremFiroozbakht's conjecture#
References: - Wikipedia - primepuzzles
Quoted from FormalConjectures/Wikipedia/Firoozbakht.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: 1 open and 1 solved.
Firoozbakht.firoozbakht_conjecture
Open: stated without proof.
Firoozbakht's conjecture The inequality \(\sqrt[n+1]{p_{n+1}} < \sqrt[n]{p_n}\) holds for all prime numbers \(p_n\).
theorem firoozbakht_conjecture (n : ℕ) :
firoozbakhtSeq (n+1) < firoozbakhtSeq n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Firoozbakht.lean, line 45.
Firoozbakht.firoozbakht_conjecture_consequence
Solved: stated here without proof.
The inequality \(p_{n+1}-p_n < (\log p_n)^2-\log p_n\) holds for all \(n>4\). A consequence of Firuzbakht's conjecture.
theorem firoozbakht_conjecture_consequence (n : ℕ) (hn : 3 < n) (P : type_of% firoozbakht_conjecture) :
(n+1).nth Prime - n.nth Prime < (log (n.nth Prime))^2 - log (n.nth Prime)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Firoozbakht.lean, line 54.
Sources
TheoremConvergence of the Flint Hills and Cookson Hills series#
References: - Wikipedia: Examples of numerical series - MathWorld: Flint Hills Series - Alekseyev, On the Flint Hills series - MathWorld: Cookson Hills Series
Quoted from FormalConjectures/Wikipedia/FlintCooksonHills.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.
FlintCooksonHills.flint_hills_series_converges
Open: stated without proof.
The Flint Hills series summing \(csc(n)^2 / n^3\) from \(n=1\) to \(\infty\) converges. (Note that we 0-index the series below.)
theorem flint_hills_series_converges :
Summable (fun n : ℕ =>
1 / ((((n + 1) : ℝ)^3) * (Real.sin (n + 1)^2)))
Category research open; AMS 40 Sequences, series, summability. Declared in FormalConjectures/Wikipedia/FlintCooksonHills.lean, line 39.
FlintCooksonHills.cookson_hills_series_converges
Open: stated without proof.
The Cookson Hills series summing \(sec(n)^2 / n^3\) from \(n=1\) to \(\infty\) converges.
theorem cookson_hills_series_converges :
Summable (fun n : ℕ =>
1 / ((((n + 1) : ℝ)^3) * (Real.cos (n + 1)^2)))
Category research open; AMS 40 Sequences, series, summability. Declared in FormalConjectures/Wikipedia/FlintCooksonHills.lean, line 48.
Sources
TheoremFortune's Conjecture#
A Fortunate number is the smallest integer \(m > 1\) such that \(p_n\\# + m\) is prime, where \(p_n\\#\) denotes the primorial of the \(n\)-th prime — equivalently, the product of the first \(n\) primes.
Fortune's Conjecture asserts that every Fortunate number is prime — equivalently, that no Fortunate number is composite.
The conjecture is named after the social anthropologist Reo Fortune, who proposed it. The first few Fortunate numbers are \(3, 5, 7, 13, 23, 17, 19, 23, 37, 61, \ldots\) (OEIS A005235); all known values are prime.
References: - Wikipedia - OEIS A005235 - PrimePages glossary entry - PlanetMath: Fortune's conjecture
Quoted from FormalConjectures/Wikipedia/FortuneConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 7 API statements, counted here but not shown.
FortuneConjecture.fortune_conjecture
Open: stated without proof.
Fortune's Conjecture: Every Fortunate number is prime.
theorem fortune_conjecture :
(∀ n : ℕ, Nat.Prime (fortunateNumber n))
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/FortuneConjecture.lean, line 139.
Sources
TheoremFuglede's conjecture in dimensions 1 and 2#
References: - Fuglede's conjecture - [Zh26] Zhang, Tao, Both directions of Fuglede's conjecture fail in dimension two, arXiv:2607.15632 (2026)
Quoted from FormalConjectures/Wikipedia/Fuglede.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 2 open and 1 solved.
Fuglede.FugledeConjecture.variants.dim_1
Open: stated without proof.
Fuglede's conjecture in one dimension: A bounded subset of ℝ with positive Lebesgue measure is spectral iff it tiles ℝ by translation.
theorem FugledeConjecture.variants.dim_1 :
FugledeConjectureFor 1
Category research open; AMS 42 Harmonic analysis on Euclidean spaces, 46 Functional analysis, 47 Operator theory. Declared in FormalConjectures/Wikipedia/Fuglede.lean, line 47.
Fuglede.FugledeConjecture.variants.dim_2
Open: stated without proof.
Fuglede's conjecture in two dimensions: A bounded subset of ℝ^2 with positive Lebesgue measure is spectral iff it tiles ℝ^2 by translation.
[Zh26], a July 2026 preprint, announces a negative answer in both directions, from two explicit \(60\)-point subsets of \(\mathbb{Z}_{60} \times \mathbb{Z}_{12}\) lifted to finite unions of unit squares in \(\mathbb{R}^2\). It is not yet published.
theorem FugledeConjecture.variants.dim_2 :
FugledeConjectureFor 2
Category research open; AMS 42 Harmonic analysis on Euclidean spaces, 46 Functional analysis, 47 Operator theory. Declared in FormalConjectures/Wikipedia/Fuglede.lean, line 59.
Fuglede.FugledeConjecture.variants.dim_3_or_higher
Solved: stated here without proof.
Fuglede's conjecture fails in every dimension \(n \geq 3\): for each such \(n\) there is a bounded subset of \(\mathbb{R}^n\) with positive Lebesgue measure that is spectral but does not tile \(\mathbb{R}^n\) by translation, or that tiles \(\mathbb{R}^n\) by translation but is not spectral. (Note that counterexamples in lower dimensions would also disprove the conjecture in higher dimensions.)
theorem FugledeConjecture.variants.dim_3_or_higher (n : ℕ) (hn : 3 ≤ n) :
¬ FugledeConjectureFor n
Category research solved; AMS 42 Harmonic analysis on Euclidean spaces, 46 Functional analysis, 47 Operator theory. Declared in FormalConjectures/Wikipedia/Fuglede.lean, line 71.
Sources
TheoremGap conjecture#
References: - Wikipedia - On the Gap Conjecture concerning group growth by Rostislav Grigorchuk
Quoted from FormalConjectures/Wikipedia/GapConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open.
GapConjecture.gap_conjecture
Open: stated without proof.
If a finitely generated group has superpolynomial growth, then with respect to any finite generating set its growth function is at least \(e^{\sqrt n}\) in Grigorchuk's preorder on growth functions, where the comparison is witnessed by linearly rescaling the radius.
theorem gap_conjecture :
∀ (G : Type) [Group G] (S : Set G), S.Finite → Subgroup.closure S = ⊤ →
HasSuperPolynomialGrowth G →
∃ C : ℕ, 0 < C ∧
∀ᶠ n : ℕ in atTop, Real.exp (Real.sqrt (n : ℝ)) ≤
(GrowthFunction S (C * n) : ℝ)
Category research open; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/GapConjecture.lean, line 41.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.