Pierce–Birkhoff conjecture to Hypothesis H
TheoremPierce–Birkhoff conjecture#
Reference: Wikipedia
The Pierce-Birkhoff conjecture asserts that any piecewise-polynomial function can be expressed as a maximum of finite minima of finite collections of polynomials. It was first stated in 1956 by Garrett Birkhoff and Richard S. Pierce, though the modern rigorous formulation is due to Melvin Henriksen and John R. Isbell.
The conjecture has been proved for
n = 1andn = 2by Louis Mahé.
Quoted from FormalConjectures/Wikipedia/PierceBirkhoff.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.
PierceBirkhoff.pierce_birkhoff_conjecture
Open: stated without proof.
The Pierce-Birkhoff conjecture states that for every real piecewise-polynomial function
f : ℝⁿ → ℝ, there exists a finite set of polynomialsgᵢⱼ ∈ ℝ[x₁, ..., xₙ]such thatf = supᵢ infⱼ(gᵢⱼ).
theorem pierce_birkhoff_conjecture {n : ℕ} (f : (Fin n → ℝ) → ℝ)
(hf : IsPiecewiseMvPolynomial f) :
∃ (ι κ : Type) (g : ι → κ → MvPolynomial (Fin n) ℝ), Finite ι ∧ Finite κ ∧
∀ x, f x = ⨆ i, ⨅ j, MvPolynomial.eval x (g i j)
Category research open; AMS 13 Commutative algebra. Declared in FormalConjectures/Wikipedia/PierceBirkhoff.lean, line 90.
PierceBirkhoff.pierce_birkhoff_conjecture_dim_one
Solved: stated here without proof.
The Pierce-Birkhoff conjecture holds for
n = 1. This was proved by Louis Mahé.
theorem pierce_birkhoff_conjecture_dim_one (f : ℝ → ℝ)
(hf : IsPiecewisePolynomial f) :
∃ (ι κ : Type) (g : ι → κ → Polynomial ℝ), Finite ι ∧ Finite κ ∧
∀ x, f x = ⨆ i, ⨅ j, Polynomial.eval x (g i j)
Category research solved; AMS 13 Commutative algebra. Declared in FormalConjectures/Wikipedia/PierceBirkhoff.lean, line 101.
PierceBirkhoff.pierce_birkhoff_conjecture_dim_two
Solved: stated here without proof.
The Pierce-Birkhoff conjecture holds for
n = 2. This was proved by Louis Mahé.
theorem pierce_birkhoff_conjecture_dim_two
(f : (Fin 2 → ℝ) → ℝ) (hf : IsPiecewiseMvPolynomial f) :
∃ (ι κ : Type) (g : ι → κ → MvPolynomial (Fin 2) ℝ), Finite ι ∧ Finite κ ∧
∀ x, f x = ⨆ i, ⨅ j, MvPolynomial.eval x (g i j)
Category research solved; AMS 13 Commutative algebra. Declared in FormalConjectures/Wikipedia/PierceBirkhoff.lean, line 112.
Sources
TheoremPierpont primes#
A Pierpont prime is a prime of the form \(2^a 3^b + 1\), where \(a\) and \(b\) are nonnegative integers. Marc Gleason conjectured that there are infinitely many.
References: - Wikipedia, Pierpont prime - OEIS A005109
Quoted from FormalConjectures/Wikipedia/PierpontPrime.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.
PierpontPrime.infinitely_many_pierpont_primes
Open: stated without proof.
There are infinitely many Pierpont primes.
theorem infinitely_many_pierpont_primes :
Set.Infinite {p : ℕ | IsPierpontPrime p}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PierpontPrime.lean, line 51.
Sources
TheoremPollock's (tetrahedral numbers) conjecture#
Every positive integer is the sum of at most 5 tetrahedral numbers.
References: - Wikipedia - A797 - L. E. Dickson, History of the Theory of Numbers, Vol. II: Diophantine Analysis, Dover (2005), pp. 22–23 - Frederick Pollock, On the extension of the principle of Fermat's theorem on the polygonal numbers to the higher order of series whose ultimate differences are constant, Abstracts of the Papers Communicated to the Royal Society of London 5 (1850), 922–924 - H. E. Salzer and N. Levine, Table of integers not exceeding 100000 that are not expressible as the sum of four tetrahedral numbers, Math. Comp. 12 (1958), 141–144 - MathWorld: Pollock's Conjecture
Quoted from FormalConjectures/Wikipedia/PollocksConjecture.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 textbook result.
PollocksConjecture.pollock_tetrahedral
Open: stated without proof.
Pollock's (tetrahedral numbers) conjecture: every integer is the sum of at most \(5\) tetrahedral numbers.
theorem pollock_tetrahedral (N : ℕ) :
∃ f : Fin 5 → ℕ, N = ∑ i, tetrahedral (f i)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PollocksConjecture.lean, line 59.
PollocksConjecture.pollock_tetrahedral.salzer_levine
Open: stated without proof.
Salzer–Levine strengthening (as stated on Wikipedia/OEIS): there are exactly \(241\) integers that are not a sum of \(4\) tetrahedral numbers, and the largest is \(343867\).
theorem pollock_tetrahedral.salzer_levine :
IsGreatest NotSumOfFourTetrahedral 343867
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PollocksConjecture.lean, line 68.
PollocksConjecture.pollock_tetrahedral.ncard_exceptions
Textbook result, stated without proof.
As stated on Wikipedia/OEIS (A797), the set of exceptions has cardinality \(241\).
theorem pollock_tetrahedral.ncard_exceptions :
type_of% pollock_tetrahedral.salzer_levine ↔
NotSumOfFourTetrahedral.ncard = 241
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PollocksConjecture.lean, line 74.
Sources
TheoremThe Pompeiu problem#
Let \(\Omega \subset \mathbb{R}^{N+1}\) be a bounded domain. A rigid motion is an isometry of \(\mathbb{R}^{N+1}\) (a composition of translations and rotations), modelled here by an
AffineIsometryEquivof Euclidean space with itself.The domain \(\Omega\) has the Pompeiu property if the only continuous function \(f : \mathbb{R}^{N+1} \to \mathbb{R}\) with \(\int_{\sigma(\Omega)} f = 0\) for every rigid motion \(\sigma\) is \(f \equiv 0\).
The Pompeiu problem (Pompeiu's conjecture) asserted that, among bounded simply connected domains with Lipschitz boundary, the Euclidean ball is the only domain that fails to have the Pompeiu property. That a ball fails is classical: radial functions built from Bessel functions have vanishing integral over every congruent ball. The converse is false. Two independent proofs of this negative conclusion are referenced below.
References: - Wikipedia - Encyclopedia of Mathematics - [BST73] Brown, L., Schreiber, B. M. and Taylor, B. A., Spectral synthesis and the Pompeiu problem, Ann. Inst. Fourier 23 (1973), 125–154. (Proves a ball fails the Pompeiu property; for a ball of radius
Rthe witness isf(x) = sin(a x₁)withJ_{n/2}(a R) = 0.) - Zalcman, L., A bibliographic survey of the Pompeiu problem, in Approximation by Solutions of Partial Differential Equations, NATO ASI Ser. 365 (1992), 185–194. - [CLD26] Cao-Labora, G. and de Dios Pont, J., Schiffer, a Lean 4 formalization of a non-disk planar counterexample. - [CS26] Colbrook, M. J. and Stepaniants, G., A computer-assisted counterexample to the planar Pompeiu and Schiffer conjectures, arXiv:2608.01579 (2026).
Quoted from FormalConjectures/Wikipedia/PompeiuProblem.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: 3 solved. It also has 1 test statement, counted here but not shown.
PompeiuProblem.pompeiu_conjecture
Solved: stated here; a Lean proof is at https://github.com/jaumededios/Schiffer/blob/2938e277969c329caf154e48a3d8823f3635c7f1/Schiffer/FormalConjecturesSolution.lean#L446-L469.
Pompeiu's conjecture is false. There is a bounded, simply connected Lipschitz domain in \(\mathbb{R}^2\) which fails to have the Pompeiu property but is not a Euclidean ball. This conclusion has two independent proofs: the Lean-formalized construction of Cao-Labora and de Dios Pont [CLD26], and the computer-assisted construction of Colbrook and Stepaniants [CS26].
theorem pompeiu_conjecture :
¬ ∀ Ω : Set (EuclideanSpace ℝ (Fin 2)),
IsAdmissibleDomain Ω → (¬ HasPompeiuProperty Ω ↔ IsBall Ω)
Category research solved; AMS 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/Wikipedia/PompeiuProblem.lean, line 109.
PompeiuProblem.ball_not_hasPompeiuProperty
Solved: stated here without proof.
The classical (easy) direction, proved by Brown–Schreiber–Taylor [BST73]: a Euclidean ball fails to have the Pompeiu property. For a ball of radius
R, an explicit witness isf(x) = sin(a x₁)wherea > 0is chosen so that the Bessel functionJ_{n/2}(a R) = 0; its integral over every congruent ball vanishes.
theorem ball_not_hasPompeiuProperty (Ω : Set (EuclideanSpace ℝ (Fin (N + 1))))
(hball : IsBall Ω) :
¬ HasPompeiuProperty Ω
Category research solved; AMS 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/Wikipedia/PompeiuProblem.lean, line 121.
PompeiuProblem.not_hasPompeiuProperty_imp_ball
Solved: stated here; a Lean proof is at https://github.com/jaumededios/Schiffer/blob/2938e277969c329caf154e48a3d8823f3635c7f1/Schiffer/FormalConjecturesSolution.lean#L446-L469.
The hard direction of the Pompeiu problem is false: some admissible planar domain lacks the Pompeiu property without being a ball. Two independent proofs are given in [CLD26] and [CS26].
theorem not_hasPompeiuProperty_imp_ball :
¬ ∀ Ω : Set (EuclideanSpace ℝ (Fin 2)),
IsAdmissibleDomain Ω → ¬ HasPompeiuProperty Ω → IsBall Ω
Category research solved; AMS 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/Wikipedia/PompeiuProblem.lean, line 134.
Sources
TheoremAsymptotic density of powerful numbers#
Let \(Q(x)\) denote the number of powerful integers up to \(x\). Erdős and Szekeres [ES35] proved
\[Q(x) = \frac{\zeta(3/2)}{\zeta(3)} x^{1/2} + O(x^{1/3}),\]and Bateman and Grosswald [BG58] sharpened this to
\[Q(x) = \frac{\zeta(3/2)}{\zeta(3)} x^{1/2} + \frac{\zeta(2/3)}{\zeta(2)} x^{1/3} + O(x^{1/6}).\]Improving the exponent \(1/6\) in the error term unconditionally remains open; conditional improvements are known under the Riemann Hypothesis.
References: - Wikipedia - [ES35] Erdős, P. and Szekeres, G., Über die Anzahl der Abelschen Gruppen gegebener Ordnung und über ein verwandtes zahlentheoretisches Problem, Acta Sci. Math. (Szeged) 7 (1935), 95–102. - [BG58] Bateman, P. T. and Grosswald, E., On a theorem of Erdős and Szekeres, Illinois J. Math. 2 (1958), 88–98.
Quoted from FormalConjectures/Wikipedia/PowerfulNumbersDensity.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.
PowerfulNumbersDensity.asymptotic_erdos_szekeres
Solved: stated here without proof.
Erdős and Szekeres [ES35] proved that the number of powerful integers up to \(x\) satisfies
\[Q(x) = \frac{\zeta(3/2)}{\zeta(3)} x^{1/2} + O(x^{1/3}).\]In particular \(Q(x) \sim \frac{\zeta(3/2)}{\zeta(3)} \sqrt{x}\).
theorem asymptotic_erdos_szekeres :
(fun x : ℝ => (Q x : ℝ) - A * x ^ ((1 : ℝ) / 2)) =O[atTop]
fun x => x ^ ((1 : ℝ) / 3)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PowerfulNumbersDensity.lean, line 60.
PowerfulNumbersDensity.asymptotic_bateman_grosswald
Solved: stated here without proof.
Bateman and Grosswald [BG58] proved the sharper asymptotic
\[Q(x) = \frac{\zeta(3/2)}{\zeta(3)} x^{1/2} + \frac{\zeta(2/3)}{\zeta(2)} x^{1/3} + O(x^{1/6}).\]
theorem asymptotic_bateman_grosswald :
(fun x : ℝ => (Q x : ℝ) - A * x ^ ((1 : ℝ) / 2) - B * x ^ ((1 : ℝ) / 3)) =O[atTop]
fun x => x ^ ((1 : ℝ) / 6)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PowerfulNumbersDensity.lean, line 70.
PowerfulNumbersDensity.error_term_improvement
Open: stated without proof.
Can the exponent \(1/6\) in the error term of the Bateman–Grosswald asymptotic be improved unconditionally? That is, is there \(\delta > 0\) such that
\[Q(x) = \frac{\zeta(3/2)}{\zeta(3)} x^{1/2} + \frac{\zeta(2/3)}{\zeta(2)} x^{1/3} + O(x^{1/6 - \delta})?\]Improvements are known under the Riemann Hypothesis.
theorem error_term_improvement :
∃ δ > (0 : ℝ),
(fun x : ℝ => (Q x : ℝ) - A * x ^ ((1 : ℝ) / 2) - B * x ^ ((1 : ℝ) / 3)) =O[atTop]
fun x => x ^ ((1 : ℝ) / 6 - δ)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PowerfulNumbersDensity.lean, line 83.
Sources
TheoremPrimes and perfect squares#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/PrimesAndPerfectSquares.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.
PrimesAndPerfectSquares.infinite_prime_sq_add_one
Open: stated without proof.
Are there infinitely many primes \(p\) such that \(p - 1\) is a perfect square? In other words: Are there infinitely many primes of the form \(n^2 + 1\)?
theorem infinite_prime_sq_add_one :
{n : ℕ | Prime (n^2 + 1)}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PrimesAndPerfectSquares.lean, line 35.
Sources
TheoremPrime Triplet Conjecture#
Reference: Prime Triplet Wikipedia Page
Quoted from FormalConjectures/Wikipedia/PrimeTriplets.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.
PrimeTriplets.prime_triplets
Open: stated without proof.
Are there infinitely many tuples of three consecutive primes \((p, q, r)\) such that \(r - p = 6\)?
theorem prime_triplets :
{p : ℕ | Prime p ∧ (Prime (p + 2) ∨ Prime (p + 4)) ∧ Prime (p + 6)}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PrimeTriplets.lean, line 34.
Sources
TheoremQuasiperfect Numbers#
Reference: - Wikipedia
Quoted from FormalConjectures/Wikipedia/QuasiperfectNumbers.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.
QuasiperfectNumbers.exists_quasiperfect
Open: stated without proof.
Quasiperfect Numbers Conjecture. Do quasiperfect numbers exist?
theorem exists_quasiperfect :
∃ n, Quasiperfect n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/QuasiperfectNumbers.lean, line 46.
Sources
TheoremRamanujan τ-function#
There are two conjectures related to the Ramanujan τ-function:
- Ramanujan-Petersson conjecture: For every prime
p, the absolute value of the Ramanujan τ-function atpis bounded by2 * p^(11/2).- Lehmer's conjecture: The Ramanujan τ-function is never zero for any positive integer
n.References: - Ramanujan-Petersson conjecture - Lehmer's conjecture
Quoted from FormalConjectures/Wikipedia/RamanujanTau.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. It also has 3 test statements and 1 API statement, counted here but not shown.
RamanujanTau.ramanujan_petersson
Solved: stated here without proof.
The Ramanujan-Petersson conjecture: \(|\tau(p)| \le 2 p^{11/2}\) for primes \(p\).
theorem ramanujan_petersson : ∀ p : ℕ, Prime p → abs (τ p) ≤ 2 * (p : ℝ) ^ ((11 : ℝ) / 2)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/RamanujanTau.lean, line 65.
RamanujanTau.lehmer_ramanujan_tau
Open: stated without proof.
Lehmer's conjecture: \(\tau(n) \ne 0\) for all \(n > 0\).
theorem lehmer_ramanujan_tau : ∀ n > 0, τ n ≠ 0
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/RamanujanTau.lean, line 70.
Sources
TheoremRamsey numbers#
The (graph) Ramsey number \(R(k,\ell)\) is the least natural number \(n\) such that every simple graph on \(n\) vertices contains either a clique of size \(k\) or an independent set of size \(\ell\) (equivalently, the complement graph contains a clique of size \(\ell\)).
We formalize the classical open problem of determining \(R(5,5)\), together with the currently best known bounds \(43 \le R(5,5) \le 46\).
Note: the diagonal Ramsey number \(R(n,n)\) can also be formulated in terms of 2-colorings of \(2\)-subsets, as
Combinatorics.hypergraphRamsey 2 n(seeFormalConjecturesForMathlib/Combinatorics/Ramsey.lean).References: - Wikipedia: Ramsey number - [Rad] S. P. Radziszowski, Small Ramsey Numbers, Electronic Journal of Combinatorics, Dynamic Survey DS1. (Updated periodically.) https://www.combinatorics.org/ojs/index.php/eljc/article/view/DS1 - [Exoo89] G. Exoo, A lower bound for \(R(5,5)\), Journal of Graph Theory 13 (1989), 97–98. DOI: 10.1002/jgt.3190130113 - [AM24] V. Angeltveit and B. McKay, \(R(5,5) \le 46\), arXiv:2409.15709 (2024). - OEIS A212954 - MathWorld: Ramsey Number
Quoted from FormalConjectures/Wikipedia/RamseyNumbers.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 15 research or textbook statements: 2 open and 13 solved. It also has 3 API statements, counted here but not shown.
RamseyNumbers.ramsey_number_five_five
Open: stated without proof.
The open problem: determine the Ramsey number \(R(5,5)\).
It is known that \(43 \le R(5,5) \le 46\).
theorem ramsey_number_five_five :
R(5, 5) = ramsey_number_five_five.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 98.
RamseyNumbers.ramsey_number_five_five_lower_bound
Solved: stated here without proof.
Lower bound \(43 \le R(5,5)\), equivalently: there exists a graph on \(42\) vertices with no \(5\)-clique and no independent set of size \(5\).
theorem ramsey_number_five_five_lower_bound :
∃ G : SimpleGraph (Fin 42), G.CliqueFree 5 ∧ (Gᶜ).CliqueFree 5
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 107.
RamseyNumbers.ramsey_number_five_five_upper_bound
Solved: stated here without proof.
Upper bound \(R(5,5) \le 46\), i.e. every graph on \(46\) vertices contains a \(5\)-clique or an independent set of size \(5\).
theorem ramsey_number_five_five_upper_bound :
IsGraphRamsey 46 5 5
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 116.
RamseyNumbers.ramsey_number_three_three
Solved: stated here without proof.
\(R(3,3) = 6\).
theorem ramsey_number_three_three : R(3, 3) = 6
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 129.
RamseyNumbers.ramsey_number_three_four
Solved: stated here without proof.
\(R(3,4) = 9\).
theorem ramsey_number_three_four : R(3, 4) = 9
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 134.
RamseyNumbers.ramsey_number_three_five
Solved: stated here without proof.
\(R(3,5) = 14\).
theorem ramsey_number_three_five : R(3, 5) = 14
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 139.
RamseyNumbers.ramsey_number_three_six
Solved: stated here without proof.
\(R(3,6) = 18\).
theorem ramsey_number_three_six : R(3, 6) = 18
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 144.
RamseyNumbers.ramsey_number_three_seven
Solved: stated here without proof.
\(R(3,7) = 23\).
theorem ramsey_number_three_seven : R(3, 7) = 23
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 149.
RamseyNumbers.ramsey_number_three_eight
Solved: stated here without proof.
\(R(3,8) = 28\).
theorem ramsey_number_three_eight : R(3, 8) = 28
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 154.
RamseyNumbers.ramsey_number_three_nine
Solved: stated here without proof.
\(R(3,9) = 36\) (Grinstead–Roberts).
theorem ramsey_number_three_nine : R(3, 9) = 36
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 159.
RamseyNumbers.ramsey_number_four_four
Solved: stated here without proof.
The diagonal Ramsey number \(R(4,4) = 18\).
theorem ramsey_number_four_four : R(4, 4) = 18
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 164.
RamseyNumbers.ramsey_number_four_five
Solved: stated here without proof.
\(R(4,5) = 25\) (McKay–Radziszowski).
theorem ramsey_number_four_five : R(4, 5) = 25
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 169.
RamseyNumbers.ramsey_number_six_six
Open: stated without proof.
The diagonal Ramsey number \(R(6,6)\) is unknown. The best known bounds recorded in [Rad] are \(102 \le R(6,6) \le 165\).
theorem ramsey_number_six_six : R(6, 6) = ramsey_number_six_six.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 179.
RamseyNumbers.ramsey_number_six_six_lower_bound
Solved: stated here without proof.
Lower bound \(102 \le R(6,6)\), equivalently: there exists a graph on \(101\) vertices with no \(6\)-clique and no independent set of size \(6\).
theorem ramsey_number_six_six_lower_bound :
∃ G : SimpleGraph (Fin 101), G.CliqueFree 6 ∧ (Gᶜ).CliqueFree 6
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 187.
RamseyNumbers.ramsey_number_six_six_upper_bound
Solved: stated here without proof.
Upper bound \(R(6,6) \le 165\), i.e. every graph on \(165\) vertices contains a \(6\)-clique or an independent set of size \(6\).
theorem ramsey_number_six_six_upper_bound :
IsGraphRamsey 165 6 6
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/RamseyNumbers.lean, line 196.
Sources
TheoremRational distance problem#
References: - Wikipedia - mathoverflow/418260 asked by user Yuan Yang - D19 in Unsolved Problems in Number Theory by Richard K. Guy
Quoted from FormalConjectures/Wikipedia/RationalDistanceProblem.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.
RationalDistanceProblem.rational_distance_problem
Open: stated without proof.
Does there exist a point in the plane at rational distance from all four vertices of the unit square?
theorem rational_distance_problem :
∃ P : ℝ² , ∀ i, ¬ Irrational (dist P (UnitSquareCorners i))
Category research open; AMS 11 Number theory, 51 Geometry. Declared in FormalConjectures/Wikipedia/RationalDistanceProblem.lean, line 44.
Sources
TheoremThe reconstruction conjecture#
References: * Wikipedia * [Ke57] Kelly, P. J. (1957). "A congruence theorem for trees." Pacific J. Math. 7, pp. 961--968. * [Ul60] Ulam, S. M. (1960). A Collection of Mathematical Problems. Interscience, New York. * [Ha64] Harary, F. (1964). "On the reconstruction of a graph from a collection of subgraphs." In Theory of Graphs and its Applications, Academia, Prague, pp. 47--52. * [Lo72] Lovász, L. (1972). "A note on the line reconstruction problem." J. Combin. Theory Ser. B 13, pp. 309--310. * [Mu77] Müller, V. (1977). "The edge reconstruction hypothesis is true for graphs with more than n·log n edges." J. Combin. Theory Ser. B 22, pp. 281--283. * [Bo91] Bondy, J. A. (1991). "A graph reconstructor's manual." In Surveys in Combinatorics, LMS Lecture Note Series 166, Cambridge University Press, pp. 221--252.
Quoted from FormalConjectures/Wikipedia/ReconstructionConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 6 research or textbook statements: 2 open and 4 solved. It also has 1 test statement and 3 API statements, counted here but not shown.
ReconstructionConjecture.reconstruction_conjecture
Open: stated without proof.
The reconstruction conjecture (Kelly [Ke57], Ulam [Ul60]).
Every finite simple graph on at least three vertices is determined up to isomorphism by its deck of vertex-deleted subgraphs: any two hypomorphic graphs on at least three vertices are isomorphic.
theorem reconstruction_conjecture {V W : Type} [Fintype V] [Fintype W]
(hV : 3 ≤ Fintype.card V) (G : SimpleGraph V) (H : SimpleGraph W)
(h : Hypomorphic G H) : Nonempty (G ≃g H)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/ReconstructionConjecture.lean, line 92.
ReconstructionConjecture.reconstruction_conjecture.variants.tree
Solved: stated here without proof.
Trees are reconstructible (Kelly [Ke57]).
Every tree on at least three vertices is determined up to isomorphism by its deck of vertex-deleted subgraphs.
theorem reconstruction_conjecture.variants.tree {V W : Type} [Fintype V] [Fintype W]
(hV : 3 ≤ Fintype.card V) (G : SimpleGraph V) (H : SimpleGraph W)
(hc : G.Connected) (ha : G.IsAcyclic) (h : Hypomorphic G H) : Nonempty (G ≃g H)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/ReconstructionConjecture.lean, line 104.
ReconstructionConjecture.reconstruction_conjecture.variants.disconnected
Solved: stated here without proof.
Disconnected graphs are reconstructible.
Every disconnected graph on at least three vertices is determined up to isomorphism by its deck of vertex-deleted subgraphs; see [Bo91].
theorem reconstruction_conjecture.variants.disconnected {V W : Type} [Fintype V] [Fintype W]
(hV : 3 ≤ Fintype.card V) (G : SimpleGraph V) (H : SimpleGraph W)
(hd : ¬G.Connected) (h : Hypomorphic G H) : Nonempty (G ≃g H)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/ReconstructionConjecture.lean, line 116.
ReconstructionConjecture.edge_reconstruction_conjecture
Open: stated without proof.
The edge reconstruction conjecture (Harary [Ha64]).
Every finite simple graph with at least four edges is determined up to isomorphism by its deck of edge-deleted subgraphs: any two edge-hypomorphic graphs on the same vertex set with at least four edges are isomorphic.
theorem edge_reconstruction_conjecture {V : Type} [Fintype V] (G H : SimpleGraph V)
(hE : 4 ≤ G.edgeSet.ncard) (h : EdgeHypomorphic G H) : Nonempty (G ≃g H)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/ReconstructionConjecture.lean, line 152.
ReconstructionConjecture.edge_reconstruction_conjecture.variants.lovasz
Solved: stated here without proof.
Lovász (1972): graphs with more than half of all possible edges are edge-reconstructible.
If a graph on
nvertices has more thann (n - 1) / 4edges, then it is determined up to isomorphism by its deck of edge-deleted subgraphs.Reference: [Lo72].
theorem edge_reconstruction_conjecture.variants.lovasz {V : Type} [Fintype V]
(G H : SimpleGraph V) (hE : (Fintype.card V).choose 2 < 2 * G.edgeSet.ncard)
(h : EdgeHypomorphic G H) : Nonempty (G ≃g H)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/ReconstructionConjecture.lean, line 165.
ReconstructionConjecture.edge_reconstruction_conjecture.variants.mueller
Solved: stated here without proof.
Müller (1977): graphs with many edges are edge-reconstructible.
If a graph on
nvertices withmedges satisfiesn! < 2 ^ (m - 1), then it is determined up to isomorphism by its deck of edge-deleted subgraphs.Reference: [Mu77].
theorem edge_reconstruction_conjecture.variants.mueller {V : Type} [Fintype V]
(G H : SimpleGraph V) (hE : Nat.factorial (Fintype.card V) < 2 ^ (G.edgeSet.ncard - 1))
(h : EdgeHypomorphic G H) : Nonempty (G ≃g H)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/ReconstructionConjecture.lean, line 179.
Sources
TheoremInfinite Regular Primes#
We define the notion of regular primes, which are prime numbers that are coprime with the cardinality of the class group of the
p-th cyclotomic field. We also state that there are infinitely many regular primes.Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/RegularPrimes.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 5 research or textbook statements: 1 open, 1 solved and 3 textbook results.
RegularPrimes.not_isRegularPrime_37
Textbook result, stated without proof.
The prime 37 is not a regular prime.
theorem not_isRegularPrime_37 : ¬ @IsRegularPrime 37 (by decide)
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/RegularPrimes.lean, line 45.
RegularPrimes.small_regular_primes
Textbook result, stated without proof.
The primes 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, and 31 are regular.
lemma small_regular_primes :
{ 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31 } ⊆ regularPrimes
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/RegularPrimes.lean, line 56.
RegularPrimes.isRegularPrime_iff_Bernoulli
Textbook result, stated without proof.
Kummer's criterion. An equivalent definition of a regular prime
pis that it does not divide the numerator of any of the Bernoulli numbers \(B_k\) for \(k = 2, 4, 6, \dots, p - 3\). Not in Mathlib.
theorem isRegularPrime_iff_Bernoulli (p : ℕ) [Fact p.Prime] :
IsRegularPrime p ↔ ∀ k ∈ Finset.Icc 2 (p - 3), Even k → ¬ (p : ℤ) ∣ (bernoulli' k).num
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/RegularPrimes.lean, line 64.
RegularPrimes.infinitude_of_irregularprimes
Solved: stated here without proof.
The set of irregular primes is infinite.
theorem infinitude_of_irregularprimes : irregularPrimes.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/RegularPrimes.lean, line 70.
RegularPrimes.regularprime_conjecture
Open: stated without proof.
Conjecture: The set of regular primes is infinite.
theorem regularprime_conjecture : RegularPrimeConjecture
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/RegularPrimes.lean, line 79.
Sources
TheoremDecimal Repunit Primes#
A decimal repunit is a natural number whose decimal representation consists entirely of ones. It is conjectured that infinitely many decimal repunits are prime.
References: - Wikipedia: Repunit - OEIS A002275 - OEIS A004022 - OEIS A004023
Quoted from FormalConjectures/Wikipedia/RepunitPrime.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 test statements, counted here but not shown.
RepunitPrime.infinitely_many_repunit_primes
Open: stated without proof.
Wikipedia's repunit article states: "It has been conjectured that there are infinitely many repunit primes."
theorem infinitely_many_repunit_primes :
{n : ℕ | (repunit10 n).Prime}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/RepunitPrime.lean, line 73.
Sources
TheoremResolution of singularities#
A variety \(X\) over a field \(k\) admits a resolution of singularities if there is a smooth \(k\)-variety \(Y\) and a proper birational morphism \(Y \to X\). Hironaka proved that every variety over a field of characteristic zero admits one. In positive characteristic this is known over a perfect field in dimension at most three, and is open from dimension four on. Perfectness of \(k\) cannot be dropped from the statement in this form: over an imperfect field it fails already in dimension zero, see
exists_not_hasResolution_of_not_perfectFieldbelow. Over an arbitrary field one asks instead that \(Y\) be regular.References: * Wikipedia * [Hir1964] H. Hironaka, Resolution of singularities of an algebraic variety over a field of characteristic zero, I and II, Ann. of Math. 79 (1964), 109--203 and 205--326. * [Kol2007] J. Kollár, Resolution of singularities -- Seattle lecture, Theorem 36. * [Hau2010] H. Hauser, On the problem of resolution of singularities in positive characteristic (or: a proof we are still waiting for), Bull. Amer. Math. Soc. 47 (2010), 1--30. * [Lip1978] J. Lipman, Desingularization of two-dimensional schemes, Ann. of Math. 107 (1978), 151--207. * [CP2008] V. Cossart and O. Piltant, Resolution of singularities of threefolds in positive characteristic I, J. Algebra 320 (2008), 1051--1082. * [CP2009] V. Cossart and O. Piltant, Resolution of singularities of threefolds in positive characteristic II, J. Algebra 321 (2009), 1836--1976. * [CP2019] V. Cossart and O. Piltant, Resolution of singularities of arithmetical threefolds, J. Algebra 529 (2019), 268--535.
Quoted from FormalConjectures/Wikipedia/ResolutionOfSingularities.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: 1 open, 2 solved and 1 textbook result. It also has 1 test statement and 1 API statement, counted here but not shown.
AlgebraicGeometry.resolution_of_singularities
Open: stated without proof.
Resolution of singularities in positive characteristic. Let \(k\) be a perfect field of characteristic \(p > 0\) and let \(X\) be an integral scheme that is separated and of finite type over \(k\). Then there is an integral scheme \(Y\) that is smooth over \(k\) together with a proper birational morphism \(Y \to X\).
This is open from dimension four on; see [Hau2010]. Perfectness of \(k\) is needed for the conclusion as stated; see
exists_not_hasResolution_of_not_perfectField.
theorem resolution_of_singularities (k : Type u) [Field k] [PerfectField k] (p : ℕ)
[Fact p.Prime] [CharP k p] {X : Scheme.{u}} (sX : X ⟶ Spec (.of k)) [IsIntegral X]
[LocallyOfFiniteType sX] [QuasiCompact sX] [IsSeparated sX] :
Scheme.HasResolution sX
Category research open; AMS 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/ResolutionOfSingularities.lean, line 105.
AlgebraicGeometry.resolution_of_singularities_of_charZero
Solved: stated here without proof.
Hironaka's theorem. Every integral scheme that is separated and of finite type over a field of characteristic zero admits a resolution of singularities. This is the main theorem of [Hir1964]; see [Kol2007], Theorem 36, for a statement in the generality used here.
theorem resolution_of_singularities_of_charZero (k : Type u) [Field k] [CharZero k]
{X : Scheme.{u}} (sX : X ⟶ Spec (.of k)) [IsIntegral X] [LocallyOfFiniteType sX]
[QuasiCompact sX] [IsSeparated sX] :
Scheme.HasResolution sX
Category research solved; AMS 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/ResolutionOfSingularities.lean, line 117.
AlgebraicGeometry.resolution_of_singularities_of_topologicalKrullDim_le_three
Solved: stated here without proof.
Resolution of singularities holds in dimension at most three over any perfect field. In characteristic zero this is [Hir1964]. In positive characteristic, dimension at most two is [Lip1978] and dimension three is due to Cossart and Piltant: [CP2008] and [CP2009] prove it for quasi-projective varieties over a field that is differentially finite over a perfect subfield, and [CP2019], Theorem 1.1, removes both restrictions, resolving every reduced separated Noetherian quasi-excellent scheme of dimension at most three in any characteristic. That theorem gives an everywhere regular source, which over a perfect field is the same as a smooth one. The problem is open in positive characteristic from dimension four on.
theorem resolution_of_singularities_of_topologicalKrullDim_le_three (k : Type u) [Field k]
[PerfectField k] {X : Scheme.{u}} (sX : X ⟶ Spec (.of k)) [IsIntegral X]
[LocallyOfFiniteType sX] [QuasiCompact sX] [IsSeparated sX]
(hX : topologicalKrullDim X ≤ 3) :
Scheme.HasResolution sX
Category research solved; AMS 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/ResolutionOfSingularities.lean, line 134.
AlgebraicGeometry.exists_not_hasResolution_of_not_perfectField
Textbook result, stated without proof.
Resolution of singularities fails over imperfect fields. If the field \(k\) is not perfect, then there is an integral scheme \(X\) of dimension zero that is separated and of finite type over \(k\) and has no resolution of singularities: no integral scheme smooth over \(k\) admits a proper birational morphism to \(X\).
A witness: \(k\) has characteristic \(p > 0\) and there is some \(a \in k \setminus k^p\). Take \(X = \operatorname{Spec} k(a^{1/p})\). Every integral scheme birational to \(X\) has function field \(k(a^{1/p})\), which is not separable over \(k\), whereas the function field of an integral scheme smooth over \(k\) is separable over \(k\).
So the hypothesis
PerfectField kcannot be dropped fromresolution_of_singularitiesor fromresolution_of_singularities_of_topologicalKrullDim_le_three.
theorem exists_not_hasResolution_of_not_perfectField (k : Type u) [Field k]
(hk : ¬ PerfectField k) :
∃ (X : Scheme.{u}) (sX : X ⟶ Spec (.of k)), IsIntegral X ∧ LocallyOfFiniteType sX ∧
QuasiCompact sX ∧ IsSeparated sX ∧ topologicalKrullDim X = 0 ∧
¬ Scheme.HasResolution sX
Category textbook; AMS 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/ResolutionOfSingularities.lean, line 156.
Sources
TheoremParticular values of the Riemann zeta function#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/RiemannZetaValues.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 8 research or textbook statements: 4 open and 4 solved.
RiemannZetaValues.irrational_five
Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/a14b09f420e81b662b9b3e18d0b9b7ccefbdbeef/FormalConjectures/Wikipedia/RiemannZetaValues.lean#L38; a Lean proof is at https://github.com/mo271/Zeta5/blob/2c80b320d06b4395605edbd413649d19094507af/Apery/Main.lean#L26.
\(\zeta(5)\) is irrational.
[Fa26] A. Fauzan (2026). \(\zeta(5)\) is irrational. Preprint, 17 September 2026.
theorem irrational_five : ∃ x, Irrational x ∧ riemannZeta 5 = x
Category research solved; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/RiemannZetaValues.lean, line 42.
RiemannZetaValues.irrational_seven
Open: stated without proof.
\(\zeta(7)\) is irrational.
theorem irrational_seven : ∃ x, Irrational x ∧ riemannZeta 7 = x
Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/RiemannZetaValues.lean, line 49.
RiemannZetaValues.irrational_nine
Open: stated without proof.
\(\zeta(9)\) is irrational.
theorem irrational_nine : ∃ x, Irrational x ∧ riemannZeta 9 = x
Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/RiemannZetaValues.lean, line 56.
RiemannZetaValues.irrational_eleven
Open: stated without proof.
\(\zeta(11)\) is irrational.
theorem irrational_eleven : ∃ x, Irrational x ∧ riemannZeta 11 = x
Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/RiemannZetaValues.lean, line 63.
RiemannZetaValues.irrational_odd
Open: stated without proof.
\(\zeta(2n + 1)\) is irrational for any \(n\in\mathbb{N}^{+}\).
theorem irrational_odd (n : ℕ) (hn : 0 < n) :
∃ x, Irrational x ∧ riemannZeta (2 * n + 1) = x
Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/RiemannZetaValues.lean, line 70.
RiemannZetaValues.irrational_three
Solved: stated here without proof.
\(\zeta(3)\) is irrational.
[Ap79] Apéry, R. (1979). Irrationalité de ζ(2) et ζ(3). Astérisque. 61: 11–13.
theorem irrational_three : ∃ x, Irrational x ∧ riemannZeta 3 = x
Category research solved; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/RiemannZetaValues.lean, line 80.
RiemannZetaValues.infinite_irrational_at_odd
Solved: stated here without proof.
There are infinitely many \(\zeta(2n + 1)\), \(n \in \mathbb{N}\), that are irrational.
[Ri00] Rivoal, T. (2000). La fonction zeta de Riemann prend une infinité de valeurs irrationnelles aux entiers impairs. Comptes Rendus de l'Académie des Sciences, Série I. 331 (4): 267–270.
theorem infinite_irrational_at_odd :
{ n : ℕ | ∃ x, Irrational x ∧ riemannZeta (2 * n + 1) = x }.Infinite
Category research solved; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/RiemannZetaValues.lean, line 89.
RiemannZetaValues.exists_irrational_of_five_seven_nine_eleven
Solved: stated here without proof.
At least one of \(\zeta(5), \zeta(7), \zeta(9)\) or \(\zeta(11)\) is irrational.
[Zu01] W. Zudilin (2001). One of the numbers ζ(5), ζ(7), ζ(9), ζ(11) is irrational. Russ. Math. Surv. 56 (4): 774–776.
theorem exists_irrational_of_five_seven_nine_eleven :
{5, 7, 9, 11} ∩ { a | ∃ x, Irrational x ∧ riemannZeta a = x} |>.Nonempty
Category research solved; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/RiemannZetaValues.lean, line 99.
Sources
TheoremRudin's conjecture on squares in arithmetic progressions#
References: - Wikipedia - [Ru60] Rudin, W., Trigonometric series with gaps, J. Math. Mech. 9 (1960), 203–227. - González-Jiménez, E. and Xarles, X., On a conjecture of Rudin on squares in arithmetic progressions, LMS J. Comput. Math. 17 (2014), 58–76.
Quoted from FormalConjectures/Wikipedia/RudinsConjecture.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: 3 open. It also has 3 test statements, counted here but not shown.
RudinsConjecture.rudins_conjecture
Open: stated without proof.
Rudin's conjecture. The maximal number of squares among the first \(N\) terms of a non-trivial arithmetic progression grows at most like \(\sqrt{N}\):
\[Q(N) = O(\sqrt{N}).\]
theorem rudins_conjecture :
(fun N : ℕ => (Qmax N : ℝ)) =O[atTop] fun N : ℕ => Real.sqrt N
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/RudinsConjecture.lean, line 101.
RudinsConjecture.rudins_conjecture_strong
Open: stated without proof.
A stronger form of Rudin's conjecture: for every \(N \ge 6\), the arithmetic progression \(24 n + 1\) attains the maximum \(Q(N)\).
theorem rudins_conjecture_strong (N : ℕ) (hN : 6 ≤ N) : Q N 24 1 = Qmax N
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/RudinsConjecture.lean, line 110.
RudinsConjecture.rudins_conjecture_unique
Open: stated without proof.
The strongest form of Rudin's conjecture also asserts uniqueness: for \(N \ge 6\), any non-trivial arithmetic progression attaining the maximum \(Q(N)\) has common difference \(24\). (Its initial term is then forced by \(\gcd(24, a) = 1\); the progression \(24n + 1\) is the canonical representative.)
theorem rudins_conjecture_unique (N : ℕ) (hN : 6 ≤ N) (q a : ℕ)
(hqa : IsNontrivial q a) (hmax : Q N q a = Qmax N) : q = 24
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/RudinsConjecture.lean, line 119.
Sources
TheoremSato–Tate conjecture#
The Sato–Tate conjecture describes the distribution of the normalized Frobenius traces \(a_p(E)/(2\sqrt{p})\) of a non-CM elliptic curve \(E\) over \(\mathbb{Q}\), as \(p\) ranges over the primes of good reduction: they equidistribute in \([-1,1]\) with respect to the Sato–Tate measure
\[ \frac{2}{\pi}\sqrt{1-x^2}\,dx. \]Originally conjectured independently by Mikio Sato and John Tate around 1960, it is now a theorem: the case of elliptic curves over totally real fields with nonintegral \(j\)-invariant was established through the work of Clozel, Harris, and Taylor [CHT08], Taylor [Tay08], and Harris, Shepherd-Barron, and Taylor [HST10]. The remaining non-CM case was settled by Barnet-Lamb, Geraghty, Harris, and Taylor [BGHT11]. In particular, it holds unconditionally for every non-CM elliptic curve over \(\mathbb{Q}\).
We use
ModularityConjecture.WeierstrassCurve.ap, which agrees with the Frobenius trace at every prime where the supplied Weierstrass equation has integral coefficients and nonsingular reduction. Only finitely many primes are exceptional. Including these primes does not change the limiting density, so the formal statement averages over all primes below \(N\).The non-CM hypothesis is expressed using the classification of rational CM \(j\)-invariants. Complex multiplication here means complex multiplication over \(\overline{\mathbb{Q}}\).
References
- [CHT08] L. Clozel, M. Harris, R. Taylor, Automorphy for some \(l\)-adic lifts of automorphic mod \(l\) Galois representations, Publications Mathématiques de l'IHÉS 108 (2008), 1–181. https://doi.org/10.1007/s10240-008-0016-1
- [Tay08] R. Taylor, Automorphy for some \(l\)-adic lifts of automorphic mod \(l\) Galois representations. II, Publications Mathématiques de l'IHÉS 108 (2008), 183–239. https://doi.org/10.1007/s10240-008-0015-2
- [HST10] M. Harris, N. Shepherd-Barron, R. Taylor, A family of Calabi-Yau varieties and potential automorphy, Annals of Mathematics 171 (2010), no. 2, 779–813. https://doi.org/10.4007/annals.2010.171.779
- [BGHT11] T. Barnet-Lamb, D. Geraghty, M. Harris, R. Taylor, A family of Calabi-Yau varieties and potential automorphy II, Publications of the Research Institute for Mathematical Sciences 47 (2011), no. 1, 29–98. https://doi.org/10.2977/PRIMS/31
- Wikipedia
Quoted from FormalConjectures/Wikipedia/SatoTateConjecture.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 solved. It also has 1 test statement, counted here but not shown.
SatoTateConjecture.satoTate_conjecture
Solved: stated here without proof.
The Sato–Tate conjecture: for a non-CM elliptic curve \(E\) over \(\mathbb{Q}\) and \(-1 \le a \le b \le 1\), the proportion of primes \(p < N\) whose normalized coefficient belongs to \([a,b]\) tends to
\[ \frac{2}{\pi}\int_a^b \sqrt{1-x^2}\,dx \]as \(N \to \infty\).
The finitely many primes where the supplied equation fails to have integral coefficients and nonsingular reduction do not affect this limit.
Established through the work of Clozel–Harris–Taylor [CHT08], Taylor [Tay08], Harris–Shepherd-Barron–Taylor [HST10], and Barnet-Lamb–Geraghty–Harris–Taylor [BGHT11].
theorem satoTate_conjecture
(E : WeierstrassCurve ℚ) [E.IsElliptic] (hCM : ¬ HasCM E)
(a b : ℝ) (ha : -1 ≤ a) (hab : a ≤ b) (hb : b ≤ 1) :
Filter.Tendsto
(fun N : ℕ ↦
(primeCountInInterval E a b N : ℝ) /
((Nat.primesBelow N).card : ℝ))
Filter.atTop
(nhds (satoTateMeasure a b))
Category research solved; AMS 11 Number theory, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/SatoTateConjecture.lean, line 169.
Sources
TheoremSchanuel's Conjecture#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/Schanuel.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.
Schanuel.schanuel_conjecture
Open: stated without proof.
Given any set of \(n\) complex numbers \(\{z_1, ..., z_n\}\) that are linearly independent over \(\mathbb{Q}\), the field extension \(\mathbb{Q}(z_1, ..., z_n, e^{z_1}, ..., e^{z_n})\) has transcendence degree at least \(n\) over \(\mathbb{Q}\).
theorem schanuel_conjecture (n : ℕ) (z : Fin n → ℂ) (h : LinearIndependent ℚ z) :
n ≤ Algebra.trdeg ℚ (adjoin ℚ (Set.range z ∪ Set.range (cexp ∘ z)))
Category research open; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Schanuel.lean, line 39.
Sources
TheoremHypothesis H#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/Schinzel.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.
Schinzel.schinzel_conjecture
Open: stated without proof.
Schinzel conjecture (H hypothesis) If a finite set of polynomials \(f_i\) satisfies both Schinzel and Bunyakovsky conditions, there exist infinitely many natural numbers \(n\) such that \(f_i(n)\) are primes for all \(i\).
theorem schinzel_conjecture (fs : Finset ℤ[X]) (hfs : ∀ f ∈ fs, BunyakovskyCondition f)
(hfs' : SchinzelCondition fs) : Infinite {n : ℕ | ∀ f ∈ fs, (f.eval (n : ℤ)).natAbs.Prime}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Schinzel.lean, line 37.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.