Open questions on irrationality… to Lovász's conjecture on…

TheoremOpen questions on irrationality of numbers#

References: - Wikipedia - [OAI26a] OpenAI, Catalan's constant is irrational. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Catalans-constant-is-irrational-September-24-2026/paper.pdf

Quoted from FormalConjectures/Wikipedia/Irrational.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 9 research or textbook statements: 8 open and 1 solved.

Irrational.algebraicIndependent_e_pi

Open: stated without proof.

Are \(e\) and \(\pi\) algebraically independent?

theorem algebraicIndependent_e_pi :
    AlgebraicIndependent ℚ ![e, π]

Category research open; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Irrational.lean, line 42.

Irrational.irrational_e_plus_pi

Open: stated without proof.

Is \(e + \pi\) irrational?

theorem irrational_e_plus_pi :
    Irrational (e + π)

Category research open; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Irrational.lean, line 50.

Irrational.irrational_e_times_pi

Open: stated without proof.

Is \(e \pi\) irrational?

theorem irrational_e_times_pi :
    Irrational (e * π)

Category research open; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Irrational.lean, line 58.

Irrational.irrational_e_to_e

Open: stated without proof.

Is \(e ^ e\) irrational?

theorem irrational_e_to_e :
    Irrational (e ^ e)

Category research open; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Irrational.lean, line 66.

Irrational.irrational_pi_to_e

Open: stated without proof.

Is \(\pi ^ e\) irrational?

theorem irrational_pi_to_e :
    Irrational (π ^ e)

Category research open; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Irrational.lean, line 74.

Irrational.irrational_pi_to_pi

Open: stated without proof.

Is \(\pi ^ \pi\) irrational?

theorem irrational_pi_to_pi :
    Irrational (π ^ π)

Category research open; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Irrational.lean, line 82.

Irrational.irrational_ln_pi

Open: stated without proof.

Is \(\ln(\pi)\) irrational?

theorem irrational_ln_pi :
    Irrational (log π)

Category research open; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Irrational.lean, line 90.

Irrational.irrational_eulerMascheroniConstant

Open: stated without proof.

Is the Euler-Mascheroni constant \(\gamma\) irrational?

theorem irrational_eulerMascheroniConstant :
    Irrational eulerMascheroniConstant

Category research open; AMS 33 Special functions. Declared in FormalConjectures/Wikipedia/Irrational.lean, line 98.

Irrational.irrational_catalanConstant

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/Catalan/Results/Conclusions.lean#L11.

Is the Catalan constant

\[G = \sum_{n=0}^∞ (-1)^n / (2n + 1)^2 \approx 0.91596\]

irrational?

This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.

theorem irrational_catalanConstant :
    Irrational catalanConstant

Category research solved; AMS 11 Number theory, 33 Special functions. Declared in FormalConjectures/Wikipedia/Irrational.lean, line 110.

Sources
LeanIrrational.algebraicIndependent_e_pi · Irrational.irrational_e_plus_pi · Irrational.irrational_e_times_pi · Irrational.irrational_e_to_e · Irrational.irrational_pi_to_e · Irrational.irrational_pi_to_pi · Irrational.irrational_ln_pi · Irrational.irrational_eulerMascheroniConstant · Irrational.irrational_catalanConstant

TheoremJacobian conjecture#

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/JacobianConjecture.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 5 API statements, counted here but not shown.

JacobianConjecture.jacobian_conjecture

Proved here.

The Jacobian Conjecture: any regular function (i.e. vector valued polynomial function from) kⁿ → kᵐ whose Jacobian is a non-zero constant has an inverse that is given by a regular function, where k is a field of characteristic 0.

This is false: F has Jacobian determinant 1 but identifies two distinct points, so it admits no inverse. This counterexample works in all characteristics.

theorem jacobian_conjecture {k : Type} [CommRing k] [Nontrivial k] :
    ¬ ∀ {σ : Type} [Fintype σ] [DecidableEq σ], JacobianConjectureProp k σ

Category research solved; AMS 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/JacobianConjecture.lean, line 105.

JacobianConjecture.jacobian_conjecture_two_variables

Open: stated without proof.

Does the Jacobian conjecture hold in the two variable case?

theorem jacobian_conjecture_two_variables :
    ∀ {k : Type} [Field k] [CharZero k], JacobianConjectureProp k (Fin 2)

Category research open; AMS 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/JacobianConjecture.lean, line 118.

Sources
LeanJacobianConjecture.jacobian_conjecture · JacobianConjecture.jacobian_conjecture_two_variables

TheoremJacobson Conjecture#

References: - Wikipedia - [He1965]: Herstein, I. N. (1965), "A counterexample in Noetherian rings", Proceedings of the National Academy of Sciences of the United States of America, 54 (4): 1036–1037 https://pmc.ncbi.nlm.nih.gov/articles/PMC219788/ - [Ja1956]: Jacobson, Nathan. Structure of rings. Vol. 37. American Mathematical Soc., 1956. - [Le1977]: Lenagan, T. H. (1977), "Noetherian rings with Krull dimension one", J. London Math. Soc. Series 2, 15 (1): 41–47 https://londmathsoc.onlinelibrary.wiley.com/doi/abs/10.1112/jlms/s2-15.1.41

Quoted from FormalConjectures/Wikipedia/Jacobson.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.

Jacobson.jacobson_conjecture

Open: stated without proof.

The Jacobson conjecture (in its modern form): In a (noncommutative) ring which is left and right Noetherian, the intersection of the powers of the Jacobson ideal is trivial

theorem jacobson_conjecture :
    ∀ (R : Type) [Ring R] [IsNoetherianRing R] [IsRightNoetherianRing R],
      JacobsonConjectureFor R

Category research open; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Jacobson.lean, line 51.

Jacobson.jacobson_conjecture_of_comm_ring

Textbook result, stated without proof.

For commutative rings this is the case as a consequence of Krull's intersection theorem.

theorem jacobson_conjecture_of_comm_ring (R : Type u) [CommRing R] [IsNoetherianRing R] :
    JacobsonConjectureFor R

Category textbook; AMS 13 Commutative algebra, 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Jacobson.lean, line 58.

Jacobson.jacobson_conjecture_of_right_noetherian

Solved: stated here without proof.

Originally, on page 200 of [Ja1956], Jacobson asked if the Jacobson conjecture holds for all right Noetherian rings. However in [He1965] Herstein constructs a right Noetherian ring for which the Jacobson conjecture does not hold.

theorem jacobson_conjecture_of_right_noetherian :
    ¬ ∀ (R : Type) [Ring R] [IsRightNoetherianRing R], JacobsonConjectureFor R

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Jacobson.lean, line 66.

Sources
LeanJacobson.jacobson_conjecture · Jacobson.jacobson_conjecture_of_comm_ring · Jacobson.jacobson_conjecture_of_right_noetherian

TheoremJuggler conjecture#

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/JugglerConjecture.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 1 test statement, counted here but not shown.

JugglerConjecture.juggler_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 Juggler 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 juggler_conjecture (n : ℕ) (hn : n > 0) : ∃ m, jugglerStep^[m] n = 1

Category research open; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Wikipedia/JugglerConjecture.lean, line 45.

Sources
LeanJugglerConjecture.juggler_conjecture

TheoremKakeya problem#

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/Kakeya.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. It also has 1 test statement, counted here but not shown.

Kakeya.kakeya_set_conjecture

Open: stated without proof.

The Kakeya set conjecture: Kakeya sets in \(\mathbb{R}^n\) have Hausdorff dimension \(n\).

