The Lovász–Plummer conjecture… to The Petersen colouring…
TheoremThe Lovász–Plummer conjecture (proved 2011) and Sheehan's conjecture#
References: * Wikipedia * [LP86] Lovász, L. and Plummer, M. D. (1986). Matching Theory. North-Holland. * [EKKKN11] Esperet, L., Kardoš, F., King, A. D., Král', D. and Norine, S. (2011). "Exponentially many perfect matchings in cubic graphs." Adv. Math. 227, pp. 1646--1664. arXiv:1012.2878 * [Sh77] Sheehan, J. (1977). "The multiplicity of Hamiltonian circuits in a graph." In Recent Advances in Graph Theory, Academia, Prague, pp. 477--480. * [Th98] Thomassen, C. (1998). "Independent dominating sets and a second Hamiltonian cycle in regular graphs." J. Combin. Theory Ser. B 72, pp. 104--109.
Quoted from FormalConjectures/Wikipedia/LovaszPlummerConjecture.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 and 3 solved.
LovaszPlummerConjecture.lovasz_plummer_conjecture
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/da6d56610c43a6eadd15945a3b80a62f223293f8/Proofs/T_LovaszPlummerConjecture_lovasz_plummer_conjecture.lean#L16602.
The Lovász–Plummer conjecture (1970s), proved by Esperet, Kardoš, King, Král' and Norine (2011).
Every bridgeless cubic graph on \(n\) vertices has exponentially many perfect matchings: there is a constant \(c > 0\) such that the number of perfect matchings is at least \(2^{cn}\). [EKKKN11] prove this with \(2^{n/3656}\).
theorem lovasz_plummer_conjecture :
∃ c : ℝ, 0 < c ∧ ∀ {V : Type} [Fintype V] [DecidableEq V]
(G : SimpleGraph V) [DecidableRel G.Adj],
(∀ v, G.degree v = 3) → G.IsBridgeless →
(2 : ℝ) ^ (c * Fintype.card V) ≤ perfectMatchingCount G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/LovaszPlummerConjecture.lean, line 57.
LovaszPlummerConjecture.lovasz_plummer_conjecture.variants.explicit
Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/e1059f02264088e9fc4e2866855b8cf68d9cbeda/Proofs/T_LovaszPlummerConjecture_lovasz_plummer_conjecture_variants_explicit.lean#L34280.
The explicit bound of Esperet–Kardoš–King–Král'–Norine (2011).
Every bridgeless cubic graph on \(n\) vertices has at least \(2^{n/3656}\) perfect matchings.
Reference: [EKKKN11].
theorem lovasz_plummer_conjecture.variants.explicit
{V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
(hcubic : ∀ v, G.degree v = 3) (hbridgeless : G.IsBridgeless) :
(2 : ℝ) ^ ((Fintype.card V : ℝ) / 3656) ≤ perfectMatchingCount G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/LovaszPlummerConjecture.lean, line 73.
LovaszPlummerConjecture.sheehan_conjecture
Open: stated without proof.
Sheehan's conjecture (1977).
Every \(4\)-regular graph with a Hamiltonian cycle has a second Hamiltonian cycle (one with a different edge set). Sheehan's conjecture would settle the last open case of the question, raised by Smith's theorem for cubic graphs, of which regular Hamiltonian graphs have a second Hamiltonian cycle: Thomassen [Th98] proved it for all \(r\)-regular graphs with \(r \ge 300\).
theorem sheehan_conjecture :
∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
(∀ v, G.degree v = 4) →
∀ (v : V) (c : G.Walk v v), IsHamiltonianCycle G c →
∃ (w : V) (c' : G.Walk w w), IsHamiltonianCycle G c' ∧
c'.edges.toFinset ≠ c.edges.toFinset
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/LovaszPlummerConjecture.lean, line 92.
LovaszPlummerConjecture.sheehan_conjecture.variants.thomassen
Solved: stated here without proof.
Thomassen (1998): regular graphs of large degree.
Every \(r\)-regular Hamiltonian graph with \(r \ge 300\) has a second Hamiltonian cycle.
Reference: [Th98].
theorem sheehan_conjecture.variants.thomassen
{V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
(r : ℕ) (hr : 300 ≤ r) (hreg : ∀ v, G.degree v = r)
(v : V) (c : G.Walk v v) (hc : IsHamiltonianCycle G c) :
∃ (w : V) (c' : G.Walk w w), IsHamiltonianCycle G c' ∧
c'.edges.toFinset ≠ c.edges.toFinset
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/LovaszPlummerConjecture.lean, line 108.
Sources
TheoremLychrel numbers in base 10#
A (base-10) Lychrel number is a positive integer which never becomes a palindrome under the iteration
\[a_{0} = n, \qquad a_{k+1} = a_k + \operatorname{rev}_{10}(a_k).\]One commonly stated conjectural direction is that there are no Lychrel numbers in base 10. The smallest widely studied open case is
196.References: * Wikipedia: Lychrel number * MathWorld: Lychrel Number * OEIS A023108 * OEIS A023109
Quoted from FormalConjectures/Wikipedia/LychrelNumbers.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 4 test statements and 1 API statement, counted here but not shown.
LychrelNumbers.no_lychrel_numbers_base10
Open: stated without proof.
Lychrel conjecture (base 10): conjecturally, there are no Lychrel numbers in base 10.
Equivalently, every positive integer eventually becomes a palindrome under the Lychrel iteration.
theorem no_lychrel_numbers_base10 :
∀ n : ℕ, 0 < n → ¬ IsLychrel10 n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LychrelNumbers.lean, line 74.
LychrelNumbers.isLychrel10_196
Open: stated without proof.
The first widely studied open case: whether
196is a base-10 Lychrel number.
theorem isLychrel10_196 : IsLychrel10 196
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LychrelNumbers.lean, line 82.
Sources
TheoremMagic Squares#
References:
Quoted from FormalConjectures/Wikipedia/MagicSquares.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.
MagicSquares.exists_magic_square_squares
Open: stated without proof.
Does there exist a \(3 \times 3\) matrix such that every entry is a distinct square, and all rows, columns, and diagonals add up to the same value?
0 is excluded, as a Magic Square of Squares with 0 and 8 distinct squares is know is knownn. See Magic Square of Squares
theorem exists_magic_square_squares :
∃ m : Fin 3 → Fin 3 → ℕ, ∃ t : ℕ,
m.Injective2 ∧
(∀ i j, 0 < (m i j) ∧ IsSquare (m i j)) ∧
(∀ i, ∑ j, m i j = t) ∧
(∀ j, ∑ i, m i j = t) ∧
m 0 0 + m 1 1 + m 2 2 = t ∧
m 0 2 + m 1 1 + m 2 0 = t
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/MagicSquares.lean, line 43.
MagicSquares.exists_semi_magic_square_cubes
Open: stated without proof.
Does there exist a \(3 \times 3\) semi-magic square whose entries are all distinct positive integer cubes? A square is semi-magic if all rows and columns sum to the same total.
More precisely, we seek a \(3 \times 3\) matrix with entries \(a_{ij}\) such that each \(a_{ij} = n_{ij}^3\) for some positive integer \(n_{ij}\), all nine cubes are distinct, and all row sums and column sums are equal.
Reference: Semi-Magic Square of Cubes
theorem exists_semi_magic_square_cubes :
∃ m : Fin 3 → Fin 3 → ℕ, ∃ t : ℕ,
m.Injective2 ∧
(∀ i j, ∃ n : ℕ, 0 < n ∧ m i j = n ^ 3) ∧
(∀ i, ∑ j, m i j = t) ∧
(∀ j, ∑ i, m i j = t)
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/Wikipedia/MagicSquares.lean, line 65.
Sources
TheoremMahler's 3/2 Problem#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/Mahler32.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, 1 solved and 1 textbook result.
Mahler32.mahler_conjecture
Open: stated without proof.
The Mahler Conjecture states that there are no Z-numbers.
theorem mahler_conjecture (x : ℝ) (hx : IsZNumber x) : False
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Mahler32.lean, line 42.
Mahler32.mahler_conjecture.variants.consequence
Textbook result, stated without proof.
Mahler's conjecture would follow if
Ω(3/2)exceeded1/2: a Z-numberxhas all fractional parts{x (3/2)^n}below1/2, soΩ(3/2) ≤ 1/2.
theorem mahler_conjecture.variants.consequence (H : 1 / 2 < Ω (3 / 2)) :
type_of% mahler_conjecture
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Mahler32.lean, line 48.
Mahler32.mahler_conjecture.variants.flatto_lagarias_pollington
Solved: stated here without proof.
Flatto, Lagarias and Pollington proved that for all rational
p/q > 1in lowest terms withq ≥ 2, we haveΩ(p/q) ≥ 1/p: for everyθ > 0, the limit points of{θ (p/q)^n}are not contained in any interval of length less than1/p.
theorem mahler_conjecture.variants.flatto_lagarias_pollington (p q : ℕ) (hq : 1 < q)
(hpq : p.Coprime q) (hpq' : q < p) : 1 / p ≤ Ω (p / q)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Mahler32.lean, line 56.
Sources
TheoremConjectures about the Mandelbrot and Multibrot sets#
This file adds three conjectures about the Mandelbrot and Multibrot sets: - the MLC conjecture, stating that these sets are locally connected - the density of hyperbolicity conjecture, stating that parameters with attracting cycles are dense in the Mandelbrot and Multibrot sets - the conjecture that the boundaries of these sets have zero area. The first two conjectures are related in that the former implies the latter.
References: - Wikipedia - arxiv/math/9902155 - mathoverflow/37229
Quoted from FormalConjectures/Wikipedia/Mandelbrot.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: 6 open. It also has 4 test statements and 2 API statements, counted here but not shown.
Mandelbrot.MLC
Open: stated without proof.
The MLC conjecture, stating that the mandelbrot set is locally connected.
theorem MLC : LocallyConnectedSpace mandelbrotSet
Category research open; AMS 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Wikipedia/Mandelbrot.lean, line 111.
Mandelbrot.MLC_general_exponent
Open: stated without proof.
A stronger version of the MLC conjecture, stating that all multibrots are locally connected. Note that we don't need to require
2 ≤ nbecause the conjecture holds in the trivial casesn = 0andn = 1too.
theorem MLC_general_exponent (n : ℕ) : LocallyConnectedSpace (multibrotSet n)
Category research open; AMS 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Wikipedia/Mandelbrot.lean, line 118.
Mandelbrot.density_of_hyperbolicity
Open: stated without proof.
The density of hyperbolicity conjecture, stating that the set of all parameters
cfor whichfun z ↦ z ^ 2 + chas an attracting cycle is dense in the Mandelbrot set.
theorem density_of_hyperbolicity :
mandelbrotSet ⊆ closure {c | ∃ m z, IsAttractingCycle (fun z ↦ z ^ 2 + c) m z}
Category research open; AMS 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Wikipedia/Mandelbrot.lean, line 147.
Mandelbrot.density_of_hyperbolicity_general_exponent
Open: stated without proof.
The density of hyperbolicity conjecture for Multibrot sets, stating that the set of all parameters
cfor whichfun z ↦ z ^ n + chas an attracting cycle is dense inmultibrotSet n. Note that we need to require2 ≤ nbecause the conjecture is trivially false forn = 1.
theorem density_of_hyperbolicity_general_exponent {n : ℕ} (hn : 2 ≤ n) :
multibrotSet n ⊆ closure {c | ∃ m z, IsAttractingCycle (fun z ↦ z ^ n + c) m z}
Category research open; AMS 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Wikipedia/Mandelbrot.lean, line 155.
Mandelbrot.volume_frontier_mandelbrotSet_eq_zero
Open: stated without proof.
The boundary of the Mandelbrot set is conjectured to have zero area.
theorem volume_frontier_mandelbrotSet_eq_zero : volume (frontier mandelbrotSet) = 0
Category research open; AMS 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Wikipedia/Mandelbrot.lean, line 166.
Mandelbrot.volume_frontier_multibrotSet_eq_zero
Open: stated without proof.
The boundary of any Multibrot set is conjectured to have zero area. Note that we don't need to exclude the trivial cases
n = 0andn = 1because the conjecture holds for them.
theorem volume_frontier_multibrotSet_eq_zero {n : ℕ} : volume (frontier (multibrotSet n)) = 0
Category research open; AMS 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Wikipedia/Mandelbrot.lean, line 173.
Sources
LemmaMean value problem#
Reference: - Wikipedia - The fundamental theorem of algebra and complexity theory by Steve Smale
Given a complex polynomial \(p\) of degree \(d ≥ 2\) and a complex number \(z\) there is a critical point \(c\) of \(p\), such that \(|p(z)-p(c)|/|z-c| ≤ K* |p'(z)|\) for \(K=1\).
The conjecture has been proven for: *
K = 4The fundamental theorem of algebra and complexity theory by Steve Smale *K = (d-1)/dat a point \(z\) if the normalised polynomial \(p(X + z) - p(z)\) has only real roots, or if all its nonzero roots have the same norm. Critical points and values of complex polynomials by David Tischler
Quoted from FormalConjectures/Wikipedia/MeanValueProblem.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 and 3 solved.
MeanValueProblem.mean_value_problem
Open: stated without proof.
Given a complex polynomial \(p\) of degree \(d ≥ 2\) and a complex number \(z\) there is a critical point \(c\) of \(p\), such that \(|p(z)-p(c)|/|z-c| ≤ |p'(z)|\).
lemma mean_value_problem (p : Polynomial ℂ) (hp : 2 ≤ p.degree) (z : ℂ) (K : ℝ):
∃ c : ℂ, p.derivative.eval c = 0 ∧
‖p.eval z - p.eval c‖ / ‖z - c‖ ≤ ‖p.derivative.eval z‖
Category research open; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/MeanValueProblem.lean, line 52.
MeanValueProblem.mean_value_problem_leq_4
Solved: stated here without proof.
The following weaker version of the mean value problem has been proven. Given a complex polynomial \(p\) of degree \(d ≥ 2\) and a complex number \(z\) there a critical point \(c\) of \(p\), such that \(|p(z)-p(c)|/|z-c| ≤ 4|p'(z)|\).
lemma mean_value_problem_leq_4 (p : Polynomial ℂ) (hp : 2 ≤ p.degree) (z : ℂ) (K : ℝ):
∃ c : ℂ, p.derivative.eval c = 0 ∧
‖p.eval z - p.eval c‖ / ‖z - c‖ ≤ 4 *‖p.derivative.eval z‖
Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/MeanValueProblem.lean, line 63.
MeanValueProblem.mean_value_problem_of_real_roots
Solved: stated here without proof.
The following tighter bound depending on the degree \(d\) of the polynomial \(p\) has been shown by Tischler. Let \(z\) be a complex number such that the normalised polynomial \(p(X + z) - p(z)\) has only real roots, i.e. every \(x\) with \(p(x) = p(z)\) satisfies \(\operatorname{Im} x = \operatorname{Im} z\). Then there is a critical point \(c\) of \(p\) such that \(|p(z)-p(c)|/|z-c| \le (d-1)/d \cdot |p'(z)|\).
lemma mean_value_problem_of_real_roots (p : Polynomial ℂ) (hp : 2 ≤ p.natDegree) (z : ℂ)
(h : ∀ x : ℂ, p.eval x = p.eval z → x.im = z.im) (K : ℝ) :
∃ c : ℂ, p.derivative.eval c = 0 ∧
‖p.eval z - p.eval c‖ / ‖z - c‖ ≤ (p.natDegree - 1)/ p.natDegree * ‖p.derivative.eval z‖
Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/MeanValueProblem.lean, line 77.
MeanValueProblem.mean_value_problem_of_roots_same_norm
Solved: stated here without proof.
The following tighter bound depending on the degree \(d\) of the polynomial \(p\) has been shown by Tischler. Let \(z\) be a complex number such that all nonzero roots of the normalised polynomial \(p(X + z) - p(z)\) have the same norm, i.e. all \(x \ne z\) with \(p(x) = p(z)\) have the same distance to \(z\). Then there is a critical point \(c\) of \(p\) such that \(|p(z) - p(c)|/|z-c| \le (d-1)/d \cdot |p'(z)|\).
lemma mean_value_problem_of_roots_same_norm (p : Polynomial ℂ) (hp : 2 ≤ p.natDegree) (z : ℂ)
(h : ∀ x y : ℂ, p.eval x = p.eval z → p.eval y = p.eval z → x ≠ z → y ≠ z →
‖x - z‖ = ‖y - z‖) (K : ℝ) :
∃ c : ℂ, p.derivative.eval c = 0 ∧
‖p.eval z - p.eval c‖ / ‖z - c‖ ≤ (p.natDegree - 1)/ p.natDegree * ‖p.derivative.eval z‖
Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/MeanValueProblem.lean, line 92.
Sources
TheoremConjectures about Mersenne primes#
References: - Wikipedia: Mersenne conjectures - Wikipedia: Catalan's Mersenne conjecture - MathWorld: Catalan-Mersenne Number
Quoted from FormalConjectures/Wikipedia/Mersenne.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: 4 open and 1 textbook result.
Mersenne.new_mersenne_conjecture
Open: stated without proof.
For any odd natural number
pif two of the following conditions hold, then all three must hold: 1. \(2^p-1\) is prime 2. \((2^p+1)/3\) is prime 3. Exists a numberksuch that \(p = 2^k \\pm 1\) or \(p = 4^k \\pm 3\)
theorem new_mersenne_conjecture (p : ℕ) (hp : Odd p) :
NewMersenneConjectureStatement p
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Mersenne.lean, line 80.
Mersenne.new_mersenne_conjecture_of_prime
Textbook result, proved here.
It suffices to check this conjecture for odd primes. The statement fails at
p = 2:mersenne 2 = 3is prime and2 = 2 ^ 0 + 1, but2gives no Wagstaff prime.
theorem new_mersenne_conjecture_of_prime :
(∀ p, p.Prime → Odd p → NewMersenneConjectureStatement p) →
∀ p, Odd p → NewMersenneConjectureStatement p
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Mersenne.lean, line 87.
Mersenne.new_mersenne_conjecture.variants.prime
Open: stated without proof.
The New Mersenne Conjecture statement holds for odd primes.
theorem new_mersenne_conjecture.variants.prime (p : ℕ) (hp : p.Prime) (h : Odd p) :
NewMersenneConjectureStatement p
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Mersenne.lean, line 127.
Mersenne.infinitely_many_mersenne_primes
Open: stated without proof.
Are there infinitely many Mersenne primes?
theorem infinitely_many_mersenne_primes :
Set.Infinite { p : ℕ | (mersenne p).Prime }
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Mersenne.lean, line 135.
Mersenne.catalans_mersenne_conjecture
Open: stated without proof.
The first five Catalan-Mersenne numbers \(c_0, \ldots, c_4\) are known to be prime. Catalan conjectured that they are prime "up to a certain limit". Are all Catalan-Mersenne numbers \(c_n\) with \(n \geq 5\) prime?
theorem catalans_mersenne_conjecture :
∀ n ≥ 5, Nat.Prime (catalanMersenne n)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Mersenne.lean, line 145.
Sources
TheoremMeyniel's conjecture on the cop number#
References: * Wikipedia * [Fr87] Frankl, P. (1987). "Cops and robbers in graphs with large girth and Cayley graphs." Discrete Appl. Math. 17, pp. 301--305. * [NW83] Nowakowski, R. and Winkler, P. (1983). "Vertex-to-vertex pursuit in a graph." Discrete Math. 43, pp. 235--239. * [SS11] Scott, A. and Sudakov, B. (2011). "A bound for the cops and robbers problem." SIAM J. Discrete Math. 25, pp. 1438--1442. * [BB12] Baird, W. and Bonato, A. (2012). "Meyniel's conjecture on the cop number: a survey." J. Comb. 3, pp. 225--238.
Quoted from FormalConjectures/Wikipedia/MeynielConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 4 research or textbook statements: 2 open and 2 solved. It also has 2 test statements and 4 API statements, counted here but not shown.
MeynielConjecture.meyniel_conjecture
Open: stated without proof.
Meyniel's conjecture (c. 1985).
There is a universal constant
Csuch that every connected graph onnvertices has cop number at mostC √n: a team ofO(√n)cops can always catch the robber in the game of cops and robbers. The conjecture was communicated by Meyniel to Frankl and first appeared in [Fr87]; see [BB12] for a survey.
theorem meyniel_conjecture :
∃ C : ℝ, 0 < C ∧ ∀ (V : Type) [Fintype V] (G : SimpleGraph V), G.Connected →
(copNumber G : ℝ) ≤ C * Real.sqrt (Fintype.card V)
Category research open; AMS 05 Combinatorics, 91 Game theory, economics, social and behavioral sciences. Declared in FormalConjectures/Wikipedia/MeynielConjecture.lean, line 113.
MeynielConjecture.meyniel_conjecture.variants.soft
Open: stated without proof.
The soft Meyniel conjecture.
There are constants
ε, C > 0such that every connected graph onnvertices has cop number at mostC n^(1 - ε). Even this weakening of Meyniel's conjecture is open; no bound of the formO(n^(1 - ε))is known. See [BB12].
theorem meyniel_conjecture.variants.soft :
∃ ε C : ℝ, 0 < ε ∧ 0 < C ∧ ∀ (V : Type) [Fintype V] (G : SimpleGraph V), G.Connected →
(copNumber G : ℝ) ≤ C * (Fintype.card V : ℝ) ^ ((1 : ℝ) - ε)
Category research open; AMS 05 Combinatorics, 91 Game theory, economics, social and behavioral sciences. Declared in FormalConjectures/Wikipedia/MeynielConjecture.lean, line 126.
MeynielConjecture.meyniel_conjecture.variants.scott_sudakov
Solved: stated here without proof.
Scott–Sudakov (2011): the best known general bound.
Every connected graph on
nvertices has cop number at mostn / 2^((1 - o(1)) √(log₂ n)). This (together with the same bound obtained independently by Lu–Peng and by Frieze, Krivelevich and Loh) is the best known bound towards Meyniel's conjecture.Reference: [SS11].
theorem meyniel_conjecture.variants.scott_sudakov :
∃ f : ℕ → ℝ, Tendsto f atTop (nhds 0) ∧
∀ (V : Type) [Fintype V] (G : SimpleGraph V), G.Connected →
(copNumber G : ℝ) ≤ (Fintype.card V : ℝ) /
2 ^ ((1 - f (Fintype.card V)) * Real.sqrt (Real.logb 2 (Fintype.card V)))
Category research solved; AMS 05 Combinatorics, 91 Game theory, economics, social and behavioral sciences. Declared in FormalConjectures/Wikipedia/MeynielConjecture.lean, line 141.
MeynielConjecture.meyniel_conjecture.variants.tree
Solved: stated here without proof.
Trees are cop-win (Nowakowski–Winkler 1983).
Every nonempty tree has cop number
1: a single cop, always moving towards the robber, catches the robber on any connected acyclic graph. More generally, the cop-win graphs are exactly the dismantlable graphs.Reference: [NW83].
theorem meyniel_conjecture.variants.tree {V : Type} [Fintype V] [Nonempty V]
(G : SimpleGraph V) (hc : G.Connected) (ha : G.IsAcyclic) :
copNumber G = 1
Category research solved; AMS 05 Combinatorics, 91 Game theory, economics, social and behavioral sciences. Declared in FormalConjectures/Wikipedia/MeynielConjecture.lean, line 158.
Sources
TheoremMills' Theorem#
There exists a real \(A > 1\) such that \(\lfloor A^{3^n}\rfloor\) is prime for every positive integer \(n\), where \(\lfloor\cdot\rfloor\) denotes the floor function.
The least such \(A\) is known as Mills' constant. It is irrational, and assuming the Riemann hypothesis it is approximately \(1.3063778838\ldots\).
References: - Wikipedia, Mills' constant - A prime-representing function by W. H. Mills, Bull. Amer. Math. Soc. 53 (1947), 604. - Mills' constant on Wolfram MathWorld. - Mills' constant is irrational by Kota Saito, Mathematika 71 (2025), no. 3, e70027, arXiv:2404.19461. - Determining Mills' Constant .. by Chris K. Caldwell and Yuanyou Cheng, J. Integer Seq. 8 (2005), Article 05.4.1. - OEIS A051021 (decimal expansion of Mills' constant)
Quoted from FormalConjectures/Wikipedia/Mills.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 solved.
Mills.exists'
Solved: stated here without proof.
Mills' theorem (Mills, 1947). There is a real number \(A > 1\) such that \(\lfloor A^{3^n}\rfloor\) is prime.
theorem exists' : ∃ A > 1, IsMills A
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Mills.lean, line 56.
Mills.exists_least
Solved: stated here without proof.
Mills' constant. There is a least Mills number.
theorem exists_least : ∃ A, IsMinMills A
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Mills.lean, line 69.
Mills.irrational
Solved: stated here without proof.
Mills' constant is irrational (Saito, 2024).
theorem irrational {A} (hA : IsMinMills A) :
Irrational A
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Mills.lean, line 76.
Mills.lower_bound_of_RH
Solved: stated here without proof.
Mills' constant lower bound (Caldwell–Cheng, 2005): assuming the Riemann hypothesis, Mills' constant begins at \(1.3063778838\ldots\).
theorem lower_bound_of_RH (hRH : RiemannHypothesis) {A} (hA : IsMinMills A) :
A ∈ Set.Ioo (1.3063778838 : ℝ) 1.3063778839
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Mills.lean, line 85.
Sources
TheoremModularity conjecture#
The Modularity conjecture (also known as the Shimura-Taniyama-Weil conjecture) states that every rational elliptic curve is modular, meaning that it can be associated with a modular form. We state the
a_pversion of the conjecture, which relates the coefficients of the modular form to the number of points on the elliptic curve over finite fields.Since we don't have the conductor of the elliptic curve, our definition of
a_p(E)differs from that in the literature at primes of bad reduction. For this reason, we state the conjecture with the assumption thatp ∤ N, in order to give an equivalent statement.References: - Wikipedia - F. Diamond and J. Shurman, A First Course in Modular Forms
Quoted from FormalConjectures/Wikipedia/ModularityConjecture.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.
ModularityConjecture.modularity_conjecture
Solved: stated here without proof.
The Modularity Theorem (formerly Shimura-Taniyama-Weil conjecture): every elliptic curve over \(\mathbb{Q}\) is modular.
theorem modularity_conjecture (E : WeierstrassCurve ℚ) [E.IsElliptic] : modularityConjecture E
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ModularityConjecture.lean, line 93.
Sources
TheoremMoser's Worm#
References: - Wikipedia - Tao's optimization constant 13a
Quoted from FormalConjectures/Wikipedia/MoserWorm.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: 2 open, 4 solved and 1 textbook result.
MoserWorm.disc_mem_worm_covers
Textbook result, proved here.
A disc of radius 1 / 2 is a worm cover.
This follows by translating the center of the disc to the midpoint of the worm.
theorem disc_mem_worm_covers : Metric.closedBall 0 0.5 ∈ WormCovers
Category textbook; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/MoserWorm.lean, line 55.
MoserWorm.mosers_worm_problem
Open: stated without proof.
Moser's Worm Problem What is the minimal area (or greatest lower bound on the area) of a shape that can cover every unit-length curve?
theorem mosers_worm_problem :
IsGLB {v | ∃ X ∈ WormCovers, volume X = v} mosers_worm_problem.answer
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/MoserWorm.lean, line 80.
MoserWorm.mosers_worm_problem_upper_bound
Solved: stated here without proof.
There is a set of area 0.260437 that covers all worms.
Reference: Norwood, Rick; Poole, George (2003), "An improved upper bound for Leo Moser's worm problem", Discrete and Computational Geometry, 29 (3): 409–417, doi:10.1007/s00454-002-0774-3, MR 1961007.
theorem mosers_worm_problem_upper_bound :
∃ X ∈ WormCovers, volume X = 0.260437
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/MoserWorm.lean, line 92.
MoserWorm.convex_mosers_worm_problem
Open: stated without proof.
Convex Moser's Worm Problem What is the minimal area (or greatest lower bound on the area) of a convex shape that can cover every unit-length curve?
theorem convex_mosers_worm_problem :
convexWormCoverConstant = convex_mosers_worm_problem.answer
Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/MoserWorm.lean, line 110.
MoserWorm.convex_mosers_worm_problem_bound_attained
Solved: stated here without proof.
The minimal area of a convex shape that can cover every unit-length curve is attained. This follows from the Blaschke selection theorem.
theorem convex_mosers_worm_problem_bound_attained :
∃ X ∈ WormCovers, Convex ℝ X ∧ volume X = convexWormCoverConstant
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/MoserWorm.lean, line 119.
MoserWorm.convex_mosers_worm_problem_upper_bound
Solved: stated here without proof.
There is a convex set of area 0.270911861 that covers all worms.
Reference: Wang, Wei (2006), "An improved upper bound for the worm problem", Acta Mathematica Sinica, 49 (4): 835–846, MR 2264090.
theorem convex_mosers_worm_problem_upper_bound :
∃ X ∈ WormCovers, Convex ℝ X ∧ volume X = 0.270911861
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/MoserWorm.lean, line 131.
MoserWorm.convex_mosers_worm_problem_lower_bound
Solved: stated here without proof.
0.232239 is a lower bound on the area of a convex set that covers all worms.
Reference: Khandhawit, Tirasan; Pagonakis, Dimitrios; Sriswasdi, Sira (2013), "Lower Bound for Convex Hull Area and Universal Cover Problems", International Journal of Computational Geometry & Applications, 23 (3): 197–212, arXiv:1101.5638, doi:10.1142/S0218195913500076, MR 3158583, S2CID 207132316.
theorem convex_mosers_worm_problem_lower_bound :
0.232239 ≤ convexWormCoverConstant
Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/MoserWorm.lean, line 145.
Sources
TheoremMoving Sofa Problem#
References: - Wikipedia - [Ge92] Gerver, J. L., On moving a sofa around a corner. Geometriae Dedicata 42.3 (1992): 267-283. - [Ro18] Romik, D. Differential equations and exact solutions in the moving sofa problem. Experimental mathematics 27.3 (2018): 316-330. - [Ba24] Baek, J. Optimality of Gerver's Sofa. arXiv preprint arXiv:2411.19826 (2024).
Quoted from FormalConjectures/Wikipedia/MovingSofa.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: 4 solved and 1 textbook result. It also has 3 test statements, counted here but not shown.
MovingSofa.GerversSofa.ABφθSpec.existsUnique
Textbook result, stated without proof. A Lean proof is at https://github.com/RuifengCao/sofa-formal/blob/838baca722560f30ea8e60b8c711b20147626175/SofaSubmission/Defs.lean#L173; a Lean proof is at https://github.com/dawidmtrela-dotcom/GerverSofaLean/blob/v1.0.0/GerverSofa/KernelOnly/PartE/E24KC6KernelFinalClosure.lean.
There exist unique constants \(A\), \(B\), \(\varphi\), and \(\theta\) satisfying the spec.
theorem ABφθSpec.existsUnique : ∃! ABφθ : ℝ × ℝ × ℝ × ℝ,
ABφθSpec ABφθ.1 ABφθ.2.1 ABφθ.2.2.1 ABφθ.2.2.2
Category textbook; AMS 49 Calculus of variations and optimal control; optimization. Declared in FormalConjectures/Wikipedia/MovingSofa.lean, line 164.
MovingSofa.isMovingSofa_gerversSofa
Solved: stated here; a Lean proof is at https://github.com/dawidmtrela-dotcom/GerverSofaLean/releases/tag/v1.1.0; a Lean proof is at https://github.com/RuifengCao/sofa-formal/blob/838baca722560f30ea8e60b8c711b20147626175/SofaSubmission/Solution.lean#L20; a Lean proof is at https://github.com/vltanh/lean4-moving-sofa/blob/16653ae81e0e4f52a362bafae2ad3440100ad065/Solution.lean#L161-L168; a Lean proof is at https://github.com/vltanh/lean4-moving-sofa/blob/0addd87e5a0a4550ab8a60019180f012167fa24f/Solution.lean#L120-L121.
Gerver's concrete sofa admits a valid hallway motion.
theorem isMovingSofa_gerversSofa : ∃ m, IsMovingSofa gerversSofa m
Category research solved; AMS 49 Calculus of variations and optimal control; optimization. Declared in FormalConjectures/Wikipedia/MovingSofa.lean, line 212.
MovingSofa.sofaConstant_eq
Solved: stated here; a Lean proof is at https://github.com/deancureton/MovingSofa/blob/a0753860f1d2b4424e059c35e64ad611be71a415/MovingSofaSubmission/Solution.lean#L20; a Lean proof is at https://github.com/RuifengCao/sofa-formal/blob/838baca722560f30ea8e60b8c711b20147626175/SofaSubmission/Solution.lean#L26; a Lean proof is at https://github.com/vltanh/lean4-moving-sofa/blob/16653ae81e0e4f52a362bafae2ad3440100ad065/Solution.lean#L171-L173; a Lean proof is at https://github.com/vltanh/lean4-moving-sofa/blob/0addd87e5a0a4550ab8a60019180f012167fa24f/Solution.lean#L124-L125.
What is the sofa constant?
theorem sofaConstant_eq : sofaConstant = sofaConstant_eq.answer
Category research solved; AMS 49 Calculus of variations and optimal control; optimization. Declared in FormalConjectures/Wikipedia/MovingSofa.lean, line 238.
MovingSofa.sofaConstant_eq_volume_gerversSofa
Solved: stated here; a Lean proof is at https://github.com/deancureton/MovingSofa/blob/a0753860f1d2b4424e059c35e64ad611be71a415/MovingSofaSubmission/Solution.lean#L20; a Lean proof is at https://github.com/RuifengCao/sofa-formal/blob/838baca722560f30ea8e60b8c711b20147626175/SofaSubmission/Solution.lean#L30; a Lean proof is at https://github.com/vltanh/lean4-moving-sofa/blob/16653ae81e0e4f52a362bafae2ad3440100ad065/Solution.lean#L171-L173; a Lean proof is at https://github.com/vltanh/lean4-moving-sofa/blob/0addd87e5a0a4550ab8a60019180f012167fa24f/Solution.lean#L124-L125.
Gerver's sofa attains the sofa constant, conjectured by [Ge92] and claimed by [Ba24].
theorem sofaConstant_eq_volume_gerversSofa : sofaConstant = volume gerversSofa
Category research solved; AMS 49 Calculus of variations and optimal control; optimization. Declared in FormalConjectures/Wikipedia/MovingSofa.lean, line 248.
MovingSofa.volume_eq_sofaConstant_iff_congruent_gerversSofa
Solved: stated here; a Lean proof is at https://github.com/vltanh/lean4-moving-sofa/blob/16653ae81e0e4f52a362bafae2ad3440100ad065/Solution.lean#L176-L190; a Lean proof is at https://github.com/vltanh/lean4-moving-sofa/blob/0addd87e5a0a4550ab8a60019180f012167fa24f/Solution.lean#L128-L131.
Gerver's sofa is the unique sofa that attains the sofa constant, up to a rigid motion.
The motion is needed:
horizontalHallwayis \((-\infty, 1] \times [0, 1]\), so a leftward translate of any moving sofa is again one, obtained by sliding right and then following the original motion. It has the same area, so uniqueness cannot hold on the nose.
theorem volume_eq_sofaConstant_iff_congruent_gerversSofa (s : Set ℝ²)
(hs : ∃ m, IsMovingSofa s m) :
volume s = sofaConstant ↔ ∃ g : E(2), s = g '' gerversSofa
Category research solved; AMS 49 Calculus of variations and optimal control; optimization. Declared in FormalConjectures/Wikipedia/MovingSofa.lean, line 262.
Sources
TheoremRational_variety#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/NoetherProblem.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: 5 solved. It also has 1 test statement, counted here but not shown.
NoetherProblem.noether_problem
Solved: stated here without proof.
The Noether Problem: let
Lbe the field of rational functions innindeterminates overK, and letGbe a finite group permuting these indeterminates. Is the fixed fieldL^Ga rational extension ofK, i.e. doesL/Khave the Noether property?Solution: False.
theorem noether_problem : ¬ ∀ (K L ι : Type)
[Field K] [Field L] [Fintype ι] [Algebra K L] [IsRationalExtension K L ι],
HasNoetherProperty K L ι
Category research solved; AMS 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/NoetherProblem.lean, line 73.
NoetherProblem.noether_problem.variants.two
Solved: stated here without proof.
The Noether problem has a positive solution for groups permuting two indeterminates.
theorem noether_problem.variants.two {K L ι : Type}
[Field K] [Field L] [Fintype ι] [Algebra K L]
[IsRationalExtension K L ι] (hι : Fintype.card ι = 2) :
HasNoetherProperty K L ι
Category research solved; AMS 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/NoetherProblem.lean, line 82.
NoetherProblem.noether_problem.variants.three
Solved: stated here without proof.
The Noether problem has a positive solution for groups permuting three indeterminates.
theorem noether_problem.variants.three {K L ι : Type}
[Field K] [Field L] [Fintype ι] [Algebra K L]
[IsRationalExtension K L ι] (hι : Fintype.card ι = 3) :
HasNoetherProperty K L ι
Category research solved; AMS 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/NoetherProblem.lean, line 92.
NoetherProblem.noether_problem.variants.four
Solved: stated here without proof.
The Noether problem has a positive solution for groups permuting four indeterminates.
theorem noether_problem.variants.four {K L ι : Type}
[Field K] [Field L] [Fintype ι] [Algebra K L]
[IsRationalExtension K L ι] (hι : Fintype.card ι = 4) :
HasNoetherProperty K L ι
Category research solved; AMS 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/NoetherProblem.lean, line 102.
NoetherProblem.noether_problem.variants.forty_seven
Solved: stated here without proof.
One can find a counterexample to the Noether Problem's claim by considering a group permuting the 47 indeterminates of a rational function field.
theorem noether_problem.variants.forty_seven :
∃ (K L ι : Type)
(_ : Field K) (_ : Field L) (_ : Fintype ι) (_ : Algebra K L)
(_ : IsRationalExtension K L ι),
Fintype.card ι = 47 ∧ ¬ HasNoetherProperty K L ι
Category research solved; AMS 12 Field theory and polynomials, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/NoetherProblem.lean, line 113.
Sources
TheoremNormality of mathematical constants#
Despite extensive empirical evidence—billions of digits have been computed for \(\pi\), \(e\), and \(\sqrt{2}\), all showing near-uniform digit distribution—it is an open problem whether any of the classical constants \(\pi\), \(e\), \(\sqrt{2}\), \(\ln 2\), or \(\varphi\) is normal in any base.
References: * Wikipedia (Normal number) * Wikipedia (Pi)
Quoted from FormalConjectures/Wikipedia/NormalityOfPi.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.
NormalNumber.pi_normal_base_ten
Open: stated without proof.
\(\pi\) is normal in base 10.
theorem pi_normal_base_ten : IsNormalInBase 10 π
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/NormalityOfPi.lean, line 43.
Sources
TheoremOhba's conjecture (2002; proved by Noel, Reed and Wu 2015)#
References: * Wikipedia * [Oh02] Ohba, K. (2002). "On chromatic-choosable graphs." J. Graph Theory 40, pp. 130--135. * [NRW15] Noel, J. A., Reed, B. A. and Wu, H. (2015). "A proof of a conjecture of Ohba." J. Graph Theory 79, pp. 86--102. arXiv:1211.1999 * [ERT79] Erdős, P., Rubin, A. L. and Taylor, H. (1979). "Choosability in graphs." Congr. Numer. 26, pp. 125--157.
Quoted from FormalConjectures/Wikipedia/OhbaConjecture.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. It also has 2 API statements, counted here but not shown.
OhbaConjecture.ohba_conjecture
Solved: stated here without proof.
Ohba's conjecture (2002), proved by Noel, Reed and Wu (2015).
Every graph \(G\) with at most \(2\chi(G) + 1\) vertices is chromatic-choosable: it is \(\chi(G)\)-choosable, so its choice number equals its chromatic number.
theorem ohba_conjecture :
∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
(Fintype.card V : ℕ∞) ≤ 2 * G.chromaticNumber + 1 →
Choosable G G.chromaticNumber.toNat
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/OhbaConjecture.lean, line 59.
OhbaConjecture.ohba_conjecture.variants.erdos_rubin_taylor
Solved: stated here without proof.
Complete multipartite graphs with parts of size at most \(2\) (Erdős–Rubin–Taylor 1979).
The complete multipartite graph \(K_{2,2,\dots,2}\) with \(k\) parts has \(2k\) vertices and is \(k\)-choosable, as shown by Erdős, Rubin and Taylor.
Reference: [ERT79].
theorem ohba_conjecture.variants.erdos_rubin_taylor (k : ℕ) :
Choosable (completeMultipartiteGraph (fun _ : Fin k => Fin 2)) k
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/OhbaConjecture.lean, line 74.
Sources
TheoremOppermann's Conjecture#
References: - Wikipedia - Luan Alberto Ferreira, Real exponential sums over primes and prime gaps
Quoted from FormalConjectures/Wikipedia/Oppermann.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: 3 open, 1 solved and 2 textbook results.
Oppermann.oppermann_conjecture.parts.i
Open: stated without proof.
For every integer \(x \ge 2\) there exists a prime between \(x(x-1)\) and \(x^2\).
theorem oppermann_conjecture.parts.i (x : ℕ) (hx : 2 ≤ x) :
∃ p ∈ Ioo (x * (x - 1)) (x^2), p.Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Oppermann.lean, line 38.
Oppermann.oppermann_conjecture.parts.ii
Open: stated without proof.
For every integer \(x \ge 2\) there exists a prime between \(x^2\) and \(x(x+1)\).
theorem oppermann_conjecture.parts.ii (x : ℕ) (hx : 2 ≤ x) :
∃ p ∈ Ioo (x^2) (x * (x + 1)), p.Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Oppermann.lean, line 46.
Oppermann.oppermann_conjecture
Open: stated without proof.
Oppermann's Conjecture: For every integer \(x \ge 2\), the following hold: - There exists a prime between \(x(x-1)\) and \(x^2\). - There exists a prime between \(x^2\) and \(x(x+1)\).
theorem oppermann_conjecture (x : ℕ) (hx : 2 ≤ x) :
(∃ p ∈ Ioo (x * (x - 1)) (x^2), p.Prime) ∧
(∃ p ∈ Ioo (x^2) (x * (x + 1)), p.Prime)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Oppermann.lean, line 57.
Oppermann.oppermann_implies_brocard
Textbook result, proved here.
Oppermann's conjecture implies Brocard's conjecture.
theorem oppermann_implies_brocard (n : ℕ) (hn : 1 ≤ n) (P : type_of% oppermann_conjecture) :
letI prev := n.nth Nat.Prime
letI next := (n+1).nth Nat.Prime
4 ≤ ((Ioo (prev ^ 2) (next ^ 2)).filter Nat.Prime).card
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Oppermann.lean, line 64.
Oppermann.oppermann_implies_legendre
Textbook result, proved here.
Oppermann's conjecture implies Legendre's conjecture.
theorem oppermann_implies_legendre (n : ℕ) (hn : 1 ≤ n) (P : type_of% oppermann_conjecture) :
∃ p ∈ Ioo (n ^ 2) ((n + 1) ^ 2), p.Prime
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Oppermann.lean, line 106.
Oppermann.oppermann_conjecture.ferreira_large_x
Solved: stated here without proof.
Ferreira proved that Oppermann's conjecture is true for sufficiently large x.
theorem oppermann_conjecture.ferreira_large_x : ∀ᶠ x in atTop,
(∃ p ∈ Ioo (x * (x - 1)) (x^2), p.Prime) ∧
(∃ p ∈ Ioo (x^2) (x * (x + 1)), p.Prime)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Oppermann.lean, line 117.
Sources
TheoremPebbling number conjecture#
References: - Wikipedia - Pebbling on Graph Products and Other Binary Graph Constructions
Quoted from FormalConjectures/Wikipedia/PebblingNumberConjecture.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 API statements, counted here but not shown.
PebblingNumberConjecture.pebbling_number_conjecture
Open: stated without proof.
The pebbling number conjecture: the pebbling number of a Cartesian product of connected graphs is at most equal to the product of the pebbling numbers of the factors. See Asplund, Hurlbert, and Kenter.
theorem pebbling_number_conjecture {W : Type} [Fintype V] [Fintype W] [DecidableEq W]
(G : SimpleGraph V) (H : SimpleGraph W) (hG : G.Connected) (hH : H.Connected) :
PebblingNumber (G □ H) ≤ PebblingNumber G * PebblingNumber H
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/PebblingNumberConjecture.lean, line 134.
Sources
TheoremInfinitude of Pell number primes#
References: - Wikipedia - A86383
The Pell numbers \(P_n\) are defined by \(P_0 = 0\), \(P_1 = 1\), \(P_{n+2} = 2*P_{n+1} + P_n\). OEIS A129
The conjecture says that there are infinitely many prime Pell numbers.
Quoted from FormalConjectures/Wikipedia/Pell.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 textbook results. It also has 4 test statements, counted here but not shown.
PellNumbers.pellNumber_sq_add_pellNumber_succ_sq
Textbook result, proved here.
Similar to Fibonacci numbers, there exist numerous identities around Pell numbers, i.e. P_{2n+1} = P_n ^ 2 + P_{n+1} ^ 2
theorem pellNumber_sq_add_pellNumber_succ_sq (n : ℕ) :
pellNumber (2 * n + 1) = pellNumber n ^ 2 + pellNumber (n + 1) ^ 2
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Pell.lean, line 62.
PellNumbers.coe_pellNumber_eq
Textbook result, proved here.
An explicit formula for Pell numbers, similar to Binet's formula
theorem coe_pellNumber_eq : ∀ n, (pellNumber n : ℝ) = ((1 + √2) ^ n - (1 - √2) ^ n) / (2 * √2)
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Pell.lean, line 98.
PellNumbers.infinite_pellNumber_primes
Open: stated without proof.
There are infinitely many prime Pell numbers
theorem infinite_pellNumber_primes : Infinite {n : ℕ | Prime (pellNumber n)}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Pell.lean, line 148.
Sources
TheoremPerfect numbers#
A perfect number is a positive integer that equals the sum of its proper divisors (i.e., all its positive divisors excluding the number itself).
For example, 6 is perfect because its proper divisors are 1, 2, and 3, and 1 + 2 + 3 = 6. Similarly, 28 is perfect because 1 + 2 + 4 + 7 + 14 = 28.
All known perfect numbers are even. Several open problems about perfect numbers are formalised here:
- Are there infinitely many perfect numbers?
- Are there infinitely many even perfect numbers?
- Do odd perfect numbers exist?
References: - Wikipedia - Wikipedia, Odd perfect numbers
Quoted from FormalConjectures/Wikipedia/PerfectNumbers.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: 3 open and 2 solved.
PerfectNumbers.infinitely_many_perfect
Open: stated without proof.
Infinitely many perfect numbers conjecture. Are there infinitely many perfect numbers?
Reference: Wikipedia
theorem infinitely_many_perfect :
{n : ℕ | Perfect n}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PerfectNumbers.lean, line 55.
PerfectNumbers.infinitely_many_even_perfect
Open: stated without proof.
Infinitely many even perfect numbers conjecture. Are there infinitely many even perfect numbers?
This is equivalent to asking whether there are infinitely many Mersenne primes, since by the Euclid–Euler theorem an even number is perfect if and only if it has the form \(2^{p-1}(2^p - 1)\) where \(2^p - 1\) is a Mersenne prime.
Reference: Wikipedia
theorem infinitely_many_even_perfect :
{n : ℕ | Perfect n ∧ Even n}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PerfectNumbers.lean, line 71.
PerfectNumbers.odd_perfect_number_conjecture
Open: stated without proof.
Odd Perfect Number Conjecture. The Odd Perfect Number Conjecture states that all perfect numbers are even.
Reference: Wikipedia
theorem odd_perfect_number_conjecture (n : ℕ) (hn : Perfect n) : Even n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PerfectNumbers.lean, line 83.
PerfectNumbers.odd_perfect_number.lower_bound
Solved: stated here without proof.
A known result: If an odd perfect number exists, it must be greater than \(10^{1500}\) and must have at least 101 prime factors (including multiplicities).
Reference: Pascal Ochem, Michaël Rao (2012). "Odd perfect numbers are greater than 10^1500"
theorem odd_perfect_number.lower_bound (n : ℕ) (hn : Odd n) (hp : Perfect n) :
n > 10^1500 ∧ (n.primeFactorsList).length ≥ 101
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PerfectNumbers.lean, line 94.
PerfectNumbers.odd_perfect_number.euler_form
Solved: stated here; a Lean proof is at https://github.com/mzhorvath1/formal-conjectures/blob/7deed78f7babe2ae9ea13969a8dfa26854982407/FormalConjectures/Wikipedia/PerfectNumbers.lean#L110.
A known result: If an odd perfect number exists, it must be of the form \(p^α * m^2\) where \(p\) is prime, \(p \equiv 1 \pmod{4}\), \(\alpha \equiv 1 \pmod{4}\), and \(p \nmid m\).
Reference: Euler's theorem on odd perfect numbers.
Formal proof linked here provided by AlphaProof.
theorem odd_perfect_number.euler_form (n : ℕ) (hn : Odd n) (hp : Perfect n) :
∃ (p m α : ℕ),
p.Prime ∧
p ≡ 1 [ZMOD 4] ∧
α ≡ 1 [ZMOD 4] ∧
¬ p ∣ m ∧
n = p^α * m^2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/PerfectNumbers.lean, line 109.
Sources
TheoremThe Petersen colouring conjecture (Jaeger 1988)#
References: * Wikipedia * [Ja88] Jaeger, F. (1988). "Nowhere-zero flow problems." In Selected Topics in Graph Theory 3, Academic Press, pp. 71--95. * [Mk13] Mkrtchyan, V. V. (2013). "A remark on the Petersen coloring conjecture of Jaeger." Australas. J. Combin. 56, pp. 145--151. * [HS14] Hägglund, J. and Steffen, E. (2014). "Petersen-colorings and some families of snarks." Ars Math. Contemp. 7, pp. 161--173. * [Zh97] Zhang, C.-Q. (1997). Integer flows and cycle covers of graphs. Marcel Dekker.
Quoted from FormalConjectures/Wikipedia/PetersenColoringConjecture.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 1 test statement, counted here but not shown.
PetersenColoringConjecture.petersen_coloring_conjecture
Open: stated without proof.
The Petersen colouring conjecture (Jaeger 1988).
Every bridgeless cubic graph has a Petersen colouring: an edge colouring by the edges of the Petersen graph such that the three edges at each vertex are mapped onto the three edges at some vertex of the Petersen graph. Jaeger showed that this conjecture implies both the Berge–Fulkerson conjecture and the cycle double cover conjecture.
theorem petersen_coloring_conjecture :
∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
(∀ v, G.degree v = 3) → G.IsBridgeless →
∃ φ : Sym2 V → Sym2 PetersenVertex, IsPetersenColoring G φ
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/PetersenColoringConjecture.lean, line 63.
PetersenColoringConjecture.petersen_coloring_conjecture.variants.normal_five_edge_coloring
Solved: stated here without proof.
Jaeger's reformulation: normal
5-edge-colourings.A proper
5-edge-colouring of a cubic graph is normal if every edge, together with its four neighbouring edges, sees either exactly3or exactly5colours. Jaeger showed that a cubic graph has a Petersen colouring iff it has a normal5-edge-colouring.Reference: [Ja88].
theorem petersen_coloring_conjecture.variants.normal_five_edge_coloring
{V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
(hcubic : ∀ v, G.degree v = 3) :
(∃ φ : Sym2 V → Sym2 PetersenVertex, IsPetersenColoring G φ) ↔
∃ c : Sym2 V → Fin 5,
(∀ e ∈ G.edgeFinset, ∀ f ∈ G.edgeFinset, e ≠ f → (∃ v, v ∈ e ∧ v ∈ f) → c e ≠ c f) ∧
∀ e ∈ G.edgeFinset,
((G.edgeFinset.filter fun f => ∃ v, v ∈ e ∧ v ∈ f).image c).card = 3 ∨
((G.edgeFinset.filter fun f => ∃ v, v ∈ e ∧ v ∈ f).image c).card = 5
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/PetersenColoringConjecture.lean, line 79.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.