Scholz conjecture on addition… to Tarski's exponential function…
TheoremScholz conjecture on addition chains#
References: - Wikipedia - MathWorld - Tall22 Amadou Tall. "The Scholz conjecture on addition chain is true for infinitely many integers with \(\ell(2n) = \ell(n)\)." arXiv:2210.13812 (2022). Also available as ePrint 2023/020. - OEIS A003313
Quoted from FormalConjectures/Wikipedia/ScholzConjecture.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.
ScholzConjecture.scholz_conjecture
Open: stated without proof.
The Scholz conjecture, also known as the Scholz-Brauer conjecture, asserts that for every positive integer \(n\), the addition-chain length of \(2^n - 1\) is at most \(n - 1 + \ell(n)\).
theorem scholz_conjecture :
∀ (n : ℕ), 0 < n → ℓ(2 ^ n - 1) ≤ n - 1 + ℓ(n)
Category research open; AMS 11 Number theory, 68 Computer science. Declared in FormalConjectures/Wikipedia/ScholzConjecture.lean, line 44.
Sources
TheoremSelfridge's conjectures#
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/Selfridge.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.
Selfridge.selfridge_conjecture
Open: stated without proof.
PSW conjecture (Selfridge's test) Let \(p\) be an odd number, with \(p \equiv \pm 2 \pmod{5}\), \(2^{p-1} \equiv 1 \pmod{p}\) and \(F_{p+1} \equiv 0 \pmod{p}\), then \(p\) is a prime number.
theorem selfridge_conjecture (p : ℕ) (hp : IsSelfridge p) : p.Prime
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Selfridge.lean, line 73.
Selfridge.selfridge_conjecture.variants.exist_pseudo_counterexample
Textbook result, proved here.
Selfridge's test variant: Let \(p\) be an odd number, with \(p \equiv \pm 1 \pmod{5}\), \(2^{p-1} \equiv 1 \pmod{p}\) and \(F_{p-1} \equiv 0 \pmod{p}\), then \(p\) is a prime number.
This test does not work.
theorem selfridge_conjecture.variants.exist_pseudo_counterexample :
∃ n > 1, IsPseudoSelfridge n ∧ ¬ n.Prime
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Selfridge.lean, line 84.
Selfridge.selfridge_conjecture.variants.pseudo_counterexample
Textbook result, proved here.
Selfridge's test variant: Let \(p\) be an odd number, with \(p \equiv \pm 1 \pmod{5}\), \(2^{p-1} \equiv 1 \pmod{p}\) and \(F_{p-1} \equiv 0 \pmod{p}\), then \(p\) is a prime number.
The number \(6601\) is a conterexample to this test satisfying \(6601 ≡ 1 \mod 5\)
theorem selfridge_conjecture.variants.pseudo_counterexample :
IsPseudoSelfridge 6601 ∧ ¬ (6601).Prime ∧ 6601 ≡ 1 [MOD 5]
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Selfridge.lean, line 98.
Selfridge.selfridge_conjecture.variants.pseudo_counterexample'
Textbook result, proved here.
Selfridge's test variant: Let \(p\) be an odd number, with \(p \equiv \pm 1 \pmod{5}\), \(2^{p-1} \equiv 1 \pmod{p}\) and \(F_{p-1} \equiv 0 \pmod{p}\), then \(p\) is a prime number.
The number \(30889\) is a conterexample to this test satisfying \(30889 ≡ - 1 \mod 5\)
theorem selfridge_conjecture.variants.pseudo_counterexample' :
IsPseudoSelfridge 30889 ∧ ¬ (30889).Prime ∧ 30889 ≡ 4 [MOD 5]
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Selfridge.lean, line 111.
Selfridge.selfridge_seq_conjecture
Open: stated without proof.
Selfridge conjectured that the number of prime factors of the
n-th Fermat number does not grow monotonically in \(n\).
theorem selfridge_seq_conjecture : ¬ Monotone fermatFactors
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Selfridge.lean, line 136.
Selfridge.selfridge_seq_conjecture.variants.sufficient_condition
Proved here.
Selfridge conjectured that the number of prime factors of the
n-th Fermat number does not grow monotonically in \(n\).A sufficient condition for this conjecture to hold is that there exists a Fermat prime larger than 65537.
theorem selfridge_seq_conjecture.variants.sufficient_condition (n : ℕ) (hn : Prime n.fermatNumber)
(hn' : n ≥ 5) : type_of% selfridge_seq_conjecture
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Selfridge.lean, line 147.
Sources
TheoremSendov's conjecture#
References: - Wikipedia - Lech Mazur, A Computer-Assisted Proof of Sendov's Conjecture, ProofAtlas, August 5, 2026. - Terence Tao, A digestion of the proof of Sendov's conjecture. - Tao's Lean formalization of the digested proof.
Tags: Sendov Conjecture, Ilieff's Conjecture.
Quoted from FormalConjectures/Wikipedia/Sendov.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 3 solved.
Sendov.sendov_conjecture
Solved: stated here; a Lean proof is at https://github.com/teorth/sendov/blob/1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d/Sendov/Conjecture.lean#L156-L167.
Sendov's conjecture states that for a polynomial
\[f(z)=(z-r_{1})\cdots (z-r_{n}),\qquad (n\geq 2)\]with all roots \(r_1, ..., r_n\) inside the closed unit disk \(|z| ≤ 1\), each of the \(n\) roots is at a distance no more than \(1\) from at least one critical point.
theorem sendov_conjecture (n : ℕ) (hn : 2 ≤ n) : n.SatisfiesSendovConjecture
Category research solved; AMS 12 Field theory and polynomials, 30 Functions of a complex variable, 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/Sendov.lean, line 63.
Sendov.sendov_conjecture.variants.le_eight
Solved: stated here without proof.
Sendov's conjecture states that for a polynomial
\[f(z)=(z-r_{1})\cdots (z-r_{n}),\qquad (n\geq 2)\]with all roots \(r_1, ..., r_n\) inside the closed unit disk \(|z| ≤ 1\), each of the \(n\) roots is at a distance no more than \(1\) from at least one critical point.
It has been shown that Sendov's conjecture holds when the degree \(n\) is at most \(8\).
theorem sendov_conjecture.variants.le_eight (n : ℕ) (hn : n ∈ Set.Icc 2 8) :
n.SatisfiesSendovConjecture
Category research solved; AMS 12 Field theory and polynomials, 30 Functions of a complex variable, 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/Sendov.lean, line 74.
Sendov.sendov_conjecture.variants.eventually_true
Solved: stated here without proof.
Sendov's conjecture states that for a polynomial
\[f(z)=(z-r_{1})\cdots (z-r_{n}),\qquad (n\geq 2)\]with all roots \(r_1, ..., r_n\) inside the closed unit disk \(|z| ≤ 1\), each of the \(n\) roots is at a distance no more than \(1\) from at least one critical point.
It has been shown that Sendov's conjecture holds for polynomials of sufficiently large degree.
theorem sendov_conjecture.variants.eventually_true :
∀ᶠ (n : ℕ) in Filter.atTop, n.SatisfiesSendovConjecture
Category research solved; AMS 12 Field theory and polynomials, 30 Functions of a complex variable, 52 Convex and discrete geometry. Declared in FormalConjectures/Wikipedia/Sendov.lean, line 86.
Sources
TheoremSerre's multiplicity conjectures#
Let \(R\) be a regular local ring and let \(M\), \(N\) be finitely generated \(R\)-modules such that \(M \otimes_R N\) has finite length. Serre defined the intersection multiplicity
\[\chi(M, N) = \sum_{i \ge 0} (-1)^i \ell_R(\operatorname{Tor}_i^R(M, N)).\]He proved the dimension inequality \(\dim M + \dim N \le \dim R\) for every regular local ring, and conjectured the following three properties:
- Non-negativity: \(\chi(M, N) \ge 0\).
- Vanishing: if \(\dim M + \dim N < \dim R\), then \(\chi(M, N) = 0\).
- Positivity: if \(\dim M + \dim N = \dim R\), then \(\chi(M, N) > 0\).
Serre proved all three when \(R\) is of equal characteristic, or of mixed characteristic and unramified. Vanishing was proved in general by Roberts and, independently, by Gillet and Soulé. Non-negativity was proved in general by Gabber. Positivity is open in general. For Serre's two special cases, this file states only positivity, since non-negativity and vanishing are now known in general.
The intersection multiplicity is
Module.intersectionMultiplicity, defined inFormalConjecturesForMathlib.RingTheory.IntersectionMultiplicity.References: - Wikipedia - [Se00] J.-P. Serre, Local algebra, Springer Monographs in Mathematics, Springer, 2000, Chapter V, Part B. - [Ro85] P. Roberts, The vanishing of intersection multiplicities of perfect complexes, Bull. Amer. Math. Soc. 13 (1985), 127–130. - [GS87] H. Gillet, C. Soulé, Intersection theory using Adams operations, Invent. Math. 90 (1987), 243–277. - [Ro98] P. Roberts, Recent developments on Serre's multiplicity conjectures: Gabber's proof of the nonnegativity conjecture, Enseign. Math. 44 (1998), 305–324. - [Sk19] C. Skalit, Positivity of intersection multiplicity over a two-dimensional base, J. Pure Appl. Algebra 223 (2019), 1801–1816. arXiv:1510.05146
Quoted from FormalConjectures/Wikipedia/SerreMultiplicityConjectures.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 7 research or textbook statements: 2 open and 5 solved.
SerreMultiplicityConjectures.supportDim_add_supportDim_le_ringKrullDim
Solved: stated here without proof.
Dimension inequality. Let \(R\) be a regular local ring and let \(M\), \(N\) be finitely generated \(R\)-modules such that \(M \otimes_R N\) has finite length. Then \(\dim M + \dim N \le \dim R\). Proved by Serre for every regular local ring [Se00].
theorem supportDim_add_supportDim_le_ringKrullDim (h : IsFiniteLength R (M ⊗[R] N)) :
Module.supportDim R M + Module.supportDim R N ≤ ringKrullDim R
Category research solved; AMS 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/SerreMultiplicityConjectures.lean, line 75.
SerreMultiplicityConjectures.intersectionMultiplicity_nonneg
Solved: stated here without proof.
Non-negativity. Let \(R\) be a regular local ring and let \(M\), \(N\) be finitely generated \(R\)-modules such that \(M \otimes_R N\) has finite length. Then \(\chi(M, N) \ge 0\). Conjectured by Serre and proved by Gabber in 1995 [Ro98].
theorem intersectionMultiplicity_nonneg (h : IsFiniteLength R (M ⊗[R] N)) :
0 ≤ intersectionMultiplicity R M N
Category research solved; AMS 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/SerreMultiplicityConjectures.lean, line 85.
SerreMultiplicityConjectures.intersectionMultiplicity_eq_zero_of_lt
Solved: stated here without proof.
Vanishing. Let \(R\) be a regular local ring and let \(M\), \(N\) be finitely generated \(R\)-modules such that \(M \otimes_R N\) has finite length. If \(\dim M + \dim N < \dim R\), then \(\chi(M, N) = 0\). Conjectured by Serre and proved by Roberts [Ro85] and, independently, by Gillet and Soulé [GS87].
theorem intersectionMultiplicity_eq_zero_of_lt (h : IsFiniteLength R (M ⊗[R] N))
(hdim : Module.supportDim R M + Module.supportDim R N < ringKrullDim R) :
intersectionMultiplicity R M N = 0
Category research solved; AMS 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/SerreMultiplicityConjectures.lean, line 96.
SerreMultiplicityConjectures.intersectionMultiplicity_pos
Open: stated without proof.
Positivity conjecture. Let \(R\) be a regular local ring and let \(M\), \(N\) be finitely generated \(R\)-modules such that \(M \otimes_R N\) has finite length. If \(\dim M + \dim N = \dim R\), then \(\chi(M, N) > 0\).
The hypothesis on dimensions forces \(M\) and \(N\) to be nonzero, since the dimension of the zero module is \(\bot\).
theorem intersectionMultiplicity_pos (h : IsFiniteLength R (M ⊗[R] N))
(hdim : Module.supportDim R M + Module.supportDim R N = ringKrullDim R) :
0 < intersectionMultiplicity R M N
Category research open; AMS 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/SerreMultiplicityConjectures.lean, line 110.
SerreMultiplicityConjectures.intersectionMultiplicity_pos_quotient
Open: stated without proof.
Positivity conjecture, in the form stated on Wikipedia. Let \(R\) be a regular local ring and let \(P\), \(Q\) be prime ideals of \(R\) such that \(R/P \otimes_R R/Q\) has finite length. If \(\dim R/P + \dim R/Q = \dim R\), then \(\chi(R/P, R/Q) > 0\).
theorem intersectionMultiplicity_pos_quotient (P Q : Ideal R) [P.IsPrime] [Q.IsPrime]
(h : IsFiniteLength R ((R ⧸ P) ⊗[R] (R ⧸ Q)))
(hdim : ringKrullDim (R ⧸ P) + ringKrullDim (R ⧸ Q) = ringKrullDim R) :
0 < intersectionMultiplicity R (R ⧸ P) (R ⧸ Q)
Category research open; AMS 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/SerreMultiplicityConjectures.lean, line 121.
SerreMultiplicityConjectures.intersectionMultiplicity_pos_of_equalCharacteristic
Solved: stated here without proof.
Serre proved the positivity conjecture when \(R\) is of equal characteristic, that is, when \(R\) contains a field [Se00].
theorem intersectionMultiplicity_pos_of_equalCharacteristic (k : Type*) [Field k] [Algebra k R]
(h : IsFiniteLength R (M ⊗[R] N))
(hdim : Module.supportDim R M + Module.supportDim R N = ringKrullDim R) :
0 < intersectionMultiplicity R M N
Category research solved; AMS 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/SerreMultiplicityConjectures.lean, line 132.
SerreMultiplicityConjectures.intersectionMultiplicity_pos_of_unramified
Solved: stated here without proof.
Serre proved the positivity conjecture when \(R\) is of mixed characteristic and unramified, that is, when the characteristic \(p\) of the residue field is not in the square of the maximal ideal of \(R\) [Se00]. The hypothesis \(p \notin \mathfrak m^2\) excludes \(p = 0\) and the equal characteristic case, where \(p = 0\) in \(R\).
theorem intersectionMultiplicity_pos_of_unramified (p : ℕ) [CharP (ResidueField R) p]
(hp : (p : R) ∉ maximalIdeal R ^ 2) (h : IsFiniteLength R (M ⊗[R] N))
(hdim : Module.supportDim R M + Module.supportDim R N = ringKrullDim R) :
0 < intersectionMultiplicity R M N
Category research solved; AMS 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Wikipedia/SerreMultiplicityConjectures.lean, line 145.
Sources
TheoremSidorenko's conjecture (1993)#
References: * Wikipedia * [Si93] Sidorenko, A. (1993). "A correlation inequality for bipartite graphs." Graphs Combin. 9, pp. 201--204. * [CoFo10] Conlon, D. and Fox, J. (2010). "Bounds for graph regularity and removal lemmas." Geom. Funct. Anal. 22, pp. 1191--1256. * [KLL18] Kim, J.H., Lee, C., Lee, J. (2018). "Two approaches to Sidorenko's conjecture." Trans. Amer. Math. Soc. 370, pp. 8515--8552. * [ArXiv2605] arXiv:2605.14138 * [BR65] Blakley, G. R. and Roy, P. (1965). "A Hölder type inequality for symmetric matrices with nonnegative entries." Proc. Amer. Math. Soc. 16, pp. 1244--1245. * [OAI26a] OpenAI, A counterexample to Sidorenko's conjecture. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-counterexample-to-Sidorenkos-conjecture-September-23-2026/paper.pdf
Quoted from FormalConjectures/Wikipedia/SidorenkoConjecture.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 18 research or textbook statements: 2 open and 16 solved. It also has 9 API statements, counted here but not shown.
SidorenkoConjecture.sidorenko_conjecture
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sidorenko/RandomHost.lean#L319.
Sidorenko's conjecture (1993).
For every finite bipartite simple graph \(H\) and every finite simple graph \(G\): \(t(H, G) \ge t(K_2, G)^{e(H)}\), where \(K_2\) denotes the single-edge graph on 2 vertices (i.e.
completeGraph (Fin 2)).This is false. It was disproved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof, which gives a bipartite \(H\) with \(35\) vertices and \(66\) edges and a finite host \(G\) with \(t(H, G) < t(K_2, G)^{66}\).
theorem sidorenko_conjecture :
¬ ∀ {V W : Type} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] [Nonempty W]
(H : SimpleGraph V) (G : SimpleGraph W)
[DecidableRel H.Adj] [DecidableRel G.Adj],
H.IsBipartite →
homDensity (completeGraph (Fin 2)) G ^ H.edgeFinset.card ≤ homDensity H G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 72.
SidorenkoConjecture.sidorenko_conjecture_graphon
Solved: stated here without proof.
Sidorenko's conjecture for graphons (1993).
For every finite bipartite simple graph \(H\) and every graphon \(W\) on \([0, 1]\) with Lebesgue measure: \(t(H, W) \ge t(K_2, W)^{e(H)}\), where \(t(K_2, W) = p(W)\) is the edge density of \(W\), and \(t(H, W)\) is the graphon homomorphism density of \(H\) in \(W\).
This is false. The finite counterexample of [OAI26a] (see
sidorenko_conjecture) also refutes the graphon form: the step graphon of the finite host graph has the same homomorphism densities and the same edge density as the host. This reduction is not part of the linked Lean proof of the finite form.
theorem sidorenko_conjecture_graphon :
¬ ∀ {V : Type*} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj],
H.IsBipartite →
∀ (W : Graphon),
(graphonEdgeDensity W) ^ H.edgeFinset.card ≤ graphonHomDensity H W
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 93.
SidorenkoConjecture.sidorenko_tree_graphon
Solved: stated here without proof.
Case:
His a tree (Sidorenko 1993, graphon version).If
His a finite tree then Sidorenko's inequality holds for all graphons on \([0, 1]\).
theorem sidorenko_tree_graphon {V : Type*} [Fintype V] [DecidableEq V]
(H : SimpleGraph V) [DecidableRel H.Adj] (hTree : H.IsTree)
(W : LimitObjects.Graphon) :
(graphonEdgeDensity W) ^ H.edgeFinset.card ≤ graphonHomDensity H W
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 108.
SidorenkoConjecture.sidorenko_even_cycle_graphon
Solved: stated here without proof.
Case:
H = C_{2k}is an even cycle (Sidorenko 1993, graphon version).Every even cycle \(C_{2k}\) satisfies Sidorenko's inequality for all graphons on \([0, 1]\).
theorem sidorenko_even_cycle_graphon (k : ℕ) (hk : 1 ≤ k)
(W : LimitObjects.Graphon) :
(graphonEdgeDensity W) ^ (cycleGraph (2 * k)).edgeFinset.card ≤
graphonHomDensity (cycleGraph (2 * k)) W
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 120.
SidorenkoConjecture.sidorenko_completeBipartiteGraph_graphon
Solved: stated here without proof.
Case:
H = K_{a,b}is a complete bipartite graph (Sidorenko 1993, graphon version).Every complete bipartite graph \(K_{a,b}\) satisfies Sidorenko's inequality for all graphons on \([0, 1]\).
theorem sidorenko_completeBipartiteGraph_graphon {A B : Type*} [Fintype A] [Fintype B]
[DecidableEq A] [DecidableEq B] (W : LimitObjects.Graphon) :
(graphonEdgeDensity W) ^ (completeBipartiteGraph A B).edgeFinset.card ≤
graphonHomDensity (completeBipartiteGraph A B) W
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 133.
SidorenkoConjecture.tournament_anti_sidorenko_trees_conjecture
Open: stated without proof.
Tournament Anti-Sidorenko (TAS) Trees Conjecture.
For every finite undirected tree \(T\), there exists an orientation \(\vec{T}\) of its edges such that for any finite tournament \(G\), the homomorphism density satisfies:
\[ t_{\vec{T}}(G) \le 2^{-e(T)} \]where \(e(T)\) is the total number of edges in \(T\).
theorem tournament_anti_sidorenko_trees_conjecture :
∀ {V : Type*} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj],
T.IsTree →
∃ (D : Digraph V),
D.IsOrientation T ∧
∀ {W : Type*} [Fintype W] [DecidableEq W] [Nonempty W]
(G : Digraph W) [DecidableRel G.Adj],
G.IsTournament →
Digraph.homDensity D G ≤ (1 / 2 : ℝ) ^ T.edgeFinset.card
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 151.
SidorenkoConjecture.tournament_anti_sidorenko_trees_conjecture_tournamenton
Open: stated without proof.
Tournament Anti-Sidorenko (TAS) Trees Conjecture (Tournamenton limit version).
For every finite undirected tree \(T\), there exists an orientation \(\vec{T}\) of its edges such that for every tournamenton \(W : [0, 1]^2 \to [0, 1]\), the homomorphism density satisfies:
\[ t_{\vec{T}}(W) \le 2^{-e(T)} \]where \(e(T)\) is the total number of edges in \(T\).
theorem tournament_anti_sidorenko_trees_conjecture_tournamenton :
∀ {V : Type*} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj],
T.IsTree →
∃ (D : Digraph V),
D.IsOrientation T ∧
∀ (W : LimitObjects.Tournamenton),
tournamentonHomDensity D W ≤ (1 / 2 : ℝ) ^ T.edgeFinset.card
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 172.
SidorenkoConjecture.tournament_anti_sidorenko_single_even_degree_tree
Solved: stated here without proof.
TAS Trees Conjecture: Trees with a single even-degree vertex.
Proven case of TAS Trees Conjecture: any tree containing exactly one vertex of even degree possesses an orientation satisfying the Tournament Anti-Sidorenko inequality \(t_{\vec{T}}(G) \le 2^{-e(T)}\).
theorem tournament_anti_sidorenko_single_even_degree_tree {V : Type*} [Fintype V] [DecidableEq V]
(T : SimpleGraph V) [DecidableRel T.Adj] (hTree : T.IsTree)
(hEven : (Finset.univ.filter (fun v => Even (T.degree v))).card = 1) :
∃ (D : Digraph V),
D.IsOrientation T ∧
∀ {W : Type*} [Fintype W] [DecidableEq W] [Nonempty W]
(G : Digraph W) [DecidableRel G.Adj],
G.IsTournament →
Digraph.homDensity D G ≤ (1 / 2 : ℝ) ^ T.edgeFinset.card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 189.
SidorenkoConjecture.tournament_anti_sidorenko_spider234
Solved: stated here without proof.
TAS Trees Conjecture: The \((2,3,4)\)-spider tree (Solved case).
The \((2,3,4)\)-spider tree satisfies the Tournament Anti-Sidorenko Trees Conjecture.
Reference: * ArXiv 2605.14138
theorem tournament_anti_sidorenko_spider234 {V : Type*} [Fintype V] [DecidableEq V]
(T : SimpleGraph V) [DecidableRel T.Adj] (hSpider : IsSpider234 T) :
∃ (D : Digraph V),
D.IsOrientation T ∧
∀ {W : Type*} [Fintype W] [DecidableEq W] [Nonempty W]
(G : Digraph W) [DecidableRel G.Adj],
G.IsTournament →
Digraph.homDensity D G ≤ (1 / 2 : ℝ) ^ T.edgeFinset.card
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 226.
SidorenkoConjecture.sidorenko_K2
Proved here.
Case
H = K_2(single edge): Sidorenko's inequality holds trivially with equality.When
HisK_2(the single-edge graph on 2 vertices),e(H) = 1, so the RHS of Sidorenko's inequality is justt(K_2, G)^1 = t(K_2, G) = t(H, G), which equals the LHS. Hence the inequality holds as equality.The proof records that
(completeGraph (Fin 2)).edgeFinset.card = 1and then reduces the claim tot(K_2, G) ≤ t(K_2, G), which isle_refl.
theorem sidorenko_K2 {W : Type} [Fintype W] [DecidableEq W]
(G : SimpleGraph W) [DecidableRel G.Adj] :
homDensity (completeGraph (Fin 2)) G ^
((completeGraph (Fin 2)).edgeFinset.card) ≤
homDensity (completeGraph (Fin 2)) G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 249.
SidorenkoConjecture.sidorenko_K22
Proved here.
Case
H = K_{2,2}(four-cycle, also calledC_4): Sidorenko's conjecture holds, by Cauchy–Schwarz.The textbook statement at
H = K_{2,2}ist(K_2, G)^{e(K_{2,2})} = t(K_2, G)^4 ≤ t(K_{2,2}, G).Proof sketch. Write
d(a) := G.degree a. Then -homCount(K_2, G) = ∑_a d(a) = 2·|E(G)|(handshaking). -homCount(K_{2,2}, G) = ∑_{b₀, b₁} |N(b₀) ∩ N(b₁)|²(product structure of bipartite homomorphism). -∑_{b₀, b₁} |N(b₀) ∩ N(b₁)| = ∑_a d(a)²(swap sums). - Cauchy–Schwarz #1:(∑_{b₀, b₁} |N(b₀) ∩ N(b₁)|)² ≤ |W|² · ∑_{b₀, b₁} |N(b₀) ∩ N(b₁)|². - Cauchy–Schwarz #2:(∑_a d(a))² ≤ |W| · ∑_a d(a)². - Chain:(∑_a d(a))⁴ ≤ |W|⁴ · homCount(K_{2,2}, G). - Divide by|W|^8to gett(K_2, G)^4 ≤ t(K_{2,2}, G).The proof uses
Finset.sum_mul_sq_le_sq_mul_sq(discrete Cauchy–Schwarz) fromMathlib.Algebra.Order.BigOperators.Ring.Finset.Status (2026-04-22): main theorem closed sorry-free. See [Si93].
theorem sidorenko_K22 {W : Type} [Fintype W] [DecidableEq W]
(G : SimpleGraph W) [DecidableRel G.Adj] :
homDensity (completeGraph (Fin 2)) G ^
((completeBipartiteGraph (Fin 2) (Fin 2)).edgeFinset.card) ≤
homDensity (completeBipartiteGraph (Fin 2) (Fin 2)) G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 535.
SidorenkoConjecture.sidorenko_tree_subsingleton
Proved here.
Base case of Sidorenko for trees. When the tree
Hhas at most one vertex, both sides of Sidorenko's inequality evaluate to1(there are no edges, and every function is a homomorphism). Thus the inequality1 ≤ 1holds trivially.This covers the
|V(T)| = 1base case of the induction on tree size.
theorem sidorenko_tree_subsingleton {V W : Type} [Fintype V] [Fintype W]
[Subsingleton V] [DecidableEq V] [DecidableEq W] [Nonempty W]
(H : SimpleGraph V) (G : SimpleGraph W)
[DecidableRel H.Adj] [DecidableRel G.Adj] :
homDensity (completeGraph (Fin 2)) G ^ (H.edgeFinset.card) ≤ homDensity H G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 704.
SidorenkoConjecture.sidorenko_tree
Solved: stated here without proof.
Case:
His a tree (Sidorenko 1993).If
His a finite tree then Sidorenko's inequality holds.Proof idea (Sidorenko 1993): by induction on the tree, applying Jensen / convexity. The number of homomorphisms from a tree
Twithvvertices andv - 1edges intoGfactors nicely in the degree sequence ofG, and AM–GM / convexity gives the required lower bound.Current status (2026-04-22, partial): - The subsingleton base case (
|V(T)| ≤ 1) is dispatched viasidorenko_tree_subsingleton. - The main inductive step (leaf extraction + AM–GM on the degree sequence) is deferred; it requires a walk-parametrised homomorphism count for trees and a discrete Jensen inequality. See [Si93].The full proof is left as
sorry; the subsingleton case is closed.
theorem sidorenko_tree {V W : Type} [Fintype V] [Fintype W]
[DecidableEq V] [DecidableEq W] [Nonempty W]
(H : SimpleGraph V) (G : SimpleGraph W)
[DecidableRel H.Adj] [DecidableRel G.Adj]
(hTree : H.IsTree) :
homDensity (completeGraph (Fin 2)) G ^ (H.edgeFinset.card) ≤ homDensity H G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 737.
SidorenkoConjecture.sidorenko_conjecture.variants.complete_bipartite
Solved: stated here without proof.
Case: complete bipartite graphs
K_{s,t}(Sidorenko 1993).Sidorenko's inequality holds when
H = K_{s,t}is a complete bipartite graph. This is one of the earliest known cases; it follows from repeated applications of the Cauchy–Schwarz / Hölder inequality. Thes = t = 2instance issidorenko_K22.Reference: [Si93].
theorem sidorenko_conjecture.variants.complete_bipartite (s t : ℕ)
[DecidableRel (completeBipartiteGraph (Fin s) (Fin t)).Adj]
{W : Type} [Fintype W] [DecidableEq W] [Nonempty W]
(G : SimpleGraph W) [DecidableRel G.Adj] :
homDensity (completeGraph (Fin 2)) G ^
((completeBipartiteGraph (Fin s) (Fin t)).edgeFinset.card) ≤
homDensity (completeBipartiteGraph (Fin s) (Fin t)) G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 776.
SidorenkoConjecture.sidorenko_conjecture.variants.even_cycle
Solved: stated here without proof.
Case: even cycles
C_{2k}(Sidorenko 1993).Sidorenko's inequality holds for every even cycle
C_{2k}withk ≥ 2(cycleGraph (2 * k)). Even cycles are bipartite; thek = 2caseC_4coincides withK_{2,2}(sidorenko_K22).Reference: [Si93].
theorem sidorenko_conjecture.variants.even_cycle (k : ℕ) (hk : 2 ≤ k)
{W : Type} [Fintype W] [DecidableEq W] [Nonempty W]
(G : SimpleGraph W) [DecidableRel G.Adj] :
homDensity (completeGraph (Fin 2)) G ^
((cycleGraph (2 * k)).edgeFinset.card) ≤
homDensity (cycleGraph (2 * k)) G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 795.
SidorenkoConjecture.sidorenko_conjecture.variants.path_blakley_roy
Solved: stated here without proof.
Case: paths, the Blakley–Roy inequality (1965).
For the path
P_nonnvertices (pathGraph n), Sidorenko's inequalityt(K_2, G)^{e(P_n)} ≤ t(P_n, G)is the Blakley–Roy inequality, established well before Sidorenko's general conjecture. Paths are trees, so this is also a special case ofsidorenko_tree.Reference: [BR65].
theorem sidorenko_conjecture.variants.path_blakley_roy (n : ℕ)
[DecidableRel (pathGraph n).Adj]
{W : Type} [Fintype W] [DecidableEq W] [Nonempty W]
(G : SimpleGraph W) [DecidableRel G.Adj] :
homDensity (completeGraph (Fin 2)) G ^ ((pathGraph n).edgeFinset.card) ≤
homDensity (pathGraph n) G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 814.
SidorenkoConjecture.sidorenko_conjecture.variants.star
Proved here.
Case: stars
K_{1,m}(Sidorenko).Sidorenko's inequality holds for every star
K_{1,m} = completeBipartiteGraph (Fin 1) (Fin m). This is a fully proved instance of bothsidorenko_conjecture.variants.complete_bipartiteandsidorenko_tree(a star is a complete bipartite graph and a tree).Proof. With
d(c) := G.degree candN := |W|, the star hasmedges, so the desired inequality is(∑_c d(c) / N^2)^m ≤ (∑_c d(c)^m) / N^{m+1}(usingt(K_2, G) = ∑_c d(c) / N^2andt(K_{1,m}, G) = ∑_c d(c)^m / N^{m+1}viahomCount_star_eq_sum_degree_pow). After clearing denominators this is(∑_c d(c))^m ≤ N^{m-1} · ∑_c d(c)^m, the power-mean (Jensen) inequalityFinset.pow_sum_div_card_le_sum_pow.
theorem sidorenko_conjecture.variants.star (m : ℕ)
[DecidableRel (completeBipartiteGraph (Fin 1) (Fin m)).Adj]
{W : Type} [Fintype W] [DecidableEq W] [Nonempty W]
(G : SimpleGraph W) [DecidableRel G.Adj] :
homDensity (completeGraph (Fin 2)) G ^
((completeBipartiteGraph (Fin 1) (Fin m)).edgeFinset.card) ≤
homDensity (completeBipartiteGraph (Fin 1) (Fin m)) G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 933.
SidorenkoConjecture.sidorenko_conjecture.variants.non_bipartite_necessary
Proved here.
Bipartiteness is necessary: the triangle is not a Sidorenko graph.
The hypothesis
H.IsBipartiteinsidorenko_conjecturecannot be dropped. For the triangleH = K_3(chromatic number3, hence not bipartite) and the single edgeG = K_2, Sidorenko's inequality fails: the putative lower bound ist(K_2, K_2)^{e(K_3)} = (1/2)^3 = 1/8, while the actual density ist(K_3, K_2) = 0, because there is no graph homomorphism fromK_3into the triangle-free graphK_2(such a homomorphism would be an injectionFin 3 ↪ Fin 2). So the lower bound1/8strictly exceeds the true value0.More generally, any
Hcontaining an odd cycle fails Sidorenko's inequality against a suitable bipartiteG, since thent(H, G) = 0 < t(K_2, G)^{e(H)}.
theorem sidorenko_conjecture.variants.non_bipartite_necessary :
homDensity (completeGraph (Fin 3)) (completeGraph (Fin 2)) <
homDensity (completeGraph (Fin 2)) (completeGraph (Fin 2)) ^
((completeGraph (Fin 3)).edgeFinset.card)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SidorenkoConjecture.lean, line 992.
Sources
TheoremSierpiński number#
References: - Wikipedia, Sierpiński number - [Si60] Sierpiński, W., Elementary Theory of Numbers. Państwowe Wydawnictwo Naukowe, Warsaw (1960).
A positive odd integer \(k\) is a Sierpiński number if \(k \cdot 2^n + 1\) is composite for all natural numbers \(n\). In 1960, Sierpiński proved that there are infinitely many such numbers. John Selfridge proved in 1962 that 78557 is a Sierpiński number. It is conjectured to be the smallest.
Sierpiński problem
The Sierpiński problem asks: is 78557 the smallest Sierpiński number?
Prime Sierpiński problem
The prime Sierpiński problem asks: is 271129 the smallest prime Sierpiński number?
Extended Sierpiński problem
The extended Sierpiński problem asks: is 271129 the second-smallest Sierpiński number?
Quoted from FormalConjectures/Wikipedia/SierpinskiNumber.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: 3 open and 1 solved.
SierpinskiNumber.selfridge_78557
Proved here.
Selfridge proved in 1962 that 78557 is a Sierpiński number by showing that all numbers of the form \(78557 \cdot 2^n + 1\) have a factor in the covering set \(\{3, 5, 7, 13, 19, 37, 73\}\).
theorem selfridge_78557 : Nat.IsSierpinskiNumber 78557
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/SierpinskiNumber.lean, line 56.
SierpinskiNumber.selfridge_conjecture
Open: stated without proof.
The Sierpiński problem (Selfridge's conjecture). Is 78557 the smallest Sierpiński number?
Selfridge conjectured that 78557 is the smallest Sierpiński number. He proved in 1962 that 78557 is indeed a Sierpiński number by showing that all numbers of the form \(78557 \cdot 2^n + 1\) have a factor in the covering set \(\{3, 5, 7, 13, 19, 37, 73\}\).
theorem selfridge_conjecture :
IsLeast {k | k.IsSierpinskiNumber} 78557
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/SierpinskiNumber.lean, line 87.
SierpinskiNumber.prime_sierpinski_problem
Open: stated without proof.
The prime Sierpiński problem. Is 271129 the smallest prime Sierpiński number?
In 1976, Nathan Mendelsohn determined that the second provable Sierpiński number is the prime \(k = 271129\).
theorem prime_sierpinski_problem :
IsLeast {k | k.IsSierpinskiNumber ∧ k.Prime} 271129
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/SierpinskiNumber.lean, line 98.
SierpinskiNumber.extended_sierpinski_problem
Open: stated without proof.
The extended Sierpiński problem. Is 271129 the second-smallest Sierpiński number?
Even if 78557 is confirmed as the smallest Sierpiński number, there could exist a composite Sierpiński number \(k\) with \(78557 < k < 271129\). We formalize "second-smallest" as: the least Sierpiński number \(k\) such that there exists exactly one Sierpiński number below it.
theorem extended_sierpinski_problem :
IsLeast {k | k.IsSierpinskiNumber ∧
∃ k', k'.IsSierpinskiNumber ∧ k' < k} 271129
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/SierpinskiNumber.lean, line 110.
Sources
TheoremSingmaster's conjecture#
Singmaster's conjecture says that for any integer \(t>1\), the number of solutions to the equation:
\(\binom{n}{k} = t,\quad 1 \le k < n,\)
with \(\binom{n}{k}\) being the numbers that appear in Pascal's triangle, is bounded by a global constant \(O(1)\).
Reference: Wikipedia
Quoted from FormalConjectures/Wikipedia/Singmaster.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.
Singmaster.singmaster
Open: stated without proof.
Singmaster's conjecture: the number of times any number \(t > 1\) appears in Pascal's triangle is bounded.
theorem singmaster: ∃ (C : ℕ), ∀ (t : ℕ), t > 1 →
(Singmaster.solutions t).Finite ∧ (Singmaster.solutions t).ncard ≤ C
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Singmaster.lean, line 49.
Sources
TheoremSix standard deviations suffice (Spencer's theorem)#
Spencer's theorem in discrepancy theory: for every \(n\) and every family of \(n\) subsets \(S_1, \dots, S_n\) of \(\{1, \dots, n\}\), there is a colouring \(\chi : \{1, \dots, n\} \to \{-1, +1\}\) such that
\[\left|\sum_{j \in S_i} \chi(j)\right| \le 6\sqrt{n}\]for every \(i\).
A uniformly random colouring only achieves the bound \(O(\sqrt{n \log n})\), so Spencer's theorem ("six standard deviations suffice") is a genuine improvement over the basic probabilistic method; its proof uses a partial-colouring argument based on the entropy method, and the bound \(\Theta(\sqrt{n})\) is tight up to the value of the constant. Spencer's original argument is non-constructive; polynomial-time algorithms achieving \(O(\sqrt{n})\) were later found by Bansal (2010) and Lovett–Meka (2012).
The Komlós conjecture (the subject of a companion file in this directory) would strengthen this theorem: applied to the incidence vectors of the sets, scaled by \(1/\sqrt{n}\), it would give a discrepancy bound \(O(\sqrt{n})\) for any number of sets, not just \(n\) of them.
References: - Wikipedia - J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985), 679–706 - N. Bansal, Constructive algorithms for discrepancy minimization, FOCS 2010, 3–10 - S. Lovett and R. Meka, Constructive discrepancy minimization by walking on the edges, SIAM J. Comput. 44 (2015), 1573–1582
Quoted from FormalConjectures/Wikipedia/SixStandardDeviations.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 3 solved. It also has 1 test statement, counted here but not shown.
SixStandardDeviations.six_standard_deviations
Solved: stated here without proof.
Six standard deviations suffice (Spencer, 1985)
For every \(n\) and every family of \(n\) subsets \(S_1, \dots, S_n\) of \(\{1, \dots, n\}\), there is a colouring \(\chi : \{1, \dots, n\} \to \{-1, +1\}\) such that \(\left|\sum_{j \in S_i} \chi(j)\right| \le 6\sqrt{n}\) for every \(i\).
theorem six_standard_deviations :
∀ (n : ℕ) (S : Fin n → Finset (Fin n)),
∃ χ : Fin n → ℝ, (∀ j, χ j = 1 ∨ χ j = -1) ∧
∀ i, |∑ j ∈ S i, χ j| ≤ 6 * Real.sqrt n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SixStandardDeviations.lean, line 63.
SixStandardDeviations.six_standard_deviations.variants.random_bound
Solved: stated here; a Lean proof is at https://github.com/Lemmy00/spencer-random-coloring-lean/blob/a691214a7263c1010fdd10560091e9f8cfce903a/SpencerRandomColoring/RandomBound.lean#L37.
The random colouring bound
There is a constant \(K > 0\) such that for every \(n\) and every family of \(n\) subsets \(S_1, \dots, S_n\) of \(\{1, \dots, n\}\), there is a colouring \(\chi : \{1, \dots, n\} \to \{-1, +1\}\) with \(\left|\sum_{j \in S_i} \chi(j)\right| \le K \sqrt{n \log(n + 2)}\) for every \(i\). This follows from a Chernoff bound applied to a uniformly random colouring, and is the benchmark that Spencer's theorem improves upon by removing the logarithmic factor. (The shift \(n + 2\) inside the logarithm is a harmless normalization keeping it positive for \(n \in \{0, 1\}\).)
theorem six_standard_deviations.variants.random_bound :
∃ K : ℝ, 0 < K ∧ ∀ (n : ℕ) (S : Fin n → Finset (Fin n)),
∃ χ : Fin n → ℝ, (∀ j, χ j = 1 ∨ χ j = -1) ∧
∀ i, |∑ j ∈ S i, χ j| ≤ K * Real.sqrt (n * Real.log (n + 2))
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SixStandardDeviations.lean, line 85.
SixStandardDeviations.six_standard_deviations.variants.universal_bound
Solved: stated here; a Lean proof is at https://github.com/Lemmy00/spencer-universal-bound-lean/blob/e8d83c0a99f7c1be5a04aa155164bc477d2c6df3/Spencer/UniversalBound.lean#L15.
A universal discrepancy bound
There is a positive universal constant \(K\) such that every family of \(n\) subsets of the
npoints has a colouring with discrepancy at most \(K\sqrt{n}\) in every row. This qualitative form has the optimal order of growth, but it does not assert the constant \(6\) in Spencer's theorem.
theorem six_standard_deviations.variants.universal_bound :
∃ K : ℝ, 0 < K ∧ ∀ (n : ℕ) (S : Fin n → Finset (Fin n)),
∃ χ : Fin n → ℝ, (∀ j, χ j = 1 ∨ χ j = -1) ∧
∀ i, |∑ j ∈ S i, χ j| ≤ K * Real.sqrt n
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SixStandardDeviations.lean, line 103.
Sources
TheoremThe small Cohen-Macaulay modules conjecture#
Let \((R, \mathfrak m)\) be a Noetherian local ring of Krull dimension \(d\). A system of parameters of \(R\) is a sequence \(x_1, \dots, x_d\) of \(d\) elements of \(R\) with \(\sqrt{(x_1, \dots, x_d)} = \mathfrak m\), equivalently with \(R / (x_1, \dots, x_d)\) Artinian.
A small Cohen-Macaulay module, also called a maximal Cohen-Macaulay module, is a finitely generated \(R\)-module \(M \ne 0\) such that some system of parameters of \(R\) is a regular sequence on \(M\). A balanced big Cohen-Macaulay module is a module \(W\), not necessarily finitely generated, with \(\mathfrak m W \ne W\) and on which every system of parameters is a regular sequence. For finitely generated modules the two notions agree.
Small Cohen-Macaulay modules conjecture. If \(R\) is complete, then \(R\) has a small Cohen-Macaulay module.
Hochster conjectured this for complete local domains in the early 1970s. In the 2000s he conjectured the opposite, that there are complete local domains with no small Cohen-Macaulay module [Ho17]. Small Cohen-Macaulay modules are known to exist when \(\dim R \le 2\), and when \(R\) is \(\mathbb N\)-graded over a perfect field of characteristic \(p\) with an isolated non-Cohen-Macaulay point at the origin, a case first observed by Hartshorne and rediscovered by Peskine and Szpiro [Ho75b]. In dimension at least three the conjecture is open in every characteristic, although classes of examples keep being found there, such as three-dimensional \(F\)-pure complete local \(\mathbb F_p\)-algebras, due to Schoutens, and three-dimensional completions of \(\mathbb N\)-graded rings over a field of characteristic \(p\), due to Hochster; both are listed, with references, in [ST23]. The analogous statement for algebras is false: Bhatt constructed complete local normal domains of characteristic \(p\) admitting no module-finite extension ring that is Cohen-Macaulay [Bh14].
Balanced big Cohen-Macaulay modules, by contrast, are now known to exist over every Noetherian local ring, by Hochster in equal characteristic and by André in mixed characteristic.
Systems of parameters and Cohen-Macaulay modules are defined in
FormalConjecturesForMathlib.RingTheory.SystemOfParametersandFormalConjecturesForMathlib.RingTheory.CohenMacaulayModule.References: - Wikipedia, Homological conjectures in commutative algebra, conjectures 8 and 14. - [Ho75a] M. Hochster, Topics in the homological theory of modules over commutative rings, C.B.M.S. Regional Conf. Ser. in Math. 24, Amer. Math. Soc., 1975. - [Ho75b] M. Hochster, Big Cohen-Macaulay modules and algebras and embeddability in rings of Witt vectors, Queen's Papers in Pure and Applied Math. 42, 1975, 106-195. - [Ho17] M. Hochster, Homological conjectures and lim Cohen-Macaulay sequences, in Homological and Computational Methods in Commutative Algebra, Springer INdAM Ser. 20, Springer, 2017. PDF, Conjectures 2.1 and 2.2. - [An18] Y. André, La conjecture du facteur direct, Publ. Math. IHÉS 127 (2018), 71-93. arXiv:1609.00345. This is the paper [Ho17] credits with the existence of big Cohen-Macaulay algebras; it rests on the perfectoid Abhyankar lemma of Le lemme d'Abhyankar perfectoïde, Publ. Math. IHÉS 127 (2018), 1-70. - Stacks, Tag 00N6, on regular sequences in a Cohen-Macaulay module. - [ST23] K. Shimomoto, E. Tavanfar, Remarks on the Small Cohen-Macaulay conjecture and new instances of maximal Cohen-Macaulay modules, J. Algebra 634 (2023), 667-697. arXiv:2203.10368 - [Bh14] B. Bhatt, On the non-existence of small Cohen-Macaulay algebras, J. Algebra 411 (2014), 1-11. arXiv:1207.5413
Quoted from FormalConjectures/Wikipedia/SmallCohenMacaulayModules.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 4 research or textbook statements: 1 open, 2 solved and 1 textbook result. It also has 1 test statement, counted here but not shown.
SmallCohenMacaulayModules.exists_isSmallCohenMacaulay
Open: stated without proof.
The small Cohen-Macaulay modules conjecture. If \(R\) is a complete Noetherian local ring, then there is a finitely generated \(R\)-module \(M \ne 0\) such that some system of parameters of \(R\) is a regular sequence on \(M\).
Hochster stated the conjecture for complete local domains [Ho17, Conjecture 2.1]. The two forms are equivalent: for a minimal prime \(P\) of \(R\) with \(\dim R/P = \dim R\), a small Cohen-Macaulay module over the complete local domain \(R/P\) is one over \(R\). In the 2000s Hochster conjectured the opposite, that some complete local domain has no small Cohen-Macaulay module [Ho17, Conjecture 2.2], so this statement may well be false.
theorem exists_isSmallCohenMacaulay [IsAdicComplete (maximalIdeal R) R] :
∃ (M : Type u) (_ : AddCommGroup M) (_ : Module R M), IsSmallCohenMacaulay R M
Category research open; AMS 13 Commutative algebra. Declared in FormalConjectures/Wikipedia/SmallCohenMacaulayModules.lean, line 116.
SmallCohenMacaulayModules.exists_isSmallCohenMacaulay.variants.ringKrullDim_le_two
Solved: stated here without proof.
The conjecture holds in dimension at most \(2\). For a complete local domain the integral closure is a small Cohen-Macaulay module [Ho17]; the general case follows by passing to \(R/P\) for a minimal prime \(P\) with \(\dim R/P = \dim R\).
theorem exists_isSmallCohenMacaulay.variants.ringKrullDim_le_two
[IsAdicComplete (maximalIdeal R) R] (hR : ringKrullDim R ≤ 2) :
∃ (M : Type u) (_ : AddCommGroup M) (_ : Module R M), IsSmallCohenMacaulay R M
Category research solved; AMS 13 Commutative algebra. Declared in FormalConjectures/Wikipedia/SmallCohenMacaulayModules.lean, line 126.
SmallCohenMacaulayModules.isBalancedBigCohenMacaulay_iff_isSmallCohenMacaulay
Textbook result, stated without proof.
A finitely generated module is a balanced big Cohen-Macaulay module if and only if it is a small Cohen-Macaulay module [Ho17]. In particular, if one system of parameters is a regular sequence on a finitely generated nonzero module, then every system of parameters is; this is the "some (equivalently every)" of the Wikipedia statement. Its main ingredient is [Stacks, Tag 00N6], applied to a system of parameters of \(R\) once \(M\) is known to be Cohen-Macaulay.
theorem isBalancedBigCohenMacaulay_iff_isSmallCohenMacaulay [Module.Finite R M] :
IsBalancedBigCohenMacaulay R M ↔ IsSmallCohenMacaulay R M
Category textbook; AMS 13 Commutative algebra. Declared in FormalConjectures/Wikipedia/SmallCohenMacaulayModules.lean, line 140.
SmallCohenMacaulayModules.exists_isBalancedBigCohenMacaulay
Solved: stated here without proof.
Existence of balanced big Cohen-Macaulay modules. Every Noetherian local ring has a balanced big Cohen-Macaulay module: conjecture 8 of the Wikipedia list, and Theorem CMM of [Ho17]. Proved by Hochster in equal characteristic [Ho75a], and, using perfectoid methods, by André in mixed characteristic [An18].
theorem exists_isBalancedBigCohenMacaulay :
∃ (W : Type u) (_ : AddCommGroup W) (_ : Module R W), IsBalancedBigCohenMacaulay R W
Category research solved; AMS 13 Commutative algebra. Declared in FormalConjectures/Wikipedia/SmallCohenMacaulayModules.lean, line 151.
Sources
TheoremSnake in the box#
References: - Wikipedia - Hypercube - xkcd - [DK67] L. Danzer and V. Klee, Lengths of snakes in boxes, Journal of Combinatorial Theory 2 (1967), 258–265. - [Ze97] G. Zémor, An upper bound on the size of the snake-in-the-box, Combinatorica 17 (1997), 287–298.
Quoted from FormalConjectures/Wikipedia/SnakeInTheBox.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: 1 open and 5 solved. It also has 2 test statements, counted here but not shown.
SnakeInBox.snake_small_dimensions
Solved: stated here without proof.
The maximum length for the snake-in-the-box problem is known for dimensions zero through eight; it is \(0, 1, 2, 4, 7, 13, 26, 50, 98\).
theorem snake_small_dimensions :
map LongestSnakeInTheBox (range 9) = [0, 1, 2, 4, 7, 13, 26, 50, 98]
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SnakeInTheBox.lean, line 125.
SnakeInBox.coil_small_dimensions
Solved: stated here without proof.
The maximum length for the coil-in-the-box problem is known for dimensions zero through eight; it is \(0, 0, 4, 6, 8, 14, 26, 48, 96\).
theorem coil_small_dimensions :
map LongestCoilInTheBox (range 9) = [0, 0, 4, 6, 8, 14, 26, 48, 96]
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SnakeInTheBox.lean, line 134.
SnakeInBox.snake_dim_nine
Open: stated without proof.
For dimension \(9\), the length of the longest snake in the box is not known. This is currently the smallest dimension where this question is open.
theorem snake_dim_nine : LongestSnakeInTheBox 9 = snake_dim_nine.answer
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SnakeInTheBox.lean, line 145.
SnakeInBox.snake_dim_nine_lower_bound
Solved: stated here without proof.
The best length found so far for dimension nine is 190.
theorem snake_dim_nine_lower_bound : 190 ≤ LongestSnakeInTheBox 9
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SnakeInTheBox.lean, line 152.
SnakeInBox.snake_upper_bound
Solved: stated here without proof.
For \(n \geq 1\), an upper bound on the length of the longest snake in a box is \(2^{n-1}\) (see [DK67, Theorem B]).
theorem snake_upper_bound (n : ℕ) (hn : 1 ≤ n) : LongestSnakeInTheBox n ≤ 2 ^ (n - 1)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SnakeInTheBox.lean, line 162.
SnakeInBox.coil_upper_bound
Solved: stated here without proof.
For \(n \geq 2\), an upper bound on the maximal length of the longest coil in a box is given by
\[ 1 + 2^{n-1}\frac{6n}{6n + \frac{1}{6\sqrt{6}}n^{\frac 1 2} - 7} \](see [Ze97]). The case \(n = 1\) is excluded since the right-hand side is negative there.
theorem coil_upper_bound (n : ℕ) (hn : 2 ≤ n) : LongestCoilInTheBox n
≤ (1 : ℝ) + 2 ^ (n - 1) * (6 * n) / (6 * n + (1 / (6 * √6) * √n) - 7)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SnakeInTheBox.lean, line 173.
Sources
TheoremSolitary Numbers#
References: - Solitary number (Wikipedia) - Solitary number large clubs (Wikipedia)
Quoted from FormalConjectures/Wikipedia/SolitaryNumber.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.
SolitaryNumber.is_ten_solitary
Open: stated without proof.
Is 10 a solitary number? The smallest positive integer whose solitary status is currently unresolved is \(10\), with abundancy index \(\sigma(10) / 10 = 9/5\).
theorem is_ten_solitary : IsSolitary 10
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/SolitaryNumber.lean, line 52.
SolitaryNumber.infinite_club_exists
Open: stated without proof.
Existence of an infinite club. A club is an abundancy equivalence class, i.e. the set of all positive integers friendly with a given \(n\). It is unknown whether any club is infinite.
theorem infinite_club_exists :
∃ n, 0 < n ∧ {m : ℕ | Friendly m n}.Infinite
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/SolitaryNumber.lean, line 61.
Sources
TheoremSparse Ruler#
A sparse ruler of length \(L\) is a sequence of marks \(0 = a_1 < a_2 < \dots < a_m = L\). A distance \(k \in \mathbb{N}\) can be measured if there are \(i, j \in \{1, \dots, m\}\), such that \(k = a_j - a_i\).
One question concerns the structure of optimal rulers. Wichmann [Wi63] gave a parametric family of sparse rulers and speculated that every sufficiently large optimal ruler is of his type. The Wikipedia article records that no optimal ruler of length \(1, 13, 17, 23\) or \(58\) is a Wichmann ruler, and that every other optimal length up to \(213\) is attained by one; non-Wichmann optimal rulers also occur alongside Wichmann ones at lengths \(9, 29, 50\) and \(68\).
The asymptotic growth of the minimal number of marks of an optimal ruler of length \(L\) — i.e. the limit of \(l(n)^2 / n\), conjectured to lie in \([2.434\ldots, 3]\) — is the subject of
FormalConjectures.ErdosProblems.«170»(there phrased via \(F(N)/\sqrt{N}\)), and is not restated here.References: - [Wi63] Wichmann, B. "A note on restricted difference bases." Journal of the London Mathematical Society 38 (1963): 465-466. - Wikipedia
Quoted from FormalConjectures/Wikipedia/SparseRuler.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 open. It also has 2 API statements, counted here but not shown.
SparseRuler.wichmann_conjecture
Open: stated without proof.
Wichmann's conjecture on optimal rulers. Every optimal ruler of sufficiently large length is a Wichmann ruler \(W(r, s)\) (up to reflection, i.e. reversing the segment list). Posed by Wichmann [Wi63]. The Wikipedia article records that no optimal ruler of length \(1, 13, 17, 23\) or \(58\) is a Wichmann ruler, and that every other optimal length up to \(213\) is attained by one; non-Wichmann optimal rulers also occur alongside Wichmann ones at lengths \(9, 29, 50\) and \(68\).
theorem wichmann_conjecture :
∃ N : ℕ, ∀ g : List ℕ, IsOptimal g → N < g.sum →
∃ r s : ℕ, g = wichmannGaps r s ∨ g = (wichmannGaps r s).reverse
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SparseRuler.lean, line 104.
Sources
TheoremPacking#
This file contains a number of open problems related to the minimal size of a square (or circle) that can contain a given number of unit squares (or circles). In each case, we provide a known upper bound, and ask for the least such size.
References: - Wikipedia on packing of squares - Wikipedia on packing of circles in a circle - Wikipedia on packing of circles in a square - Friedman, Erich (2009), "Packing unit squares in squares: a survey and new results", Electronic Journal of Combinatorics, 1000, Dynamic Survey 7 - Pirl, U. (1969), "Der Mindestabstand von \(n\) in der Einheitskreisscheibe gelegenen Punkten", Mathematische Nachrichten, 40: 111–124 - A website with visualizations of packings: link - Erich Friedman, Squares in Circles - The-Anh Vu-Le, Lean 4 proof of Squares in Circles - Kenta Kitamura, Lean proof of the exact three-square minimum for Formal Conjectures
Quoted from FormalConjectures/Wikipedia/SquarePacking.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 10 research or textbook statements: 4 open, 1 solved and 5 textbook results. It also has 1 test statement, counted here but not shown.
SquarePacking.eleven_square_packing_in_square_bound
Textbook result, stated without proof.
Eleven unit squares can be packed into a square of side length < 3.877084.
Reference: Wikipedia
theorem eleven_square_packing_in_square_bound :
Nonempty (Packing 11 UnitSquare (Square 3.877084))
Category textbook; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/SquarePacking.lean, line 109.
SquarePacking.least_eleven_square_packing_in_square
Open: stated without proof.
What is the smallest square that can contain 11 unit squares?
Reference: Wikipedia
theorem least_eleven_square_packing_in_square :
IsLeast {x : ℝ | Nonempty (Packing 11 UnitSquare (Square x))}
least_eleven_square_packing_in_square.answer
Category research open; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/SquarePacking.lean, line 121.
SquarePacking.seventeen_square_packing_in_square_bound
Textbook result, stated without proof.
Seventeen unit squares can be packed into a square of side length < 4.6756.
Reference: Wikipedia
theorem seventeen_square_packing_in_square_bound :
Nonempty (Packing 17 UnitSquare (Square 4.6756))
Category textbook; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/SquarePacking.lean, line 132.
SquarePacking.least_seventeen_square_packing_in_square
Open: stated without proof.
What is the smallest square that can contain 17 unit squares?
Reference: Wikipedia
theorem least_seventeen_square_packing_in_square :
IsLeast {x : ℝ | Nonempty (Packing 17 UnitSquare (Square x))}
least_seventeen_square_packing_in_square.answer
Category research open; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/SquarePacking.lean, line 144.
SquarePacking.three_square_packing_in_circle_bound
Textbook result, stated without proof.
Three unit squares can be packed into a circle of radius \((5 \sqrt{17}) / 16 \approx 1.288\).
Reference: Wikipedia
theorem three_square_packing_in_circle_bound :
Nonempty (Packing 3 UnitSquare (Circle ((5 * NNReal.sqrt 17) / 16)))
Category textbook; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/SquarePacking.lean, line 155.
SquarePacking.least_three_square_packing_in_circle
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/three-squares-in-a-circle-lean/blob/87bd2b6915933cf608a3cae6263c2500fe81f7ec/lean/ThreeSquares/Compressed/Main.lean#L216-L219.
What is the smallest circle that can contain 3 unit squares?
The least radius is \(5\sqrt{17}/16\). The-Anh Vu-Le proved optimality in September 2026. Kenta Kitamura gave a separate Lean proof of this exact
IsLeaststatement using theSquarePackingdefinitions in this file.References: Wikipedia, Friedman's table, Vu-Le's Lean proof, and Kitamura's FC-target Lean proof.
theorem least_three_square_packing_in_circle :
IsLeast {r : ℝ≥0 | Nonempty (Packing 3 UnitSquare (Circle r))}
least_three_square_packing_in_circle.answer
Category research solved; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/SquarePacking.lean, line 177.
SquarePacking.twenty_one_circle_packing_in_square_bound
Textbook result, stated without proof.
Twenty-one unit circles can be packed into a square of side length < 9.359.
Reference: Visualizations
theorem twenty_one_circle_packing_in_square_bound :
Nonempty (Packing 21 UnitCircle (Square 9.359))
Category textbook; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/SquarePacking.lean, line 188.
SquarePacking.least_twenty_one_circle_packing_in_square
Open: stated without proof.
What is the smallest square that can contain 21 unit circles?
theorem least_twenty_one_circle_packing_in_square :
IsLeast {x : ℝ | Nonempty (Packing 21 UnitCircle (Square x))}
least_twenty_one_circle_packing_in_square.answer
Category research open; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/SquarePacking.lean, line 198.
SquarePacking.fifteen_circle_packing_in_circle_bound
Textbook result, stated without proof.
Fifteen unit circles can be packed into a circle of radius \(1 + \sqrt{6 + 2/\sqrt{5} + 4 \sqrt{1 + 2/\sqrt{5}}} \approx 4.521\).
Reference: Graham RL, Lubachevsky BD, Nurmela KJ, Ostergard PRJ. Dense packings of congruent circles in a circle. Discrete Math 1998;181:139–154.
theorem fifteen_circle_packing_in_circle_bound :
Nonempty (Packing 15 UnitCircle
(Circle (1 + NNReal.sqrt (6 + 2 / NNReal.sqrt 5 +
4 * NNReal.sqrt (1 + 2 / NNReal.sqrt 5)))))
Category textbook; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/SquarePacking.lean, line 212.
SquarePacking.least_fifteen_circle_packing_in_circle
Open: stated without proof.
What is the smallest circle that can contain 15 unit circles?
Reference: Graham RL, Lubachevsky BD, Nurmela KJ, Ostergard PRJ. Dense packings of congruent circles in a circle. Discrete Math 1998;181:139–154. Pirl (1969) conjectured this configuration to be optimal.
theorem least_fifteen_circle_packing_in_circle :
IsLeast {r : ℝ≥0 | Nonempty (Packing 15 UnitCircle (Circle r))}
least_fifteen_circle_packing_in_circle.answer
Category research open; AMS 51 Geometry. Declared in FormalConjectures/Wikipedia/SquarePacking.lean, line 229.
Sources
TheoremPolynomial-time computability of comparisons of sums of square roots#
This file formalizes the "Square-root sum problem" which asks if one can decide in polynomial time on a Turing machine whether the sum of the square roots of a list of naturals is at most a cutoff (or alternatively, at most another such sum).
This problem is relevant to questions in computational geometry (for example, in determining which of two polygonal paths in Euclidean space is longer).
Wikipedia states the problem for positive integers, an integer threshold, and lists of equal length. The versions here allow zeros, a natural-number threshold, and lists of any length. This slightly more general formulation can be reduced to the fixed length form (by removing zeros and introducing copies of \(\sqrt{4}\) to the longer list and \(\sqrt{1} + \sqrt{1}\) to the shorter one).
References: - Wikipedia: List of unsolved problems in computer science - Wikipedia: Square-root sum problem
Quoted from FormalConjectures/Wikipedia/SquareRootSum.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.
PolyTime.isPolyTime_squareRootSum
Open: stated without proof.
Is the square-root sum problem polynomial time (single sum version)?
Reference: Wikipedia
theorem isPolyTime_squareRootSum :
IsPolyTime (Function.uncurry squareRootSum)
Category research open; AMS 68 Computer science. Declared in FormalConjectures/Wikipedia/SquareRootSum.lean, line 65.
PolyTime.isPolyTime_squareRootSumTwoSided
Open: stated without proof.
Is the square-root sum problem polynomial time (two sum version)?
Reference: Wikipedia
theorem isPolyTime_squareRootSumTwoSided :
IsPolyTime (Function.uncurry squareRootSumTwoSided)
Category research open; AMS 68 Computer science. Declared in FormalConjectures/Wikipedia/SquareRootSum.lean, line 85.
Sources
TheoremSteiner Systems#
A Steiner system \(S(t, k, n)\) is a collection of \(k\)-element subsets (called blocks) of an \(n\)-element set such that every \(t\)-element subset is contained in exactly one block.
References: - Wikipedia - Large Steiner Systems by Kunal Marwaha
Quoted from FormalConjectures/Wikipedia/SteinerSystem.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 and 4 solved. It also has 1 test statement, counted here but not shown.
SteinerSystems.large_steiner_systems
Open: stated without proof.
Construct an \(S(t, k, n)\)-Steiner system with \(n > k > t > 5\), \(t < 10\), and \(n < 200\).
No example of a Steiner system with \(t > 5\) is known, despite a 2014 existence theorem by Keevash showing that such systems must exist for sufficiently large \(n\).
Reference: Large Steiner Systems
theorem large_steiner_systems : Nonempty LargeSteinerSystemWitness
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SteinerSystem.lean, line 87.
SteinerSystems.steiner_system_5_6_12
Proved here.
Existence of \(S(5, 6, 12)\): The small Witt design.
There exists a unique Steiner system \(S(5, 6, 12)\), known as the small Witt design. It was constructed by Witt (1938) and is closely related to the Mathieu group \(M_{12}\). This is one of only two known Steiner systems with \(t = 5\).
theorem steiner_system_5_6_12 : Nonempty S(5, 6, 12)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SteinerSystem.lean, line 110.
SteinerSystems.steiner_system_5_8_24
Solved: stated here without proof.
Existence of \(S(5, 8, 24)\): The large Witt design.
There exists a unique Steiner system \(S(5, 8, 24)\), known as the large Witt design. It was constructed by Witt (1938) and is closely related to the Mathieu group \(M_{24}\). This is one of only two known Steiner systems with \(t = 5\).
theorem steiner_system_5_8_24 : Nonempty S(5, 8, 24)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SteinerSystem.lean, line 253.
SteinerSystems.infinitely_many_steiner_t4
Solved: stated here without proof.
There are infinitely many Steiner systems with \(t = 4\).
Keevash (2014) proved that for any fixed \(t\) and \(k\), a Steiner system \(S(t, k, n)\) exists for all sufficiently large \(n\) satisfying the necessary divisibility conditions. Since there are infinitely many such admissible \(n\), this implies infinitely many \(S(4, k, n)\) systems exist (for any fixed \(k > 4\)). The proof is nonconstructive.
Explicit examples include \(S(4, 5, 11)\) (the unique system, related to the Mathieu group \(M_{11}\)) and \(S(4, 7, 23)\) (related to the Mathieu group \(M_{23}\)).
Only nontrivial systems with \(4 < k < n\) are counted: for every \(n\) the single block \(\{1, \dots, n\}\) is an \(S(4, n, n)\), and all \(4\)-subsets of an \(n\)-set form an \(S(4, 4, n)\).
theorem infinitely_many_steiner_t4 :
{s : Σ k n : ℕ, S(4, k, n) | 4 < s.1 ∧ s.1 < s.2.1}.Infinite
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SteinerSystem.lean, line 271.
SteinerSystems.infinitely_many_steiner_t5
Solved: stated here without proof.
There are infinitely many Steiner systems with \(t = 5\).
Keevash (2014) proved that for any fixed \(t\) and \(k\), a Steiner system \(S(t, k, n)\) exists for all sufficiently large \(n\) satisfying the necessary divisibility conditions. This settles the long-standing open problem of whether infinitely many \(S(5, k, n)\) systems exist. The proof is nonconstructive.
Only two explicit examples are known: \(S(5, 6, 12)\) and \(S(5, 8, 24)\), both Witt designs related to the Mathieu groups \(M_{12}\) and \(M_{24}\) respectively.
Only nontrivial systems with \(5 < k < n\) are counted, for the same reason as in
infinitely_many_steiner_t4. No Steiner system with \(t \geq 6\) has been explicitly constructed, though Keevash's result guarantees their existence nonconstructively as well.
theorem infinitely_many_steiner_t5 :
{s : Σ k n : ℕ, S(5, k, n) | 5 < s.1 ∧ s.1 < s.2.1}.Infinite
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SteinerSystem.lean, line 292.
Sources
TheoremSumner's universal tournament conjecture (1971)#
References: * Wikipedia * [HT91] Häggkvist, R. and Thomason, A. (1991). "Trees in tournaments." Combinatorica 11, pp. 123--130. * [ES04] El Sahili, A. (2004). "Trees in tournaments." J. Combin. Theory Ser. B 92, pp. 183--187. * [KMO11] Kühn, D., Mycroft, R. and Osthus, D. (2011). "A proof of Sumner's universal tournament conjecture for large tournaments." Proc. London Math. Soc. 102, pp. 731--766. arXiv:1010.4430
Quoted from FormalConjectures/Wikipedia/SumnerUniversalTournamentConjecture.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.
SumnerUniversalTournamentConjecture.sumner_conjecture
Open: stated without proof.
Sumner's universal tournament conjecture (1971).
Every tournament on \(2n - 2\) vertices contains every oriented tree on \(n \ge 2\) vertices as a subgraph.
theorem sumner_conjecture :
∀ (n : ℕ), 2 ≤ n →
∀ {W : Type} [Fintype W] [DecidableEq W] (D : Digraph W) [DecidableRel D.Adj],
Fintype.card W = n → IsOrientedTree D →
∀ {V : Type} [Fintype V] [DecidableEq V] (G : Digraph V) [DecidableRel G.Adj],
Fintype.card V = 2 * n - 2 → G.IsTournament → Embeds D G
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SumnerUniversalTournamentConjecture.lean, line 57.
SumnerUniversalTournamentConjecture.sumner_conjecture.variants.large_n
Solved: stated here without proof.
Kühn–Mycroft–Osthus (2011): the conjecture holds for all sufficiently large \(n\).
Reference: [KMO11].
theorem sumner_conjecture.variants.large_n :
∃ n₀ : ℕ, ∀ (n : ℕ), n₀ ≤ n →
∀ {W : Type} [Fintype W] [DecidableEq W] (D : Digraph W) [DecidableRel D.Adj],
Fintype.card W = n → IsOrientedTree D →
∀ {V : Type} [Fintype V] [DecidableEq V] (G : Digraph V) [DecidableRel G.Adj],
Fintype.card V = 2 * n - 2 → G.IsTournament → Embeds D G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SumnerUniversalTournamentConjecture.lean, line 71.
SumnerUniversalTournamentConjecture.sumner_conjecture.variants.el_sahili
Solved: stated here without proof.
El Sahili (2004): tournaments on \(3n - 3\) vertices suffice.
Every tournament on \(3n - 3\) vertices contains every oriented tree on \(n \ge 2\) vertices, improving the bound \(12n\) of Häggkvist and Thomason [HT91].
Reference: [ES04].
theorem sumner_conjecture.variants.el_sahili (n : ℕ) (hn : 2 ≤ n)
{W : Type} [Fintype W] [DecidableEq W] (D : Digraph W) [DecidableRel D.Adj]
(hW : Fintype.card W = n) (hD : IsOrientedTree D)
{V : Type} [Fintype V] [DecidableEq V] (G : Digraph V) [DecidableRel G.Adj]
(hV : Fintype.card V = 3 * n - 3) (hG : G.IsTournament) : Embeds D G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SumnerUniversalTournamentConjecture.lean, line 88.
SumnerUniversalTournamentConjecture.sumner_conjecture.variants.sharp
Solved: stated here without proof.
The bound \(2n - 2\) would be sharp.
For every \(n \ge 2\) there is an oriented tree on \(n\) vertices — the out-star, with arcs from a centre to the \(n - 1\) other vertices — that embeds in no regular tournament on \(2n - 3\) vertices: every vertex of such a tournament has out-degree \(n - 2 < n - 1\).
theorem sumner_conjecture.variants.sharp (n : ℕ) (hn : 2 ≤ n) :
∃ (W : Type) (_ : Fintype W) (_ : DecidableEq W) (D : Digraph W) (_ : DecidableRel D.Adj),
Fintype.card W = n ∧ IsOrientedTree D ∧
∃ (V : Type) (_ : Fintype V) (_ : DecidableEq V) (G : Digraph V) (_ : DecidableRel G.Adj),
Fintype.card V = 2 * n - 3 ∧ G.IsTournament ∧ ¬ Embeds D G
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Wikipedia/SumnerUniversalTournamentConjecture.lean, line 103.
Sources
TheoremSum of three cubes#
An integer
n : ℤcan be written as a sum of three cubes (of integers) if and only ifnis not4or5mod9.References: - Wikipedia - mathoverflow/100324 asked by user David Feldman
Quoted from FormalConjectures/Wikipedia/SumOfThreeCubes.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 4 test statements, counted here but not shown.
SumOfThreeCubes.isSumOfThreeCubesRat_any
Proved here.
Any rational number is a sum of three rational cubes.
First proved by Ryley in 1825, which can be found in [Ri1930]. The below parametrization is brought from the MSE answer [MSE].
[Ri1930] Richmond, H. W. "On Rational Solutions of \(x^3 + y^3 + z^3 = R\)." Proceedings of the Edinburgh Mathematical Society 2.2 (1930): 92-100. [MSE] Kieren MacMillan, Proving that any rational number can be represented as the sum of the cubes of three rational numbers, https://math.stackexchange.com/q/4480969
theorem isSumOfThreeCubesRat_any (r : ℚ) : IsSumOfThreeCubes r
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/SumOfThreeCubes.lean, line 78.
SumOfThreeCubes.isSumOfThreeCubes_iff_mod_9
Open: stated without proof.
An integer
n : ℤcan be written as a sum of three cubes (of integers) if and only ifnis not4or5mod9.
theorem isSumOfThreeCubes_iff_mod_9 :
∀ n : ℤ, IsSumOfThreeCubes n ↔ ¬(n ≡ 4 [ZMOD 9] ∨ n ≡ 5 [ZMOD 9])
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/SumOfThreeCubes.lean, line 93.
Sources
Theorem(m,k)-perfect numbers#
A positive integer \(n\) is \((m,k)\)-perfect if \(\sigma^m(n)=kn\), where \(\sigma^m\) is the \(m\)-th iterate of the sum-of-divisors function.
Quoted from FormalConjectures/Wikipedia/Superperfectnumbers.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.
Superperfect.twoFivePerfect
Open: stated without proof.
There does not exist a \((2,5)\)-perfect number
theorem twoFivePerfect : ¬ ∃ n, Nat.IsPerfectFor n 2 5
Category research open; AMS 11 Number theory. Declared in FormalConjectures/Wikipedia/Superperfectnumbers.lean, line 45.
Sources
TheoremGottschalk's surjunctivity conjecture#
A group \(G\) is surjunctive if every injective, continuous, \(G\)-equivariant map \(A^G \to A^G\) (for any finite alphabet \(A\)) is surjective.
Here equivariance is with respect to the left shift action of \(G\) on \(A^G\), defined by \((g \cdot x)(h) = x(g^{-1} h)\), and continuity is with respect to the product topology on \(A^G\) (where \(A\) carries the discrete topology).
Gottschalk's conjecture (1973) states that every group is surjunctive. It is false: an internal OpenAI model gave counterexamples in September 2026 [OAI26a], [OAI26b].
References: - Wikipedia - Gottschalk, W. H. (1973), "Some general dynamical notions" - [OAI26a] OpenAI, A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Characteristic Two. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Counterexample-to-Kaplanskys-Direct-Finiteness-Conjecture-in-Characteristic-Two-September-23-2026/paper.pdf - [OAI26b] OpenAI, A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Odd Characteristic. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Counterexample-to-Kaplanskys-Direct-Finiteness-Conjecture-in-Odd-Characteristic-September-26-2026/paper.pdf
Quoted from FormalConjectures/Wikipedia/SurjunctiveGroup.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 solved and 1 textbook result. It also has 3 API statements, counted here but not shown.
GottschalkSurjunctivity.gottschalk_surjunctivity_conjecture
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Algebra/OddKaplansky/Main.lean#L81.
Gottschalk's surjunctivity conjecture (1973): every group is surjunctive. That is, for every group
Gand every finite alphabetA, every injective cellular automaton onA^Gis surjective.This is false. It was disproved by an internal OpenAI model in September 2026 [OAI26a], [OAI26b]; see
counter_gottschalk_surjunctivityfor the counterexample and for what the linked Lean proof covers.
theorem gottschalk_surjunctivity_conjecture :
¬ ∀ (G : Type) [Group G], IsSurjunctive G
Category research solved; AMS 20 Group theory and generalizations, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Wikipedia/SurjunctiveGroup.lean, line 98.
GottschalkSurjunctivity.counter_gottschalk_surjunctivity
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Algebra/OddKaplansky/Main.lean#L81.
Gottschalk's surjunctivity conjecture is false: there is a group that is not surjunctive.
There are a finite field \(K\), a group \(G\) and \(a, b \in K[G]\) with \(ab = 1\) and \(ba \neq 1\). The linear cellular automaton \(x \mapsto (g \mapsto \sum_u b_u x(gu))\) on \(K^G\) is then injective but not surjective. In [OAI26a], \(K\) has characteristic two and \(G\) is finitely presented. In [OAI26b], \(K\) has odd characteristic and \(G\) is finitely generated.
This was proved by an internal OpenAI model in September 2026. The linked Lean proof is for [OAI26b]. It shows that the map above is injective and not surjective. That the map is continuous and shift-equivariant, as
IsSurjunctiverequires, is not part of the linked proof.
theorem counter_gottschalk_surjunctivity :
∃ (G : Type) (_ : Group G), ¬ IsSurjunctive G
Category research solved; AMS 20 Group theory and generalizations, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Wikipedia/SurjunctiveGroup.lean, line 118.
GottschalkSurjunctivity.isSurjunctive_of_finite
Textbook result, proved here.
Every finite group is surjunctive. This is a classical result: an injective endomorphism of a finite set is surjective.
theorem isSurjunctive_of_finite (G : Type) [Group G] [Finite G] :
IsSurjunctive G
Category textbook; AMS 20 Group theory and generalizations, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Wikipedia/SurjunctiveGroup.lean, line 125.
Sources
TheoremTarski's exponential function problem#
Tarski proved that the first-order theory of the real ordered field \((\mathbb{R}, +, \cdot, -, 0, 1, \le)\) is decidable, and asked whether the same holds for the real exponential field \(\mathbb{R}_{\exp} = (\mathbb{R}, +, \cdot, -, 0, 1, \le, \exp)\). The problem is open. Macintyre and Wilkie proved that the theory of \(\mathbb{R}_{\exp}\) is decidable if the real version of Schanuel's conjecture holds.
Decidability of a theory is formalised in
FirstOrder.Language.Theory.IsDecidable: the set of consequences of the theory is computable, with respect to the Gödel numbering of sentences fromFormalConjecturesForMathlib.ModelTheory.Encoding. The theory in question is the complete theory of \(\mathbb{R}_{\exp}\), which contains every sentence true in \(\mathbb{R}_{\exp}\), so this is the same as asking for an algorithm deciding membership (FirstOrder.Language.Theory.isDecidable_completeTheory_iff). The statements use the language of ordered rings with the order symbol≤in place of<. Some sources state the problem for \((\mathbb{R}, +, \cdot, \exp)\) instead. Since \(<\), \(\le\), \(-\), \(0\) and \(1\) are definable from \(+\) and \(\cdot\), all these structures are interdefinable, and the choice does not affect decidability.References: - Wikipedia, Tarski's exponential function problem, listed in Wikipedia, List of unsolved problems in mathematics. - A. Tarski, A decision method for elementary algebra and geometry, 2nd ed., University of California Press, Berkeley and Los Angeles, 1951. - A. Macintyre, A. J. Wilkie, On the decidability of the real exponential field, in: P. Odifreddi (ed.), Kreiseliana: about and around Georg Kreisel, A K Peters, Wellesley, MA, 1996, pp. 441–467. - S. Kuhlmann, Model theory of the real exponential function, Encyclopedia of Mathematics. - A. Berarducci, F. Gallinaro, On the elementary theory of the real exponential field, arXiv:2603.08365 (2026). Assuming Schanuel's conjecture, gives an axiomatisation of the theory of \(\mathbb{R}_{\exp}\) and recovers the Macintyre–Wilkie decidability result.
Quoted from FormalConjectures/Wikipedia/TarskiExponentialFunctionProblem.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 API statement, counted here but not shown.
TarskiExponentialFunctionProblem.isDecidable_completeTheory_real_orderedField
Solved: stated here without proof.
Tarski's theorem. The first-order theory of the real ordered field \((\mathbb{R}, +, \cdot, -, 0, 1, \le)\) is decidable.
theorem isDecidable_completeTheory_real_orderedField :
((Language.ring.sum Language.order).completeTheory ℝ).IsDecidable
Category research solved; AMS 03 Mathematical logic and foundations, 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/TarskiExponentialFunctionProblem.lean, line 66.
TarskiExponentialFunctionProblem.tarski_exponential_function_problem
Open: stated without proof.
Tarski's exponential function problem. Is the first-order theory of the real exponential field \(\mathbb{R}_{\exp} = (\mathbb{R}, +, \cdot, -, 0, 1, \le, \exp)\) decidable?
theorem tarski_exponential_function_problem :
(Language.orderedExpField.completeTheory ℝ).IsDecidable
Category research open; AMS 03 Mathematical logic and foundations, 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/TarskiExponentialFunctionProblem.lean, line 75.
TarskiExponentialFunctionProblem.isDecidable_completeTheory_realExp_of_realSchanuelConjecture
Solved: stated here without proof.
Macintyre–Wilkie. If the real version of Schanuel's conjecture holds, then the first-order theory of the real exponential field is decidable.
theorem isDecidable_completeTheory_realExp_of_realSchanuelConjecture
(h : RealSchanuelConjecture) :
(Language.orderedExpField.completeTheory ℝ).IsDecidable
Category research solved; AMS 03 Mathematical logic and foundations, 11 Number theory, 12 Field theory and polynomials. Declared in FormalConjectures/Wikipedia/TarskiExponentialFunctionProblem.lean, line 112.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.