theorem kakeya_set_conjecture (n : ℕ) (hn : n > 0) :
    KakeyaSetConjectureDim n

Category research open; AMS 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/Wikipedia/Kakeya.lean, line 62.

Kakeya.kakeya_2d

Solved: stated here without proof.

The two-dimensional case, proved by Davies [Da71].

[Da71] Davies, R. O., Some remarks on the Kakeya problem. Math. Proc. Cambridge Philos. Soc. 69 (1971), no. 3, 417–421.

theorem kakeya_2d : KakeyaSetConjectureDim 2

Category research solved; AMS 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/Wikipedia/Kakeya.lean, line 73.

Kakeya.kakeya_3d

Solved: stated here without proof.

The three-dimensional case, proved by Wang, Zahl [WaZa25].

[WaZa25] Wang, H. and Zahl, J., Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions. arXiv preprint, arXiv:2502.17655, 2025.

theorem kakeya_3d : KakeyaSetConjectureDim 3

Category research solved; AMS 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/Wikipedia/Kakeya.lean, line 83.

Kakeya.kakeya_finite

Solved: stated here without proof.

The finite field Kakeya conjecture asserts that any Kakeya set in 𝔽_qⁿ has size at least c_n · qⁿ for some constant c_n depending only on n. This was first proved by Dvir [Dv08]. The best known bound to date, due to Bukh and Chao [BuCh21], establishes that any Kakeya set in 𝔽_qⁿ has size at least qⁿ / (2 - 1/q)^(n - 1). The dimension is positive, as in kakeya_set_conjecture; for n = 0 the empty set is a Kakeya set and the bound would read 1 ≤ 0.

[Dv08] Dvir, Z., On the size of Kakeya sets in finite fields. Journal of the American Mathematical Society 22 (2009), no. 4, 1093–1097. [BuCh21] Bukh, B. and Chao, T.-W., Sharp density bounds on the finite field Kakeya problem. Discrete Analysis 26 (2021), 9 pp.

theorem kakeya_finite {F : Type*} [Field F] [Fintype F] {n : ℕ} (hn : 0 < n)
    (K : Finset (Fin n → F)) (hK : IsKakeyaFinite K) :
    card F ^ n / (2 - 1 / card F : ℚ) ^ (n - 1) ≤ K.card

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/Kakeya.lean, line 107.

Sources
LeanKakeya.kakeya_set_conjecture · Kakeya.kakeya_2d · Kakeya.kakeya_3d · Kakeya.kakeya_finite

TheoremKaplansky's Conjectures#

References: * Wikipedia * [OAI26a] OpenAI, A Torsion-Free Group Algebra with Zero Divisors. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Torsion-Free-Group-Algebra-with-Zero-Divisors-September-23-2026/paper.pdf

Throughout, "torsion-free" means that the identity is the only element of finite order (Monoid.IsTorsionFree). This is weaker than Mathlib's IsMulTorsionFree, which asks for uniqueness of roots and fails for the Promislow group below.

Quoted from FormalConjectures/Wikipedia/Kaplansky.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: 1 open and 6 solved. It also has 2 API statements, counted here but not shown.

Kaplansky.zero_divisor_conjecture

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Algebra/GroupRing/Main.lean#L13.

The zero-divisor conjecture

If G is torsion-free, then the group algebra K[G] has no non-trivial zero divisors.

This is false. It was disproved by an internal OpenAI model in September 2026 [OAI26a], which constructed a finitely presented torsion-free group \(G\) and non-zero \(\alpha, \beta \in \mathbb{F}_2[G]\) with \(\alpha \beta = 0\); see counter_zero_divisor_conjecture and the linked Lean proof.

theorem zero_divisor_conjecture :
    ¬ ∀ (K : Type) [Field K] (G : Type) [Group G], Monoid.IsTorsionFree G →
      NoZeroDivisors (MonoidAlgebra K G)

Category research solved; AMS 16 Associative rings and algebras, 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/Kaplansky.lean, line 56.

Kaplansky.idempotent_conjecture

Open: stated without proof.

The idempotent conjecture

If G is torsion-free, then K[G] has no non-trivial idempotents.

theorem idempotent_conjecture (a : MonoidAlgebra K G) (h : IsIdempotentElem a) :
    a = 0 ∨ a = 1

Category research open; AMS 16 Associative rings and algebras, 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/Kaplansky.lean, line 67.

Kaplansky.UnitConjecture.counterexamples.i

Solved: stated here without proof.

If \(P\) is the Promislow group, then the group ring \(\mathbb{F}_p[P]\) has a non-trivial unit.

theorem UnitConjecture.counterexamples.i (p : ℕ) [hp : Fact p.Prime] :
    ∃ (u : (MonoidAlgebra (ZMod p) PromislowGroup)ˣ), ¬IsTrivialUnit u.val

Category research solved; AMS 16 Associative rings and algebras, 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/Kaplansky.lean, line 109.

Kaplansky.UnitConjecture.counterexamples.ii

Solved: stated here without proof.

If \(P\) is the Promislow group, then the group ring \(\mathbb{C}[P]\) has a non-trivial unit.

theorem UnitConjecture.counterexamples.ii :
    ∃ (u : (MonoidAlgebra ℂ PromislowGroup)ˣ), ¬IsTrivialUnit u.val

Category research solved; AMS 16 Associative rings and algebras, 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/Kaplansky.lean, line 117.

Kaplansky.counter_unit_conjecture

Proved here.

The Unit Conjecture is false.

At least there is a counterexample for any prime and zero characteristic: [Mu21] Murray, A. (2021). More Counterexamples to the Unit Conjecture for Group Rings. [Pa21] Passman, D. (2021). On the counterexamples to the unit conjecture for group rings. [Ga24] Gardam, G. (2024). Non-trivial units of complex group rings.

theorem counter_unit_conjecture :
    ∃ (G : Type) (_ : Group G) (_ : Monoid.IsTorsionFree G),
    ∀ (p : ℕ) (_ : p = 0 ∨ p.Prime),
    ∃ (K : Type) (_ : Field K) (_ :  CharP K p) (u : (MonoidAlgebra K G)ˣ), ¬IsTrivialUnit u.val

Category research solved; AMS 16 Associative rings and algebras, 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/Kaplansky.lean, line 130.

Kaplansky.counter_unit_conjecture_weak

Proved here.

There is a counterexample to Unit Conjecture in any characteristic.

theorem counter_unit_conjecture_weak (p : ℕ) (hp : p = 0 ∨ p.Prime) :
    ∃ (G : Type) (_ : Group G) (_ : Monoid.IsTorsionFree G)
      (K : Type) (_ : Field K) (_ :  CharP K p) (u : (MonoidAlgebra K G)ˣ), ¬IsTrivialUnit u.val

Category research solved; AMS 16 Associative rings and algebras, 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/Kaplansky.lean, line 142.

Kaplansky.counter_zero_divisor_conjecture

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Algebra/GroupRing/Main.lean#L13.

The Zero-divisor Conjecture is false: there is a finitely presented torsion-free group \(G\) and non-zero \(\alpha, \beta \in \mathbb{F}_2[G]\) with \(\alpha \beta = 0\).

This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.

theorem counter_zero_divisor_conjecture :
    ∃ (G : Type) (_ : Group G) (_ : Monoid.IsTorsionFree G) (_ : Group.IsFinitelyPresented G)
      (α β : MonoidAlgebra (ZMod 2) G), α ≠ 0 ∧ β ≠ 0 ∧ α * β = 0

