Bounded Burnside problem to Dirichlet divisor problem
TheoremBounded Burnside problem#
References: - Wikipedia - [NA68] P. S. Novikov, S. I. Adian. "Infinite periodic groups I-III." Izv. Akad. Nauk SSSR Ser. Mat. 32 (1968). - [Ad79] S. I. Adian. The Burnside Problem and Identities in Groups. Springer, 1979. - [Iv94] S. V. Ivanov. "The free Burnside groups of sufficiently large exponents." Internat. J. Algebra Comput. 4 (1994), 1-308. - [Ly96] I. G. Lysënok. "Infinite Burnside groups of even exponent." Izv. Ross. Akad. Nauk Ser. Mat. 60 (1996), 3-224.
Quoted from FormalConjectures/Wikipedia/BoundedBurnsideProblem.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.
BoundedBurnsideProblem.bounded_burnside_problem
Solved: stated here without proof.
Let \(G\) be a finitely generated group, and assume there exists \(n\) such that for every \(g\) in \(G\), \(g^n = 1\). Must \(G\) be finite?
The answer is negative. Novikov and Adian proved that for every odd \(n > 4381\) there exist infinite, finitely generated groups of exponent \(n\) [NA68]; Adian later reduced this to odd \(n > 665\) [Ad79]. The even case is harder: Ivanov proved \(B(m, n)\) infinite for \(m > 1\) and even \(n \ge 2^{48}\) divisible by \(2^9\) [Iv94], and Lysënok improved this to \(m > 1\) and \(n \ge 8000\) [Ly96]. Any such group, for example the free Burnside group \(B(2, 667)\), refutes the statement below.
Note this concerns only the universally quantified question stated here, which a single counterexample closes. The classification of which free Burnside groups \(B(m, n)\) are finite remains open, with \(B(2, 5)\) the best known open case.
theorem bounded_burnside_problem :
¬ ∀ (G : Type) [Group G] (fin_gen : Group.FG G)
(n : ℕ) (hn : n > 0) (bounded : ∀ g : G, g^n = 1), Finite G
Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/BoundedBurnsideProblem.lean, line 54.
Sources
TheoremBrennan's Conjecture#
Reference: - Wikipedia - arXiv:2409.15074 - arXiv:2512.09330 - [OAI26a] OpenAI, Brennan's conjecture and sharp inverse-square integral means. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Brennans-conjecture-and-sharp-inverse-square-integral-means-September-24-2026/paper.pdf
Quoted from FormalConjectures/Wikipedia/Brennanconjecture.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 and 3 API statements, counted here but not shown.
BrennanConjecture.brennan_universalSpectrum
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Analysis/IntegralMeans/Main.lean#L10.
Brennan's conjecture, part 1: \(B(-2) = 1\).
This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.
theorem brennan_universalSpectrum :
universalSpectrum (-2) = 1
Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/Wikipedia/Brennanconjecture.lean, line 88.
BrennanConjecture.brennan_universalSpectrumBounded
Open: stated without proof.
Brennan's conjecture, part 2: \(B_b(-2) = 1\).
theorem brennan_universalSpectrumBounded :
universalSpectrumBounded (-2) = 1
Category research open; AMS 30 Functions of a complex variable. Declared in FormalConjectures/Wikipedia/Brennanconjecture.lean, line 94.
Sources
TheoremBrocard's Conjecture#
References: - Wikipedia - Luan Alberto Ferreira, Real exponential sums over primes and prime gaps
Quoted from FormalConjectures/Wikipedia/BrocardConjecture.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.
Brocard.brocard_conjecture
Open: stated without proof.
Brocard's Conjecture For every
n ≥ 2, between the squares of then-th and(n+1)-th primes, there are at least four prime numbers.
theorem brocard_conjecture (n : ℕ) (hn : 1 ≤ n) :
letI prev := n.nth Nat.Prime;
letI next := (n+1).nth Nat.Prime;
4 ≤ ((Ioo (prev^2) (next^2)).filter Nat.Prime).card
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/BrocardConjecture.lean, line 40.
Brocard.brocard_conjecture.ferreira_large_n
Solved: stated here without proof.
Ferreira proved that Brocard's conjecture is true for sufficiently large n.
theorem brocard_conjecture.ferreira_large_n : ∀ᶠ n in atTop,
letI prev := n.nth Nat.Prime;
letI next := (n+1).nth Nat.Prime;
4 ≤ ((Ioo (prev^2) (next^2)).filter Nat.Prime).card
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/BrocardConjecture.lean, line 50.
Sources
TheoremBüchi's problem#
References: - Wikipedia
Quoted from FormalConjectures/Wikipedia/Buchi.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 5 test statements, counted here but not shown.
Buchi.buchi_problem
Open: stated without proof.
Büchi's problem There exists a positive integer \(M\) such that, for all integers \(x\) and \(a\), if \((x+n)^2 + a\) is a square for \(M\) consecutive values of \(n\), then \(a = 0\).
theorem buchi_problem :
∃ M : ℕ, 1 ≤ M ∧ IsBuchi M
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Buchi.lean, line 42.
Buchi.buchi_problem_M5
Open: stated without proof.
Büchi's problem (first open case, \(M = 5\)): For all integers \(x\) and \(a\), if \((x+n)^2 + a\) is a perfect square for \(n = 0, 1, 2, 3, 4\), then \(a = 0\).
Non-trivial sequences of length 3 and 4 are known to exist, so \(M = 5\) is the first open case.
theorem buchi_problem_M5 : IsBuchi 5
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Buchi.lean, line 55.
Sources
TheoremBunyakovsky conjecture#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/Bunyakovsky.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.
Bunyakovsky.bunyakovsky_conjecture
Open: stated without proof.
Bunyakovsky conjecture If a polynomial \(f\) over integers satisfies both Schinzel and Bunyakovsky conditions, there exist infinitely many natural numbers \(m\) such that \(f(m)\) is prime.
theorem bunyakovsky_conjecture (f : ℤ[X]) :
BunyakovskyCondition f ∧ SchinzelCondition {f} →
Infinite {n : ℕ | (f.eval (n : ℤ)).natAbs.Prime}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Bunyakovsky.lean, line 37.
Sources
TheoremBusy Beaver#
The Busy Beaver problem asks for the maximum number of steps that an n-state, 2-symbol Turing machine can take before halting, when started on an empty tape.
References:
Quoted from FormalConjectures/Wikipedia/BusyBeaver.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. It also has 1 test statement and 1 API statement, counted here but not shown.
BusyBeaver.BB_2
Textbook result, stated without proof.
The value of the Busy Beaver function for 2 states is 6.
theorem BB_2 : BB 2 = 6
Category textbook; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/Wikipedia/BusyBeaver.lean, line 79.
BusyBeaver.BB_3
Textbook result, stated without proof.
The value of the Busy Beaver function for 3 states is 21.
theorem BB_3 : BB 3 = 21
Category textbook; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/Wikipedia/BusyBeaver.lean, line 84.
BusyBeaver.BB_4
Textbook result, stated without proof.
The value of the Busy Beaver function for 4 states is 107.
theorem BB_4 : BB 4 = 107
Category textbook; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/Wikipedia/BusyBeaver.lean, line 89.
BusyBeaver.BB_5
Solved: stated here without proof.
The value of the Busy Beaver function for 5 states is 47176870.
theorem BB_5 : BB 5 = 47176870
Category research solved; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/Wikipedia/BusyBeaver.lean, line 94.
BusyBeaver.BB_6
Open: stated without proof.
Determine the value of the Busy Beaver function at n = 6.
theorem BB_6 : BB 6 = BB_6.answer
Category research open; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/Wikipedia/BusyBeaver.lean, line 103.
Sources
TheoremCarmichael's totient function conjecture#
For every positive natural number \(n\), there exists a natural number \(m\) with \(m ≠ n\), such that \(φ(n) = φ(m)\) where \(φ\) is the Euler totient function.
References: - Wikipedia - [F1998] Kevin Ford. The distribution of totients. https://arxiv.org/abs/1104.3264
Quoted from FormalConjectures/Wikipedia/CarmichaelTotient.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. It also has 1 test statement, counted here but not shown.
CarmichaelTotient.carmichealTotientFor_odd
Textbook result, proved here.
For every odd number \(n\), \(φ(2n) = φ(n)\)
theorem carmichealTotientFor_odd {n : ℕ} (hn : Odd n) : CarmichaelTotientFor n
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/CarmichaelTotient.lean, line 51.
CarmichaelTotient.charmichaelTotient
Open: stated without proof.
Carmichael's totient function conjecture: For every positive natural number \(n\), there exists a natural number \(m\) with \(m ≠ n\), such that \(φ(n) = φ(m)\).
theorem charmichaelTotient :
∀ ⦃n : ℕ⦄, 0 < n → CarmichaelTotientFor n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/CarmichaelTotient.lean, line 59.
CarmichaelTotient.carchimaelTotient_bound
Solved: stated here without proof.
In Theorem 6 in [F1998], Kevin Ford proves that the smallest counterexample to Carmichael's totient function conjecture must be \(≥ 10 ^ (10 ^ 10)\)
theorem carchimaelTotient_bound {n : ℕ} (hn : 0 < n) (hn' : n < 10 ^ (10 ^ 10)) :
CarmichaelTotientFor n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/CarmichaelTotient.lean, line 66.
Sources
TheoremCatalan's conjecture and related Diophantine equations#
References: - Wikipedia - Catalan's conjecture - arXiv:2507.12397 (Lebesgue-Nagell equation)
Quoted from FormalConjectures/Wikipedia/Catalan.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 2 open and 1 solved. It also has 2 test statements, counted here but not shown.
Catalan.catalans_conjecture
Solved: stated here; a Lean proof is at https://github.com/cadamcat/catalan-lean4/blob/4bf1f742eb341decbdfc59ec56e1616f4d13e33b/Catalan/Final/Assembly.lean#L32.
The only natural number solution to the equation \(x^a - y^b = 1\) such that \(a, b > 1\) and \(x, y > 0\) is given by \(a = 2\), \(b = 3\), \(x = 3\), and \(y = 2\).
theorem catalans_conjecture (a b x y : ℕ) (ha : 1 < a) (hb : 1 < b) (hx : 0 < x) (hy : 0 < y)
(heq : x ^ a - y ^ b = 1) : a = 2 ∧ b = 3 ∧ x = 3 ∧ y = 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Catalan.lean, line 39.
Catalan.pillais_conjecture
Open: stated without proof.
For positive integers a, b, and c, there are only finitely many positive solutions (x, y, m, n) to the equation \(ax^n - by^m = c\) where \((m, n) \neq (2, 2)\) and \(x, y > 1\).
theorem pillais_conjecture (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
{ (x, y, m, n) : (ℕ × ℕ × ℕ × ℕ) |
1 < x ∧ 1 < y ∧ 1 < m ∧ 1 < n ∧ (m, n) ≠ (2, 2) ∧
a * x^n - b * y^m = c }.Finite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Catalan.lean, line 48.
LebesgueNagell.lebesgue_nagell
Open: stated without proof.
Lebesgue-Nagell Equation Conjecture
For any odd prime \(p\), the only integer solutions \((x, y)\) to the equation \(x^2 - 2 = y^p\) are \((x, y) = (\pm 1, -1)\).
Reference: Ethan Katz and Kyle Pratt, "On the Lebesgue-Nagell equation \(x^2 - 2 = y^p\)", arXiv:2507.12397
theorem lebesgue_nagell (p : ℕ) (hp : p.Prime) (hodd : Odd p) (x y : ℤ) :
x ^ 2 - 2 = y ^ p ↔ (x = 1 ∨ x = -1) ∧ y = -1
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Catalan.lean, line 70.
Sources
TheoremČerný Conjecture#
A synchronizing word (also called a reset word) for a deterministic finite automaton (DFA) \(M = (Q, \Sigma, \delta)\) is a word \(w \in \Sigma^\*\) such that reading \(w\) from any state always leads to the same single state — formally, \(\exists p \in Q, \forall q \in Q, \delta^\*(q, w) = p\).
A DFA is called synchronizing if it admits at least one synchronizing word.
The Černý conjecture asserts that every synchronizing DFA with \(n\) states has a synchronizing word of length at most \((n - 1)^2\). This bound is sharp: the family of Černý automata \(C_n\) witnesses it, requiring exactly \((n - 1)^2\) steps.
Status: Open. The best known upper bound is \(\left(\frac{7}{48} + \frac{2 \cdot 15625}{1597536}\right) n^3 + o(n^3) \approx 0.1654\,n^3\) (Shitov, 2019). The bound \((n - 1)^2\) has been verified for small \(n\) and for special classes of automata (e.g., Eulerian, aperiodic, cyclic automata).
We use Mathlib's
DFA α σ(fromMathlib.Computability.DFA), together with the auxiliaryDFA.IsSynchronizingWordandDFA.IsSynchronizingpredicates defined inFormalConjecturesForMathlib.Computability.DFA.References: - Wikipedia: Synchronizing word - J. Černý, Poznámka k homogénnym experimentom s konečnými automatmi, Matematicko-fyzikálny časopis, Vol. 14 (1964), No. 3, 208--216. - Y. Shitov, An improvement to a recent upper bound for synchronizing words of finite automata, J. Autom. Lang. Comb. Vol. 24 (2019), 367--373.
Quoted from FormalConjectures/Wikipedia/CernyConjecture.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.
CernyConjecture.cerny_conjecture
Open: stated without proof.
Černý Conjecture: Every synchronizing DFA with \(n\) states admits a synchronizing word of length at most \((n - 1)^2\).
theorem cerny_conjecture :
∀ {α : Type*} {σ : Type*} [Fintype σ] (M : DFA α σ) (hM : M.IsSynchronizing) ,
∃ w : List α, M.IsSynchronizingWord w ∧ w.length ≤ (Fintype.card σ - 1)^2
Category research open; AMS 68 Computer science. Declared in FormalConjectures/Wikipedia/CernyConjecture.lean, line 60.
CernyConjecture.shitov_upper_bound
Solved: stated here without proof.
Shitov's bound (2019): Every synchronizing DFA with \(n\) states admits a synchronizing word of length at most \(\left(\frac{7}{48} + \frac{2 \cdot 15625}{1597536}\right) n^3 + o(n^3)\), where the \(o(n^3)\) term is uniform over all alphabets. This is the best known upper bound towards the Černý conjecture.
theorem shitov_upper_bound :
∃ f : ℝ → ℝ, f =o[atTop] (fun n : ℝ => n ^ 3) ∧
∀ {α : Type*} {σ : Type*} [Fintype σ] (M : DFA α σ) (hM : M.IsSynchronizing) ,
∃ w : List α, M.IsSynchronizingWord w ∧
(w.length : ℝ) ≤ (7 / 48 + 2 * 15625 / 1597536) * (Fintype.card σ : ℝ) ^ 3
+ f (Fintype.card σ : ℝ)
Category research solved; AMS 68 Computer science. Declared in FormalConjectures/Wikipedia/CernyConjecture.lean, line 71.
Sources
TheoremClass number problem for real quadratic fields#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/ClassNumberProblem.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.
ClassNumberProblem.class_number_problem
Open: stated without proof.
There are infinitely many real quadratic fields
ℚ(√d)with class number one, whered > 1is a squarefree integer.
theorem class_number_problem :
{ d : ℤ | Squarefree d ∧ d > 1 ∧ IsClassNumberOne d }.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ClassNumberProblem.lean, line 41.
ClassNumberProblem.class_number_problem.variants.imaginary
Solved: stated here without proof.
Stark–Heegner theorem : For any squarefree integer
d < 0, the class number of the imaginary quadratic field Q(√d) is one if and only ifd ∈ {-1, -2, -3, -7, -11, -19, -43, -67, -163}.
theorem class_number_problem.variants.imaginary :
{ d : ℤ | Squarefree d ∧ d < 0 ∧ IsClassNumberOne d } =
{-1, -2, -3, -7, -11, -19, -43, -67, -163}
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/ClassNumberProblem.lean, line 50.
Sources
TheoremCollatz conjecture#
References: * Wikipedia * erdosproblems.com/1135 * [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. * [La10] Lagarias, Jeffrey C., The {\(3x+1\)} problem: an overview. (2010), 3--29. * [La16] Lagarias, Jeffrey C., Erdős, Klarner, and the {\(3x+1\)} problem. Amer. Math. Monthly (2016), 753--776. * [La85] Lagarias, Jeffrey C., The {\(3x+1\)} problem and its generalizations. Amer. Math. Monthly (1985), 3--23.
Quoted from FormalConjectures/Wikipedia/CollatzConjecture.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.
CollatzConjecture.collatz_conjecture
Open: stated without proof.
Now form a sequence beginning with any positive integer, where each subsequent term is obtained by applying the operation defined above to the previous term. The Collatz conjecture states that for any positive integer \(n\), there exists a natural number \(m\) such that the \(m\)-th term of the sequence is 1.
theorem collatz_conjecture (n : ℕ) (hn : n > 0) : ∃ m, collatzStep^[m] n = 1
Category research open; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Wikipedia/CollatzConjecture.lean, line 53.
Sources
TheoremCongruent Number#
A natural number \(n\) is called a congruent number if there exists a right triangle with rational sides \(a\), \(b\), and hypotenuse \(c\) such that the area of the triangle is \(\frac{1}{2}ab = n\).
References: - Wikipedia (Congruent number) - Wikipedia (Tunnell's theorem) - Keith Conrad's note
Quoted from FormalConjectures/Wikipedia/CongruentNumber.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: 2 open, 2 solved and 1 textbook result. It also has 4 test statements, counted here but not shown.
CongruentNumber.not_congruentNumber_1
Textbook result, stated without proof.
1 is not a congruent number, as proved by Fermat via infinite descent.
theorem not_congruentNumber_1 : ¬ congruentNumber 1
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/CongruentNumber.lean, line 41.
CongruentNumber.Tunnell_odd
Solved: stated here without proof.
Tunnell's theorem (necessary condition) for odd squarefree congruent numbers.
theorem Tunnell_odd (n : ℕ) (hsqf : Squarefree n) (hodd : Odd n) :
congruentNumber n → 2 * (A n).ncard = (B n).ncard
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/CongruentNumber.lean, line 104.
CongruentNumber.Tunnell_even
Solved: stated here without proof.
Tunnell's theorem (necessary condition) for even squarefree congruent numbers.
theorem Tunnell_even (n : ℕ) (hsqf : Squarefree n) (heven : Even n) :
congruentNumber n → 2 * (C n).ncard = (D n).ncard
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/CongruentNumber.lean, line 110.
CongruentNumber.Tunnell_odd_converse
Open: stated without proof.
Tunnell's theorem (sufficient condition assuming BSD) for odd squarefree congruent numbers.
theorem Tunnell_odd_converse (n : ℕ) (hsqf : Squarefree n) (hodd : Odd n) :
2 * (A n).ncard = (B n).ncard → congruentNumber n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/CongruentNumber.lean, line 118.
CongruentNumber.Tunnell_even_converse
Open: stated without proof.
Tunnell's theorem (sufficient condition assuming BSD) for even squarefree congruent numbers.
theorem Tunnell_even_converse (n : ℕ) (hsqf : Squarefree n) (heven : Even n) :
2 * (C n).ncard = (D n).ncard → congruentNumber n
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/CongruentNumber.lean, line 124.
Sources
TheoremThe \(\frac 1 3\)–\(\frac 2 3\) conjecture#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/conjecture_1_3_to_2_3.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.
Conjecture_1_3_to_2_3.conjecture_1_3_to_2_3
Open: stated without proof.
Does every finite partially ordered set that is not totally ordered contain two elements \(x\) and \(y\) such that the probability that \(x\) appears before \(y\) in a random linear extension is between \(\frac 1 3\) and \(\frac 2 3\)?
The set of all total order extensions is represented as order preserving bijections \(P\) of \(1, ..., n\).
theorem conjecture_1_3_to_2_3 : ∀ (P : Type) [Finite P] [PartialOrder P]
(not_total : ¬ Std.Total (α := P) (· ≤ ·)) (total_ext : Set <| OrderHom P ℕ)
(total_ext_def : ∀ σ, σ ∈ total_ext ↔ Set.range σ = Set.Icc 1 (Nat.card P)),
∃ x y : P, ({σ ∈ total_ext | σ x < σ y}.ncard / total_ext.ncard : ℚ)
∈ Set.Icc (1/3) (2/3)
Category research open; AMS 06 Order, lattices, ordered algebraic structures. Declared in FormalConjectures/Wikipedia/conjecture_1_3_to_2_3.lean, line 39.
Sources
LemmaConway's 99-graph problem#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/Conway99Graph.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 3 test statements and 1 API statement, counted here but not shown.
Conway99Graph.completeGraphIsClique
Textbook result, proved here.
A finset of vertices in a complete graph is always a clique.
lemma completeGraphIsClique (s : Finset V) : (⊤ : SimpleGraph V).IsClique s
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/Conway99Graph.lean, line 38.
Conway99Graph.completeGraph_cliqueSet
Textbook result, proved here.
The only clique of size
nin a complete graph onnvertices is the entire set of vertices.
lemma completeGraph_cliqueSet :
(⊤ : SimpleGraph V).cliqueSet (Fintype.card V) = {Set.univ.toFinset}
Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/Conway99Graph.lean, line 45.
Conway99Graph.conway99Graph
Open: stated without proof.
Does there exist an undirected graph with 99 vertices, in which each two adjacent vertices have exactly one common neighbor, and in which each two non-adjacent vertices have exactly two common neighbors? Equivalently, every edge should be part of a unique triangle and every non-adjacent pair should be one of the two diagonals of a unique 4-cycle. The first condition is equivalent to being locally linear.
theorem conway99Graph : ∃ G : SimpleGraph (Fin 99),
G.LocallyLinear ∧ NonEdgesAreDiagonals G
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/Conway99Graph.lean, line 67.
Sources
LemmaDedekind Numbers#
A Dedekind number
M(n)counts the number of monotone Boolean functions onnvariables, or equivalently, the number of antichains (Sperner families) in the Boolean lattice2^[n].For example,
\[M ( 0 ) = 2 , M ( 1 ) = 3 , M ( 2 ) = 6 , and M ( 3 ) = 20 .\]The first few values grew slowly:
\[M ( 4 ) = 168 , M ( 5 ) = 7581\], but then rapidly:
\[M ( 6 ) = 7828354 , M ( 7 ) = 2414682040998 , M ( 8 ) = 56130437228687557907788\], and
\[M ( 9 ) = 286386577668298411128469151667598498812366\](computed in 2023).
We formalize two definitions: -
M n: the number of monotone Boolean functions(Fin n → Bool) → Bool-M' n: the number of antichains (Sperner families) ofFinset (Fin n)We prove their values for small
nand show that the two definitions agree for alln.The problem is to determine the exact values of \(M(n)\) for \(n ≥ 10\). In particular, the value of \(M(10)\) is currently unknown.
Quoted from FormalConjectures/Wikipedia/DedekindNumber.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, 1 solved and 3 textbook results. It also has 13 test statements and 6 API statements, counted here but not shown.
DedekindNumber.exists_minimal_true_subset
Textbook result, proved here.
Every true set of a monotone Boolean function contains a minimal true set.
lemma exists_minimal_true_subset {n : ℕ} {f : (Fin n → Bool) → Bool} (_ : Monotone f)
{s : Finset (Fin n)} (hs : f (χ s) = true) :
∃ t, t ⊆ s ∧ f (χ t) = true ∧ ∀ u, u ⊆ t → f (χ u) = true → t ⊆ u
Category textbook; AMS 05 Combinatorics, 06 Order, lattices, ordered algebraic structures. Declared in FormalConjectures/Wikipedia/DedekindNumber.lean, line 168.
DedekindNumber.fromSperner_toSperner
Textbook result, proved here.
Converting a monotone function to a Sperner family and back yields the same function.
lemma fromSperner_toSperner {n : ℕ} (f : (Fin n → Bool) → Bool) (hf : Monotone f) :
fromSperner (toSperner f) = f
Category textbook; AMS 05 Combinatorics, 06 Order, lattices, ordered algebraic structures. Declared in FormalConjectures/Wikipedia/DedekindNumber.lean, line 184.
DedekindNumber.toSperner_fromSperner
Textbook result, proved here.
Converting a Sperner family to a monotone function and back yields the same family.
lemma toSperner_fromSperner {n : ℕ} (A : Finset (Finset (Fin n))) (hA : IsSperner A) :
toSperner (fromSperner A) = A
Category textbook; AMS 05 Combinatorics, 06 Order, lattices, ordered algebraic structures. Declared in FormalConjectures/Wikipedia/DedekindNumber.lean, line 203.
DedekindNumber.M_eq_kisielewiczFormula
Solved: stated here without proof.
Kisielewicz (1988) proved the following arithmetic formula for the Dedekind numbers:
\[ M(n) = \sum_{k=0}^{2^{2^n}}\prod_{j = 1}^{2 ^ n - 1}\prod_{i = 0}^{j - 1} \left( 1 - b_i^kb_j^k \prod_{m = 0}^{\log_2 i} (1 - b_m^i + b_m^ib_m^j)\right), \]where \(b_i^k\) is the \(i\)-th bit of \(k\). However, this formula is not computationally efficient for large \(n\).
theorem M_eq_kisielewiczFormula : M = kisielewiczFormula
Category research solved; AMS 05 Combinatorics, 06 Order, lattices, ordered algebraic structures. Declared in FormalConjectures/Wikipedia/DedekindNumber.lean, line 259.
DedekindNumber.M_eq
Open: stated without proof.
No closed-form expression that allows efficient computation of Dedekind numbers is currently known.
theorem M_eq : M = M_eq.answer
Category research open; AMS 05 Combinatorics, 06 Order, lattices, ordered algebraic structures. Declared in FormalConjectures/Wikipedia/DedekindNumber.lean, line 269.
DedekindNumber.Dedekind_10
Open: stated without proof.
In particular, the Dedekind number for
n = 10is currently unknown.
theorem Dedekind_10 : M 10 = Dedekind_10.answer
Category research open; AMS 05 Combinatorics, 06 Order, lattices, ordered algebraic structures. Declared in FormalConjectures/Wikipedia/DedekindNumber.lean, line 278.
Sources
TheoremDeterminantal conjecture#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/DeterminantalConjecture.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.
DeterminantalConjecture.determinantal_conjecture
Open: stated without proof.
Does the determinant of the sum \(A + B\) of two \(n \times n\) normal complex matrices \(A\) and \(B\) always lie in the convex hull of the \(n!\) points \(\prod\_i (\lambda(A)\_i + \lambda(B)\_{\sigma(i)})\)? Here the numbers \(\lambda(A)\_i\) and \(\lambda(B)\_i\) are the eigenvalues of \(A\) and \(B\), and \(\sigma\) is an element of the symmetric group \(S\_n\).
theorem determinantal_conjecture
(n : Type) [Fintype n] [DecidableEq n]
(d1 d2 : n → ℂ) (U1 U2 : unitary (Matrix n n ℂ)) :
(U1 * Matrix.diagonal d1 * star U1 + U2 * Matrix.diagonal d2 * star U2).det
∈ convexHull ℝ { ∏ i, (d1 i + d2 (σ i)) | σ : Equiv.Perm n }
Category research open; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Wikipedia/DeterminantalConjecture.lean, line 46.
Sources
TheoremBabai–Seress Conjectures on the Diameter of Finite Groups#
References: - Wikipedia, Diameter (group theory) - H. A. Helfgott and Á. Seress, On the diameter of permutation groups - L. Babai and Á. Seress, On the diameter of permutation groups, European Journal of Combinatorics 13 (1992), 231–243
This file contains two conjectures from the Babai–Seress paper:
Conjecture 1.5: \(\operatorname{diam}(A_n) < n^C\) for some absolute constant \(C\), where \(A_n\) is the alternating group on \(n\) elements.
Conjecture 1.7: \(\operatorname{diam}(G) < (\log |G|)^C\) for some absolute constant \(C\), where \(G\) ranges over all non-abelian finite simple groups.
Conjecture 1.7 generalises Conjecture 1.5, since for \(G = A_n\) we have \(\log |A_n| \approx n \log n\), so a polylogarithmic bound in \(|G|\) implies a polynomial bound in \(n\).
Quoted from FormalConjectures/Wikipedia/DiameterSimpleFiniteGroups.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 3 test statements, counted here but not shown.
BabaiSeressConjectures.babai_seress_conjecture_alternating
Open: stated without proof.
Babai–Seress Conjecture (Conjecture 1.5): There exists an absolute constant \(C\) such that the diameter of the alternating group \(A_n\) satisfies
\[\operatorname{diam}(A_n) \leq n^C.\]
theorem babai_seress_conjecture_alternating :
∃ C : ℕ, ∀ n : ℕ,
(groupDiam (alternatingGroup (Fin n)) : ℝ) ≤ (n : ℝ) ^ C
Category research open; AMS 05 Combinatorics, 20 Group theory and generalizations, 68 Computer science. Declared in FormalConjectures/Wikipedia/DiameterSimpleFiniteGroups.lean, line 156.
BabaiSeressConjectures.babai_seress_conjecture
Open: stated without proof.
Babai–Seress Conjecture (Conjecture 1.7): There exists an absolute constant \(C\) such that every finite simple non-abelian group \(G\) satisfies
\[\operatorname{diam}(G) \leq (\log |G|)^C.\]
theorem babai_seress_conjecture :
∃ C : ℕ,
∀ (G : Type) [Group G] [Fintype G] [IsSimpleGroup G],
(∃ a b : G, a * b ≠ b * a) →
(groupDiam G : ℝ) ≤ (Real.log (Fintype.card G : ℝ)) ^ C
Category research open; AMS 05 Combinatorics, 20 Group theory and generalizations, 68 Computer science. Declared in FormalConjectures/Wikipedia/DiameterSimpleFiniteGroups.lean, line 168.
Sources
TheoremDickson's conjecture#
References: - Wikipedia - PrimePages glossary - OEIS Wiki - MathWorld - Leonard Eugene Dickson, History of the Theory of Numbers, Vol. I: Divisibility and Primality - Arxiv
Quoted from FormalConjectures/Wikipedia/Dickson.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 open.
Dickson.dickson_conjecture
Open: stated without proof.
Dickson's conjecture If a finite set of linear integer forms \(f_i(n) = a_i n+b_i\) satisfies Schinzel condition, there exist infinitely many natural numbers \(m\) such that \(f_i(m)\) are primes for all \(i\).
theorem dickson_conjecture (fs : Finset ℤ[X]) (hfs : ∀ f ∈ fs, f.degree = 1 ∧ 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/Dickson.lean, line 43.
Dickson.generalized_twin_primes
Open: stated without proof.
The generalized twin-prime conjecture For any positive integer \(k\) there are infinitely many primes \(p\) such that \(p + 2k\) is prime.
theorem generalized_twin_primes (k : ℕ) (hk : 0 < k) :
Infinite {p : ℕ | p.Prime ∧ (p + 2 * k).Prime}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Dickson.lean, line 54.
Dickson.infinite_safe_primes
Open: stated without proof.
The infinitude of Sophie Germain primes There are infinitely many primes \(p\) such that \(2p + 1\) is prime.
theorem infinite_safe_primes :
Infinite {p : ℕ | Prime p ∧ Prime (2 * p + 1)}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Dickson.lean, line 63.
Dickson.infinite_cousin_primes
Open: stated without proof.
The infinitude of cousin primes There are infinitely many primes \(p\) such that \(p + 4\) is prime.
theorem infinite_cousin_primes :
Infinite {p : ℕ | Prime p ∧ Prime (p + 4)}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Dickson.lean, line 72.
Dickson.infinite_sexy_primes
Open: stated without proof.
The infinitude of sexy primes There are infinitely many primes \(p\) such that \(p + 6\) is prime.
theorem infinite_sexy_primes :
Infinite {p : ℕ | Prime p ∧ Prime (p + 6)}
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Dickson.lean, line 81.
Sources
TheoremDiophantine \(m\)-tuples#
A Diophantine \(m\)-tuple is a set of \(m\) distinct positive integers \(\{a_1, \dots, a_m\}\) such that \(a_i a_j + 1\) is a perfect square for every \(i \neq j\).
References: - Wikipedia - [Du16] Dujella, Andrej, What is... a Diophantine m-tuple?, Notices Amer. Math. Soc. 63 (2016), 772--774. - [Du] Dujella, Andrej, Diophantine quintuple conjecture. - [HTZ19] He, Bo, Togbé, Alain and Ziegler, Volker, There is no Diophantine quintuple, Trans. Amer. Math. Soc. 371 (2019), 6665--6709. - [BD69] Baker, Alan and Davenport, Harold, The equations \(3x^2-2=y^2\) and \(8x^2-7=z^2\). Quart. J. Math. Oxford Ser. (2) 20 (1969), 129--137. - [Gi99] Gibbs, Philip, Some rational Diophantine sextuples, (1999).
Quoted from FormalConjectures/Wikipedia/DiophantineTuple.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, 2 solved and 2 textbook results. It also has 2 test statements, counted here but not shown.
DiophantineTuple.isDiophantineTuple_of_subset
Textbook result, proved here.
The property of being a Diophantine tuple is closed under subsets. [Du16]
theorem isDiophantineTuple_of_subset (s t : Finset R) (h1 : IsDiophantineTuple t)
(h2 : s ⊆ t) : IsDiophantineTuple s
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/DiophantineTuple.lean, line 71.
DiophantineTuple.noIntegralDiophantineFiveTuple
Solved: stated here without proof.
The Diophantine 5-tuple theorem: there does not exist an integral Diophantine 5-tuple. [HTZ19]
theorem noIntegralDiophantineFiveTuple : NoIntegralDiophantineFiveTuple
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/DiophantineTuple.lean, line 109.
DiophantineTuple.hasUniqueExtension_of_forall
Open: stated without proof.
The "strong Diophantine 5-tuple conjecture", so-called because it implies the Diophantine 5-tuple theorem (see
noIntegralDiophantineFiveTuple_of_hasUniqueExtensionOfForall). [Du]
theorem hasUniqueExtension_of_forall : HasUniqueExtensionOfForall
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/DiophantineTuple.lean, line 150.
DiophantineTuple.noIntegralDiophantineFiveTuple_of_hasUniqueExtensionOfForall
Textbook result, proved here.
If every integral Diophantine triple has a unique extension by a larger element, then there is no integral Diophantine 5-tuple. [Du]
Proof: suppose a 5-tuple \(a < b < c < d_1 < d_2\) exists; then \(d_1 = d_2\) by unique extension.
theorem noIntegralDiophantineFiveTuple_of_hasUniqueExtensionOfForall :
HasUniqueExtensionOfForall → NoIntegralDiophantineFiveTuple
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/DiophantineTuple.lean, line 159.
DiophantineTuple.hasUniqueExtension_of_1_3_8
Solved: stated here without proof.
HasUniqueExtensionis known to hold for certain triples, including \(\{1, 3, 8\}\): this is essentially the Baker–Davenport theorem [BD69], which states that \(120\) is the only integer \(d\) such that \(\{1, 3, 8, d\}\) is a Diophantine tuple. Together with a finite check ruling out \(d < 8\), this shows that no integral Diophantine tuple properly extends \(\{1, 3, 8, 120\}\).
theorem hasUniqueExtension_of_1_3_8 : HasUniqueExtension 1 3 8
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/DiophantineTuple.lean, line 195.
DiophantineTuple.rational_7_tuple
Open: stated without proof.
Does there exist a rational Diophantine 7-tuple? [Du16]
theorem rational_7_tuple :
∃ t, IsRationalDiophantineTuple t ∧ t.card = 7
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/DiophantineTuple.lean, line 221.
Sources
TheoremDirichlet divisor problem#
Let \(d(n)\) be the number of divisors of \(n\) and \(D(x) = \sum_{n \le x} d(n)\) the divisor summatory function. Dirichlet's hyperbola method gives
\[D(x) = x \log x + (2\gamma - 1) x + \Delta(x), \qquad \Delta(x) = O(x^{1/2}),\]where \(\gamma\) is the Euler–Mascheroni constant. The Dirichlet divisor problem asks for the infimum \(\theta\) of exponents with \(\Delta(x) = O(x^{\theta})\). It is conjectured that \(\theta = 1/4\), i.e. \(\Delta(x) = O(x^{1/4 + \varepsilon})\) for every \(\varepsilon > 0\). Hardy showed \(\theta \ge 1/4\), so the conjecture would be sharp. Huxley's bound \(\theta \le 131/416 \approx 0.3149\) [Hu03] is now historical: the best known upper bound is \(\theta \le 0.314483\ldots\), due to Li and Yang [LY23]. The problem remains open.
References: - Wikipedia: Divisor summatory function - Wikipedia: Dirichlet divisor problem - [Di49] P. G. L. Dirichlet, Über die Bestimmung der mittleren Werthe in der Zahlentheorie, Abhandl. Königl. Preuss. Akad. Wiss. (1849), 69-83. - [Ha16] G. H. Hardy, On Dirichlet's divisor problem, Proc. London Math. Soc. (1916), 1-25. - [Hu03] M. N. Huxley, Exponential sums and lattice points III, Proc. London Math. Soc. (2003), 591-609. - [LY23] X. Li, X. Yang, An improvement on Gauss's circle problem and Dirichlet's divisor problem, arXiv:2308.14859 (2023), Theorem 1.2.
Quoted from FormalConjectures/Wikipedia/DirichletDivisorProblem.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. It also has 1 test statement, counted here but not shown.
DirichletDivisorProblem.divisor_error_dirichlet
Textbook result, stated without proof.
Dirichlet's bound [Di49]: \(\Delta(x) = O(x^{1/2})\).
theorem divisor_error_dirichlet :
divisorError =O[atTop] fun x => Real.sqrt x
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/DirichletDivisorProblem.lean, line 70.
DirichletDivisorProblem.dirichlet_divisor_problem
Open: stated without proof.
The Dirichlet divisor problem: is it true that \(\Delta(x) = O(x^{1/4 + \varepsilon})\) for every \(\varepsilon > 0\)? (Equivalently, is the infimum of admissible exponents equal to \(1/4\)?)
theorem dirichlet_divisor_problem :
∀ ε > (0 : ℝ), divisorError =O[atTop] fun x => x ^ ((1 : ℝ) / 4 + ε)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/DirichletDivisorProblem.lean, line 79.
DirichletDivisorProblem.divisor_error_hardy
Solved: stated here without proof.
Hardy's lower bound [Ha16]: \(\Delta(x)\) is not \(o(x^{1/4})\), so the exponent \(1/4\) in the Dirichlet divisor problem cannot be improved.
theorem divisor_error_hardy :
¬ (divisorError =o[atTop] fun x => x ^ ((1 : ℝ) / 4))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/DirichletDivisorProblem.lean, line 88.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.