Category research solved; AMS 16 Associative rings and algebras, 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/Kaplansky.lean, line 158.

Sources
LeanKaplansky.zero_divisor_conjecture · Kaplansky.idempotent_conjecture · Kaplansky.UnitConjecture.counterexamples.i · Kaplansky.UnitConjecture.counterexamples.ii · Kaplansky.counter_unit_conjecture · Kaplansky.counter_unit_conjecture_weak · Kaplansky.counter_zero_divisor_conjecture

TheoremKöthe conjecture#

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/Koethe.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 13 research or textbook statements: 5 open and 8 solved. It also has 1 test statement and 12 API statements, counted here but not shown.

Koethe.KotheConjecture

Open: stated without proof.

The Köthe conjecture: In any ring, the sum of two nil left ideals is nil.

theorem KotheConjecture (I J : Ideal R) (hI : IsNil I) (hJ : IsNil J) : IsNil (I + J)

Category research open; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 115.

Koethe.KotherConjecture.variants.le_KotherRadical

Open: stated without proof.

The Köthe conjecture: every left nil radical is contained in the Köthe radical.

theorem KotherConjecture.variants.le_KotherRadical {I : Ideal R} (hI : IsNil I) :
    (I : Set R) ⊆ KotheRadical R

Category research open; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 120.

Koethe.KotherConjecture.variants.general_matrix

Open: stated without proof.

The Köthe conjecture: for any nil ideal I of R, the matrix ideal M_n(I) is a nil ideal of the matrix ring M_n(R).

theorem KotherConjecture.variants.general_matrix {I : TwoSidedIdeal R} (hI : IsNil I)
    (n : Type*) [Fintype n] : IsNil (matrix n I)

Category research open; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 128.

Koethe.KotherConjecture.variants.two_by_two_matrix

Open: stated without proof.

The Köthe conjecture: for any nil ideal I of R, the matrix ideal M_2(I) is a nil ideal of the matrix ring M_2(R).

theorem KotherConjecture.variants.two_by_two_matrix {I : TwoSidedIdeal R} (hI : IsNil I) :
    IsNil (matrix (Fin 2) I)

Category research open; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 135.

Koethe.KotherConjecture.variants.matrixOver_KotherRadical

Open: stated without proof.

The Köthe conjecture: for any finite index type n, the Köthe radical of the matrix ring M_n(R) is the ideal M_n(Nil*(R)) of matrices with entries in the Köthe radical of R.

theorem KotherConjecture.variants.matrixOver_KotherRadical (n : Type*) [Fintype n] :
    matrix n (Nil* R) = Nil* (Matrix n n R)

Category research open; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 143.

Koethe.KotherConjecture.variants.general_matrix_of_KotheConjecture

Proved here.

The Köthe conjecture (for rings in universe max u v) implies the general matrix formulation for rings in universe u and index types in universe v.

theorem KotherConjecture.variants.general_matrix_of_KotheConjecture
    (h : type_of% @KotheConjecture.{max u v}) :
    type_of% @KotherConjecture.variants.general_matrix.{u, v}

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 236.

Koethe.KotherConjecture.variants.KotheConjecture_of_le_KotherRadical

Proved here.

If every nil left ideal is contained in the Köthe radical, then the Köthe conjecture holds.

theorem KotherConjecture.variants.KotheConjecture_of_le_KotherRadical
    (h : type_of% @KotherConjecture.variants.le_KotherRadical.{u}) :
    type_of% @KotheConjecture.{u}

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 246.

Koethe.KotherConjecture.variants.le_KotherRadical_of_KotheConjecture

Proved here.

The Köthe conjecture implies that every nil left ideal is contained in the Köthe radical.

theorem KotherConjecture.variants.le_KotherRadical_of_KotheConjecture
    (h : type_of% @KotheConjecture.{u}) :
    type_of% @KotherConjecture.variants.le_KotherRadical.{u}

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 256.

Koethe.KotherConjecture.variants.general_matrix_of_le_KotherRadical

Proved here.

If every nil left ideal is contained in the Köthe radical (for rings in universe max u v), then the general matrix formulation holds.

theorem KotherConjecture.variants.general_matrix_of_le_KotherRadical
    (h : type_of% @KotherConjecture.variants.le_KotherRadical.{max u v}) :
    type_of% @KotherConjecture.variants.general_matrix.{u, v}

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 283.

Koethe.KotherConjecture.variants.general_matrix_of_two_by_two_matrix

Proved here.

The 2 × 2 matrix formulation of the Köthe conjecture (for rings in universe u) implies the general matrix formulation (Krempa): one first deduces the case of 2 ^ k × 2 ^ k matrices by induction and then embeds M_n(R) in a corner of M_{2 ^ k}(R).

theorem KotherConjecture.variants.general_matrix_of_two_by_two_matrix
    (h : type_of% @KotherConjecture.variants.two_by_two_matrix.{u}) :
    type_of% @KotherConjecture.variants.general_matrix.{u, v}

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 346.

Koethe.KotherConjecture.variants.general_matrix_of_matrixOver_KotherRadical

Proved here.

The formulation of the Köthe conjecture in terms of the Köthe radical of matrix rings implies the general matrix formulation.

theorem KotherConjecture.variants.general_matrix_of_matrixOver_KotherRadical
    (h : type_of% @KotherConjecture.variants.matrixOver_KotherRadical.{u, v}) :
    type_of% @KotherConjecture.variants.general_matrix.{u, v}

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 368.

Koethe.KotherConjecture.variants.matrixOver_KotherRadical_of_general_matrix

Proved here.

The general matrix formulation of the Köthe conjecture implies the formulation in terms of the Köthe radical of matrix rings.

theorem KotherConjecture.variants.matrixOver_KotherRadical_of_general_matrix
    (h : type_of% @KotherConjecture.variants.general_matrix.{u, v}) :
    type_of% @KotherConjecture.variants.matrixOver_KotherRadical.{u, v}

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 380.

Koethe.amitsur_conjecture

Solved: stated here without proof.

The Amitsur Conjecture: If J is a nil ideal in R, then J[x] is a nil ideal of the polynomial ring R[x]. This is known to be false, see Agata Smoktunowicz, Polynomial rings over nil rings need not be nil.

theorem amitsur_conjecture : ¬ ∀ (R : Type) [Ring R] (J : TwoSidedIdeal R), IsNil J →
    IsNil (TwoSidedIdeal.map (Polynomial.C) J)

Category research solved; AMS 16 Associative rings and algebras. Declared in FormalConjectures/Wikipedia/Koethe.lean, line 426.

Sources
LeanKoethe.KotheConjecture · Koethe.KotherConjecture.variants.le_KotherRadical · Koethe.KotherConjecture.variants.general_matrix · Koethe.KotherConjecture.variants.two_by_two_matrix · Koethe.KotherConjecture.variants.matrixOver_KotherRadical · Koethe.KotherConjecture.variants.general_matrix_of_KotheConjecture · Koethe.KotherConjecture.variants.KotheConjecture_of_le_KotherRadical · Koethe.KotherConjecture.variants.le_KotherRadical_of_KotheConjecture · Koethe.KotherConjecture.variants.general_matrix_of_le_KotherRadical · Koethe.KotherConjecture.variants.general_matrix_of_two_by_two_matrix · Koethe.KotherConjecture.variants.general_matrix_of_matrixOver_KotherRadical · Koethe.KotherConjecture.variants.matrixOver_KotherRadical_of_general_matrix · Koethe.amitsur_conjecture

TheoremKomlós conjecture#

The Komlós conjecture in discrepancy theory: there is a universal constant \(K\) such that for all \(n, m\) and all vectors \(v\_1, \dots, v\_n \in \mathbb{R}^m\) with \(\|v\_i\|\_2 \le 1\), there exist signs \(\varepsilon\_i \in \{-1, +1\}\) such that

\[\left\|\sum\_{i=1}^n \varepsilon\_i v\_i\right\|\_\infty \le K.\]

For a long time the best known bound was due to Banaszczyk, who proved that one can always achieve \(O(\sqrt{\log n})\). The Beck–Fiala theorem on the discrepancy of sparse set systems is a special case (up to scaling), and the conjecture implies the Beck–Fiala conjecture that set systems of degree \(t\) have discrepancy \(O(\sqrt{t})\).

The conjecture was proved in September 2026 by Guo, Fang and Lu with \(K = 3\sqrt{2\pi}\). Karingula and Lovett gave an elementary proof with \(K = 36\). A formalisation of their proof is recorded in the formal_proof attributes below.

References: - Wikipedia - W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures & Algorithms 12 (1998), 351–360 - J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985), 679–706 - S. Guo, E. X. Fang and J. Lu, Vector balancing via directional total variation, arXiv:2609.11189 - S. R. Karingula and S. Lovett, An elementary proof of the Komlós conjecture, arXiv:2609.20979

Quoted from FormalConjectures/Wikipedia/KomlosConjecture.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 1 test statement, counted here but not shown.

KomlosConjecture.komlos_conjecture

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/416b6597cb193b6745748fdfef0d64342c71dae9/FormalConjectures/Wikipedia/KomlosConjecture.lean#L64.

The Komlós conjecture

There exists a universal constant \(K > 0\) such that for all \(n, m \in \mathbb{N}\) and all vectors \(v\_1, \dots, v\_n \in \mathbb{R}^m\) with \(\|v\_i\|\_2 \le 1\) (encoded here as \(\sum\_j v\_{ij}^2 \le 1\)), there exist signs \(\varepsilon\_i \in \{-1, +1\}\) such that \(\left\|\sum\_i \varepsilon\_i v\_i\right\|\_\infty \le K\), i.e. \(\left|\sum\_i \varepsilon\_i v\_{ij}\right| \le K\) for every coordinate \(j\).

Proved by Guo, Fang and Lu with \(K = 3\sqrt{2\pi}\) and by Karingula and Lovett with \(K = 36\).

theorem komlos_conjecture :
    ∃ K : ℝ, 0 < K ∧ ∀ (n m : ℕ) (v : Fin n → Fin m → ℝ),
      (∀ i, ∑ j, (v i j) ^ 2 ≤ 1) →
      ∃ ε : Fin n → ℝ, (∀ i, ε i = 1 ∨ ε i = -1) ∧
        ∀ j, |∑ i, ε i * v i j| ≤ K

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/KomlosConjecture.lean, line 67.

KomlosConjecture.komlos_conjecture.variants.banaszczyk

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/416b6597cb193b6745748fdfef0d64342c71dae9/FormalConjectures/Wikipedia/KomlosConjecture.lean#L86.

Banaszczyk's theorem

There exists a constant \(C > 0\) such that for all \(n, m \in \mathbb{N}\) and all vectors \(v\_1, \dots, v\_n \in \mathbb{R}^m\) with \(\|v\_i\|\_2 \le 1\), there exist signs \(\varepsilon\_i \in \{-1, +1\}\) such that \(\left\|\sum\_i \varepsilon\_i v\_i\right\|\_\infty \le C \sqrt{\log(n + 2)}\). This was the best known bound towards the Komlós conjecture before its solution. (The shift \(n + 2\) inside the logarithm is a harmless normalization keeping it positive for \(n \in \{0, 1\}\).) It follows from the Komlós conjecture with \(C = 36 / \sqrt{\log 2}\).

[W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures & Algorithms 12 (1998), 351–360.]

theorem komlos_conjecture.variants.banaszczyk :
    ∃ C : ℝ, 0 < C ∧ ∀ (n m : ℕ) (v : Fin n → Fin m → ℝ),
      (∀ i, ∑ j, (v i j) ^ 2 ≤ 1) →
      ∃ ε : Fin n → ℝ, (∀ i, ε i = 1 ∨ ε i = -1) ∧
        ∀ j, |∑ i, ε i * v i j| ≤ C * Real.sqrt (Real.log (n + 2))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/KomlosConjecture.lean, line 91.

Sources
LeanKomlosConjecture.komlos_conjecture · KomlosConjecture.komlos_conjecture.variants.banaszczyk

TheoremKummer–Vandiver conjecture#

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/KummerVandiver.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.

KummerVandiver.kummer_vandiver

Open: stated without proof.

Kummer–Vandiver conjecture states that for every prime \(p\), the class number of the maximal real subfield of \(\mathbb{Q}(\zeta_p)\) is not divisible by \(p\). -

theorem kummer_vandiver (p : ℕ+) (hp : p.Prime) :
    ¬ ↑p ∣ (classNumber (maximalRealSubfield (CyclotomicField p ℚ)))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/KummerVandiver.lean, line 39.

Sources
LeanKummerVandiver.kummer_vandiver

TheoremLander, Parkin, and Selfridge Conjecture#

Reference: https://en.wikipedia.org/wiki/Lander,_Parkin,_and_Selfridge_conjecture

Quoted from FormalConjectures/Wikipedia/LanderParkinAndSelfridgeConjecture.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.

LanderParkinSelfridge.lander_parkin_selfridge

Open: stated without proof.

The Lander–Parkin–Selfridge conjecture: if the sum of \(n\) positive integer \(k\)-th powers equals the sum of \(m\) positive integer \(k\)-th powers, with all values on the left distinct from all values on the right, then \(n + m \geq k\).

Formally, for positive integers \(k, n, m \in \mathbb{N}\) and sequences \(x : \{0, \ldots, n-1\} \to \mathbb{N}\) and \(y : \{0, \ldots, m-1\} \to \mathbb{N}\) with \(x_i > 0\), \(y_j > 0\), and \(x_i \neq y_j\) for all \(i, j\), if

\[\sum_{i=0}^{n-1} x_i^k = \sum_{j=0}^{m-1} y_j^k,\]

then \(k \leq n + m\).

theorem lander_parkin_selfridge :
    ∀ (k n m : ℕ) (x : Fin n → ℕ) (y : Fin m → ℕ),
      0 < n → 0 < m →
      (∀ i, 0 < x i) → (∀ j, 0 < y j) →
      (∀ i j, x i ≠ y j) →
      ∑ i, x i ^ k = ∑ j, y j ^ k →
      k ≤ n + m

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LanderParkinAndSelfridgeConjecture.lean, line 40.

LanderParkinSelfridge.lander_parkin_selfridge.variants.five_three

Open: stated without proof.

Special case of the Lander–Parkin–Selfridge conjecture: there is no solution in positive integers to

\[x_1^5 + x_2^5 + x_3^5 = y^5.\]

That is, for all \(x_1, x_2, x_3, y \in \mathbb{N}\) with \(x_1, x_2, x_3, y > 0\),

\[x_1^5 + x_2^5 + x_3^5 \neq y^5.\]

This corresponds to the case \(k = 5\), \(n = 3\), \(m = 1\) of the general conjecture, where \(n + m = 4 < 5 = k\) would be required to yield a counterexample.

theorem lander_parkin_selfridge.variants.five_three :
    ∀ x₁ x₂ x₃ y : ℕ,
      0 < x₁ → 0 < x₂ → 0 < x₃ → 0 < y →
      x₁ ^ 5 + x₂ ^ 5 + x₃ ^ 5 ≠ y ^ 5

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LanderParkinAndSelfridgeConjecture.lean, line 57.

Sources
LeanLanderParkinSelfridge.lander_parkin_selfridge · LanderParkinSelfridge.lander_parkin_selfridge.variants.five_three

TheoremLegendre's conjecture#

References: - Landau Problems Wikipedia Page - Legendre Conjecture Wikipedia Page - Luan Alberto Ferreira, Real exponential sums over primes and prime gaps

Quoted from FormalConjectures/Wikipedia/LegendreConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 1 open and 2 solved.

LegendreConjecture.legendre_conjecture

Open: stated without proof.

Does there always exist at least one prime between consecutive perfect squares?

theorem legendre_conjecture :
    ∀ n ≥ 1, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LegendreConjecture.lean, line 38.

LegendreConjecture.bounded_gap_legendre

Solved: stated here; a Lean proof is at https://github.com/mzhorvath1/formal-conjectures/blob/a4568d467b4f42884b6a4bd09c40d65f92113ee7/FormalConjectures/Wikipedia/LegendreConjecture.lean#L48.

If there exists a constant c > 0 such that (n + 1).nth Nat.Prime - n.nth Nat.Prime < (n.nth Nat.Prime) ^ (1 / 2 - c) for all large n, then Legendre's conjecture is asymptotically true.

Formal proof linked here provided by AlphaProof.

theorem bounded_gap_legendre
    (H : ∃ c > 0, ∀ᶠ n in atTop, (n + 1).nth Nat.Prime - n.nth Nat.Prime <
      (n.nth Nat.Prime : ℝ) ^ (1 / (2 : ℝ) - c)) :
    ∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LegendreConjecture.lean, line 51.

LegendreConjecture.legendre_conjecture.ferreira_large_n

Solved: stated here without proof.

Ferreira proved that the conjecture is true for sufficiently large n.

theorem legendre_conjecture.ferreira_large_n :
    ∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LegendreConjecture.lean, line 61.

Sources
LeanLegendreConjecture.legendre_conjecture · LegendreConjecture.bounded_gap_legendre · LegendreConjecture.legendre_conjecture.ferreira_large_n

TheoremLehmer's Mahler measure problem#

References: - Wikipedia - Tao's optimization constant 40a

Quoted from FormalConjectures/Wikipedia/LehmerMahlerMeasureProblem.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.

LehmerMahlerMeasureProblem.lehmer_mahler_measure_problem

Open: stated without proof.

Let M(f) denote the Mahler measure of f. There exists a constant μ>1 such that for any f(x)∈ℤ[x], M(f)>1 → M(f)≥μ. That is, lehmerConstant > 1.

theorem lehmer_mahler_measure_problem : 1 < lehmerConstant

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LehmerMahlerMeasureProblem.lean, line 58.

LehmerMahlerMeasureProblem.lehmer_mahler_measure_problem.variants.best

Open: stated without proof.

μ=M(X^10 + X^9 - X^7 - X^6 - X^5 - X^4 - X^3 + X + 1) is the best value for lehmer_mahler_measure_problem.

theorem lehmer_mahler_measure_problem.variants.best :
    mahlerMeasureZ lehmerPolynomial ≤ lehmerConstant

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LehmerMahlerMeasureProblem.lean, line 67.

LehmerMahlerMeasureProblem.lehmer_mahler_measure_problem.variants.not_reciprocal

Solved: stated here without proof.

If \(f\) is irreducible and not reciprocal and \(M(f) > 1\) then \(M(f) \ge M(X^3 - X - 1)\).

theorem lehmer_mahler_measure_problem.variants.not_reciprocal (f : ℤ[X]) (hi : Irreducible f)
    (hf : mahlerMeasureZ f > 1) (hf' : f.reverse ≠ f) :
    mahlerMeasureZ f ≥ mahlerMeasureZ (X^3 - X - 1)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LehmerMahlerMeasureProblem.lean, line 75.

LehmerMahlerMeasureProblem.lehmer_mahler_measure_problem.variants.odd

Solved: stated here without proof.

If \(f\) is not reciprocal, all the coefficients of \(f\) are odd and \(M(f) > 1\), then \(M(f) \ge M(X^2 - X - 1)\).

A polynomial \(f\) of degree \(d\) is reciprocal when \(X^d f(1/X) = \pm f\), so nonreciprocity rules out both signs. The negative sign has to be excluded as well: the polynomial \(X^7 - X^6 - X^5 - X^4 + X^3 + X^2 + X - 1\) has all coefficients odd and satisfies \(X^7 f(1/X) = -f\), but \(1 < M(f) = 1.5823\dots < M(X^2 - X - 1)\).

theorem lehmer_mahler_measure_problem.variants.odd (f : ℤ[X])
    (hf : mahlerMeasureZ f > 1) (hf' : f.reverse ≠ f) (hf'' : f.reverse ≠ -f)
    (hodd : f.HasOddCoeffs) :
    mahlerMeasureZ f ≥ mahlerMeasureZ (X^2 - X - 1)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LehmerMahlerMeasureProblem.lean, line 94.

Sources
LeanLehmerMahlerMeasureProblem.lehmer_mahler_measure_problem · LehmerMahlerMeasureProblem.lehmer_mahler_measure_problem.variants.best · LehmerMahlerMeasureProblem.lehmer_mahler_measure_problem.variants.not_reciprocal · LehmerMahlerMeasureProblem.lehmer_mahler_measure_problem.variants.odd

TheoremLehmer's totient problem#

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/LehmerTotient.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.

LehmerTotient.lehmer_totient

Open: stated without proof.

Does there exist a composite number \(n > 1\) such that Euler’s totient function \(\varphi(n)\) divides \(n - 1\)?

theorem lehmer_totient :
    ∃ n > 1, ¬Prime n ∧ Nat.totient n ∣ n - 1

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LehmerTotient.lean, line 35.

Sources
LeanLehmerTotient.lehmer_totient

TheoremLeinster Groups#

A finite group is a Leinster group if the sum of the orders of all its normal subgroups equals twice the group's order.

References: * Wikipedia * Leinster, Tom (2001). "Perfect numbers and groups". arXiv:math/0104012

TODO: The following properties from the Wikipedia article can also be formalized: - There are no Leinster groups that are symmetric or alternating. - There is no Leinster group of order p²q² where p, q are primes. - No finite semi-simple group is Leinster. - No p-group can be a Leinster group. - All abelian Leinster groups are cyclic with order equal to a perfect number.

Quoted from FormalConjectures/Wikipedia/LeinsterGroup.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. It also has 1 API statement, counted here but not shown.

LeinsterGroup.infinitely_many_leinster_groups

Open: stated without proof.

Conjecture: Are there infinitely many Leinster groups?

This asks whether there exist infinitely many (non-isomorphic) finite groups that are Leinster groups.

Formalized via the negation of "Does there exist an n such that all Leinster groups have order less than n".

theorem infinitely_many_leinster_groups :
    ¬∃ n : ℕ, ∀ G : Type, ∀ (_ : Group G) (_ : Fintype G),
      IsLeinster G → Fintype.card G < n

Category research open; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/LeinsterGroup.lean, line 61.

LeinsterGroup.abelian_is_leinster_iff_cyclic_perfect

Solved: stated here without proof.

An abelian group is a Leinster group if and only if it is cyclic with order equal to a perfect number.

Reference: Leinster, Tom (2001). "Perfect numbers and groups". Theorem 2.1.

theorem abelian_is_leinster_iff_cyclic_perfect (G : Type*) [CommGroup G] [Fintype G] :
    IsLeinster G ↔ IsCyclic G ∧ Nat.Perfect (Fintype.card G)

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/LeinsterGroup.lean, line 86.

LeinsterGroup.exists_nonabelian_leinster_group

Solved: stated here without proof.

Non-abelian Leinster groups exist.

For example, S₃ × C₅ (order 30) and A₅ × C₁₅₁₂₈ are Leinster groups.

Reference: Leinster, Tom (2001). "Perfect numbers and groups".

theorem exists_nonabelian_leinster_group :
    ∃ G : Type, ∃ (_ : Group G) (_ : Fintype G),
      IsLeinster G ∧ ¬ ∀ (a b : G), a * b = b * a

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/LeinsterGroup.lean, line 98.

LeinsterGroup.dihedral_is_leinster_iff_odd_perfect

Solved: stated here without proof.

The dihedral group DihedralGroup n (of order 2n) is a Leinster group if and only if n is an odd perfect number. This gives a one-to-one correspondence between dihedral Leinster groups and odd perfect numbers.

In particular, the existence of odd perfect numbers is equivalent to the existence of dihedral Leinster groups.

Reference: Leinster, Tom (2001). "Perfect numbers and groups".

theorem dihedral_is_leinster_iff_odd_perfect (n : ℕ) [NeZero n] :
    IsLeinster (DihedralGroup n) ↔ Nat.Perfect n ∧ Odd n

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Wikipedia/LeinsterGroup.lean, line 114.

Sources
LeanLeinsterGroup.infinitely_many_leinster_groups · LeinsterGroup.abelian_is_leinster_iff_cyclic_perfect · LeinsterGroup.exists_nonabelian_leinster_group · LeinsterGroup.dihedral_is_leinster_iff_odd_perfect

TheoremLemoine's conjectures#

References: - Wikipedia - [Ki85] Kiltinen, J. and Young P. (1985). Goldbach, Lemoine, and a Know/Don't Know Problem.

Quoted from FormalConjectures/Wikipedia/Lemoine.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.

Lemoine.lemoine_conjecture

Open: stated without proof.

For all odd integers \(n ≥ 7\) there are prime numbers \(p,q\) such that \(n = p+2q\).

theorem lemoine_conjecture (n : ℕ) (hn : 6 < n) (odd : Odd n) :
    ∃ (p q : ℕ), p.Prime ∧ q.Prime ∧ p + 2 * q = n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Lemoine.lean, line 39.

Lemoine.lemoine_conjecture_extension

Open: stated without proof.

For all odd integers \(n ≥ 9\) there are odd prime numbers \(p,q,r,s\) and natural numbers \(a,b\) such that \(p+2q = n\), \(2+pq = 2^a+r\), \(2p+q = 2^b+s\)

theorem lemoine_conjecture_extension (n : ℕ) (hn : 8 < n) (odd : Odd n) :
    ∃ (p q r s a b : ℕ), OddPrime p ∧ OddPrime q ∧ OddPrime r ∧ OddPrime s ∧
    p + 2 * q = n ∧ 2 + p * q = 2 ^ a + r ∧ 2 * p + q = 2 ^ b + s

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Lemoine.lean, line 48.

Sources
LeanLemoine.lemoine_conjecture · Lemoine.lemoine_conjecture_extension

TheoremThe linear arboricity conjecture#

References: * Wikipedia * [AEH81] Akiyama, J., Exoo, G., and Harary, F. (1981). "Covering and packing in graphs. IV. Linear arboricity." Networks 11, pp. 69--72. * [EP84] Enomoto, H. and Péroche, B. (1984). "The linear arboricity of some regular graphs." J. Graph Theory 8, pp. 309--324. * [Al88] Alon, N. (1988). "The linear arboricity of graphs." Israel J. Math. 62, pp. 311--325.

Quoted from FormalConjectures/Wikipedia/LinearArboricityConjecture.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 1 test statement and 1 API statement, counted here but not shown.

LinearArboricityConjecture.linear_arboricity_conjecture

Open: stated without proof.

The linear arboricity conjecture (Akiyama–Exoo–Harary [AEH81]).

The edges of every graph of maximum degree Δ can be partitioned into at most ⌈(Δ + 1) / 2⌉ linear forests.

theorem linear_arboricity_conjecture {V : Type} [Fintype V] (G : SimpleGraph V)
    [DecidableRel G.Adj] :
    linearArboricity G ≤ (G.maxDegree + 2) / 2

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/LinearArboricityConjecture.lean, line 77.

LinearArboricityConjecture.linear_arboricity_conjecture.variants.regular

Open: stated without proof.

The linear arboricity conjecture for regular graphs.

Every nonempty Δ-regular graph with 0 < Δ has linear arboricity exactly ⌈(Δ + 1) / 2⌉. Since a nonempty Δ-regular graph is easily seen to have linear arboricity strictly greater than Δ / 2, this form of the conjecture is equivalent to the general upper bound; see [AEH81].

theorem linear_arboricity_conjecture.variants.regular {V : Type} [Fintype V] [Nonempty V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (Δ : ℕ) (hΔ : 0 < Δ)
    (hreg : ∀ v, G.degree v = Δ) :
    linearArboricity G = (Δ + 2) / 2

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/LinearArboricityConjecture.lean, line 91.

LinearArboricityConjecture.linear_arboricity_conjecture.variants.cubic

Solved: stated here without proof.

Cubic graphs have linear arboricity two (Akiyama–Exoo–Harary [AEH81]).

The edges of every nonempty 3-regular graph can be partitioned into two linear forests, and one linear forest is not enough.

theorem linear_arboricity_conjecture.variants.cubic {V : Type} [Fintype V] [Nonempty V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hreg : ∀ v, G.degree v = 3) :
    linearArboricity G = 2

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/LinearArboricityConjecture.lean, line 104.

LinearArboricityConjecture.linear_arboricity_conjecture.variants.alon

Solved: stated here without proof.

Alon (1988): the linear arboricity conjecture holds asymptotically.

For every ε > 0 there is a Δ₀ such that every graph of maximum degree Δ ≥ Δ₀ has linear arboricity at most (1 / 2 + ε) Δ.

Reference: [Al88].

theorem linear_arboricity_conjecture.variants.alon (ε : ℝ) (hε : 0 < ε) :
    ∃ Δ₀ : ℕ, ∀ Δ : ℕ, Δ₀ ≤ Δ → ∀ (V : Type) [Fintype V] (G : SimpleGraph V),
      ∀ [DecidableRel G.Adj], G.maxDegree ≤ Δ →
        (linearArboricity G : ℝ) ≤ (1 / 2 + ε) * Δ

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/LinearArboricityConjecture.lean, line 118.

Sources
LeanLinearArboricityConjecture.linear_arboricity_conjecture · LinearArboricityConjecture.linear_arboricity_conjecture.variants.regular · LinearArboricityConjecture.linear_arboricity_conjecture.variants.cubic · LinearArboricityConjecture.linear_arboricity_conjecture.variants.alon

TheoremLittlewood conjectures#

References: - Wikipedia - Bernard de Mathan and Olivier Teulié, Problèmes diophantiens simultanés

Quoted from FormalConjectures/Wikipedia/LittlewoodConjecture.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.

LittlewoodConjecture.littlewood_conjecture

Open: stated without proof.

For any two real numbers \(\alpha\) and \(\beta\),

\[ \liminf_{n\to\infty} n\||n\alpha\||\||n\beta\|| = 0 \]

where \(\||x\|| := \min(|x - \lfloor x \rfloor|, |x - \lceil x \rceil|)\) is the distance to the nearest integer.

theorem littlewood_conjecture (α β : ℝ) :
    atTop.liminf (fun (n : ℕ) ↦ n * distToNearestInt (n * α) * distToNearestInt (n * β)) = 0

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LittlewoodConjecture.lean, line 46.

LittlewoodConjecture.padic_littlewood_conjecture

Open: stated without proof.

For real number \(\alpha\) and prime \(p\),

\[ \liminf\_{n \to\infty} n |n|\_{p}\||n\alpha\|| = 0 \]

where \(\||x\|| := \min(|x - \lfloor x \rfloor|, |x - \lceil x \rceil|)\) is the distance to the nearest integer, and \(|x|\_{p}\) is the \(p\)-adic norm.

theorem padic_littlewood_conjecture (α : ℝ) (p : ℕ) (hp : p.Prime) :
    atTop.liminf (fun (n : ℕ) ↦ n * padicNorm p n * distToNearestInt (n * α)) = 0

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LittlewoodConjecture.lean, line 59.

Sources
LeanLittlewoodConjecture.littlewood_conjecture · LittlewoodConjecture.padic_littlewood_conjecture

TheoremLocal uniformization#

Let \(F\) be a finitely generated field extension of a field \(k\) and let \(\mathcal{O}\) be a valuation ring of \(F\) containing \(k\). Local uniformization asks for an affine model of \(F \mid k\) on which the centre of \(\mathcal{O}\) is a regular point: a finitely generated \(k\)-subalgebra \(A \subseteq \mathcal{O}\) with fraction field \(F\) such that \(A_\mathfrak{p}\) is regular, where \(\mathfrak{p} = \mathfrak{m}_\mathcal{O} \cap A\) is the centre.

This is the local form of resolution of singularities, one valuation at a time. Zariski introduced it and proved it in characteristic zero, and deduced resolution of singularities in dimension at most three from it. In positive characteristic it is known in dimension at most three, and open from dimension four on. A place is Abhyankar when the rational rank of its value group and the transcendence degree of its residue field over \(k\) add up to the transcendence degree of \(F \mid k\); an Abhyankar place whose residue field is separable over \(k\) is uniformized in any dimension [KK2005].

The form asked here is the weak one: some affine model of \(F \mid k\) works. The proofs give the strong form, where the model may moreover be required to contain a prescribed finite subset of \(\mathcal{O}\), and that is the form that patches into a resolution of singularities.

The conclusion here asks that the centre be a regular point, not a smooth one. Over a perfect field the two agree; over an imperfect field regularity is the right condition, since already \(k(a^{1/p}) \mid k\) for \(a \in k \setminus k^p\) has no model that is smooth over \(k\).

For a field extension, Algebra.EssFiniteType k F says that \(F\) is finitely generated as a field over \(k\), and Algebra.trdeg k F is the transcendence degree, the dimension of a model. The centre ValuationSubring.centerOn and the predicate ValuationSubring.HasLocalUniformization are defined in FormalConjecturesForMathlib.RingTheory.Valuation.LocalUniformization.

References: - Wikipedia - [Zar1940] O. Zariski, Local uniformization on algebraic varieties, Ann. of Math. 41 (1940), 852--896. - [Abh1956] S. Abhyankar, Local uniformization on algebraic surfaces over ground fields of characteristic \(p \neq 0\), Ann. of Math. 63 (1956), 491--526. - [Abh1966] S. Abhyankar, Resolution of singularities of embedded algebraic surfaces, Monographs in Pure and Applied Mathematics 24, Academic Press, 1966; birational resolution of threefolds over an algebraically closed field of characteristic \(p > 5\). - [Cut2009] S. D. Cutkosky, Resolution of singularities for 3-folds in positive characteristic, Amer. J. Math. 131 (2009), 59--127; a simplification of [Abh1966], also over an algebraically closed field. - [CP2008] V. Cossart and O. Piltant, Resolution of singularities of threefolds in positive characteristic I, J. Algebra 320 (2008), 1051--1082. - [CP2009] V. Cossart and O. Piltant, Resolution of singularities of threefolds in positive characteristic II, J. Algebra 321 (2009), 1836--1976; quasi-projective threefolds over a field \(k\) with \([k : k^p] < \infty\), in every positive characteristic. - [CP2019] V. Cossart and O. Piltant, Resolution of singularities of arithmetical threefolds, J. Algebra 529 (2019), 268--535. - [KK2005] H. Knaf and F.-V. Kuhlmann, Abhyankar places admit local uniformization in any characteristic, Ann. Sci. École Norm. Sup. 38 (2005), 833--846; the hypotheses are that the place is Abhyankar and that its residue field is separable over the ground field. - [KK2009] H. Knaf and F.-V. Kuhlmann, Every place admits local uniformization in a finite extension of the function field, Adv. Math. 221 (2009), 428--453. - [Tem2013] M. Temkin, Inseparable local uniformization, J. Algebra 373 (2013), 65--119.

Quoted from FormalConjectures/Wikipedia/LocalUniformization.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. It also has 1 test statement, counted here but not shown.

LocalUniformization.local_uniformization

Open: stated without proof.

Local uniformization in positive characteristic. Let \(k\) be a field of characteristic \(p > 0\), let \(F\) be a finitely generated field extension of \(k\), and let \(\mathcal{O}\) be a valuation ring of \(F\) containing \(k\). Then \(\mathcal{O}\) admits local uniformization over \(k\).

This is open from dimension four on: it is known when the transcendence degree of \(F \mid k\) is at most three, see local_uniformization_of_trdeg_le_three.

theorem local_uniformization (k F : Type*) [Field k] [Field F] [Algebra k F]
    [Algebra.EssFiniteType k F] (p : ℕ) [Fact p.Prime] [CharP k p] (𝒪 : ValuationSubring F)
    (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) :
    𝒪.HasLocalUniformization k

Category research open; AMS 12 Field theory and polynomials, 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/LocalUniformization.lean, line 123.

LocalUniformization.local_uniformization_of_charZero

Solved: stated here without proof.

Zariski's local uniformization theorem. Every valuation ring of a finitely generated field extension \(F \mid k\) that contains a field \(k\) of characteristic zero admits local uniformization over \(k\). This is the main theorem of [Zar1940].

theorem local_uniformization_of_charZero (k F : Type*) [Field k] [Field F] [Algebra k F]
    [Algebra.EssFiniteType k F] [CharZero k] (𝒪 : ValuationSubring F)
    (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) :
    𝒪.HasLocalUniformization k

Category research solved; AMS 12 Field theory and polynomials, 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/LocalUniformization.lean, line 135.

LocalUniformization.local_uniformization_of_trdeg_le_three

Solved: stated here without proof.

Local uniformization holds in transcendence degree at most three over any field. In characteristic zero this is [Zar1940]. In positive characteristic, surfaces are [Abh1956]; threefolds over an algebraically closed field of characteristic \(p > 5\) are [Abh1966], simplified in [Cut2009]; and the remaining characteristics \(2, 3, 5\) are [CP2008] and [CP2009], for quasi-projective threefolds over a field \(k\) with \([k : k^p] < \infty\). It follows in the generality stated here from [CP2019], Theorem 1.1, which resolves the singularities of every reduced separated Noetherian quasi-excellent scheme of dimension at most three in any characteristic: the centre of \(\mathcal{O}\) on a resolution of a proper model of \(F \mid k\) is a regular point.

theorem local_uniformization_of_trdeg_le_three (k F : Type*) [Field k] [Field F] [Algebra k F]
    [Algebra.EssFiniteType k F] (𝒪 : ValuationSubring F)
    (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) (hF : Algebra.trdeg k F ≤ 3) :
    𝒪.HasLocalUniformization k

Category research solved; AMS 12 Field theory and polynomials, 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/LocalUniformization.lean, line 153.

LocalUniformization.local_uniformization_after_finite_extension

Solved: stated here without proof.

Local uniformization after a finite extension. Every valuation ring of a finitely generated field extension \(F \mid k\) that contains \(k\) admits local uniformization over \(k\) after a finite extension \(E\) of \(F\), in any characteristic. This is the main theorem of [KK2009]. Compare [Tem2013], where the extension of \(F\) is purely inseparable but the ground field is extended too.

theorem local_uniformization_after_finite_extension (k F : Type*) [Field k] [Field F]
    [Algebra k F] [Algebra.EssFiniteType k F] (𝒪 : ValuationSubring F)
    (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) :
    ∃ (E : IntermediateField F (AlgebraicClosure F)) (_ : FiniteDimensional F E)
      (𝒪' : ValuationSubring E),
      𝒪'.comap (algebraMap F E) = 𝒪 ∧ 𝒪'.HasLocalUniformization k

Category research solved; AMS 12 Field theory and polynomials, 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/LocalUniformization.lean, line 166.

Sources
LeanLocalUniformization.local_uniformization · LocalUniformization.local_uniformization_of_charZero · LocalUniformization.local_uniformization_of_trdeg_le_three · LocalUniformization.local_uniformization_after_finite_extension

TheoremLonely runner conjecture#

Reference: Wikipedia

Quoted from FormalConjectures/Wikipedia/LonelyRunnerConjecture.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.

LonelyRunnerConjecture.lonely_runner_conjecture

Open: stated without proof.

Consider \(n\) runners on a circular track of unit length. At the initial time \(t = 0\), all runners are at the same position and start to run; the runners' speeds are constant, all distinct, and may be negative. A runner is said to be lonely at time \(t\) if they are at a distance (measured along the circle) of at least \(\frac 1 n\) from every other runner. The lonely runner conjecture states that each runner is lonely at some time, no matter the choice of speeds.

theorem lonely_runner_conjecture (n : ℕ)
    (speed : Fin n ↪ ℝ) (lonely : Fin n → ℝ → Prop)
    (lonely_def :
      ∀ r t, lonely r t ↔
        ∀ r2 : Fin n, r2 ≠ r →
        dist (t * speed r : UnitAddCircle) (t * speed r2) ≥ 1 / n)
    (r : Fin n) : ∃ t ≥ 0, lonely r t

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LonelyRunnerConjecture.lean, line 39.

LonelyRunnerConjecture.lonely_runner_conjecture.variants.tao_2017

Solved: stated here without proof.

Theorem 1.3 (Tao, 2017; arXiv:1701.02048). There exists an absolute constant \(c > 0\) such that for all sufficiently large \(n\), the gap of loneliness satisfies \(\delta_n \ge \frac{1}{2n} + \frac{c \log n}{n^2 (\log \log n)^2}\).

theorem lonely_runner_conjecture.variants.tao_2017 :
    ∃ c : ℝ, 0 < c ∧
      (∀ᶠ n : ℕ in Filter.atTop,
        deltaGap n ≥
          ((1 : ℝ) / (2 * (n : ℝ))
            + c * Real.log (n : ℝ) /
                ((n : ℝ) ^ 2 * (Real.log (Real.log (n : ℝ))) ^ 2)))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/LonelyRunnerConjecture.lean, line 73.

Sources
LeanLonelyRunnerConjecture.lonely_runner_conjecture · LonelyRunnerConjecture.lonely_runner_conjecture.variants.tao_2017

TheoremLovász's conjecture on Hamiltonian paths in vertex-transitive graphs (1970)#

References: * Wikipedia * [Lo70] Lovász, L. (1970). Problem 11, in Combinatorial Structures and their Applications (Proc. Calgary Internat. Conf. 1969), Gordon and Breach, p. 497. * [Ba79] Babai, L. (1979). "Long cycles in vertex-transitive graphs." J. Graph Theory 3, pp. 301--304. * [CHM14] Christofides, D., Hladký, J. and Máthé, A. (2014). "Hamilton cycles in dense vertex-transitive graphs." J. Combin. Theory Ser. B 109, pp. 34--72. arXiv:1008.2193 * [KM09] Kutnar, K. and Marušič, D. (2009). "Hamilton cycles and paths in vertex-transitive graphs — current directions." Discrete Math. 309, pp. 5491--5500.

Quoted from FormalConjectures/Wikipedia/LovaszConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 1 open and 2 solved. It also has 1 test statement and 2 API statements, counted here but not shown.

LovaszConjecture.lovasz_conjecture

Open: stated without proof.

Lovász's conjecture (1970).

Every finite connected vertex-transitive graph has a Hamiltonian path.

theorem lovasz_conjecture :
    ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
      G.Connected → IsVertexTransitive G → HasHamiltonianPath G

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/LovaszConjecture.lean, line 60.

LovaszConjecture.lovasz_conjecture.variants.babai

Solved: stated here without proof.

Babai (1979): long cycles in vertex-transitive graphs.

Every finite connected vertex-transitive graph on \(n \ge 3\) vertices contains a cycle of length at least \(\sqrt{3n}\).

Reference: [Ba79].

theorem lovasz_conjecture.variants.babai
    {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (hconn : G.Connected) (htrans : IsVertexTransitive G) (hcard : 3 ≤ Fintype.card V) :
    ∃ (v : V) (c : G.Walk v v), c.IsCycle ∧
      Real.sqrt (3 * Fintype.card V) ≤ (c.length : ℝ)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/LovaszConjecture.lean, line 74.

LovaszConjecture.lovasz_conjecture.variants.dense

Solved: stated here without proof.

Christofides–Hladký–Máthé (2014): Hamiltonian-path corollary of the dense case.

For every \(\varepsilon > 0\) there is \(n_0\) such that every connected vertex-transitive graph on \(n \ge n_0\) vertices with minimum degree at least \(\varepsilon n\) has a Hamiltonian path. This is a corollary of the Hamiltonian-cycle result in [CHM14, Theorem 2].

Reference: [CHM14].

theorem lovasz_conjecture.variants.dense :
    ∀ ε : ℝ, 0 < ε → ∃ n₀ : ℕ, ∀ {V : Type} [Fintype V] [DecidableEq V]
      (G : SimpleGraph V) [DecidableRel G.Adj], n₀ ≤ Fintype.card V →
      G.Connected → IsVertexTransitive G → ε * Fintype.card V ≤ G.minDegree →
      HasHamiltonianPath G

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/LovaszConjecture.lean, line 91.

Sources
LeanLovaszConjecture.lovasz_conjecture · LovaszConjecture.lovasz_conjecture.variants.babai · LovaszConjecture.lovasz_conjecture.variants.dense

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.