Generic and maximal rank of… to TxGraffiti Conjecture 1…

TheoremGeneric and maximal rank of 3-tensors#

The rank of a tensor \(T \in \mathbb{C}^{m_1} \otimes \mathbb{C}^{m_2} \otimes \mathbb{C}^{m_3}\) is the least \(r\) such that \(T\) is a sum of \(r\) decomposable tensors \(a \otimes b \otimes c\). Mathlib records such a tensor as a Holor ℂ [m₁, m₂, m₃] and its rank as Holor.cprank.

Two basic invariants of the format \((m_1, m_2, m_3)\) are the generic rank \(\operatorname{grank}(m_1, m_2, m_3)\), the rank of a generic tensor, and the maximal rank \(\operatorname{mrank}(m_1, m_2, m_3)\), the largest rank attained by a tensor of that format.

Counting parameters gives the lower bound \(\operatorname{grank}(m_1, m_2, m_3) \geq r_0(m_1, m_2, m_3) := \lceil m_1m_2m_3 / (m_1 + m_2 + m_3 - 2) \rceil\). Once \(m_3\) exceeds \((m_1-1)(m_2-1)\) the generic rank is known to be \(\min(m_3, m_1m_2)\), so the interesting case is the critical range \(3 \leq m_1 \leq m_2 \leq m_3 \leq (m_1-1)(m_2-1)\) [Fri12, Conjecture 5.1; BFZ24, (4.14)]. There the bound \(r_0\) is attained in every case that has been settled, except for the formats \((3, 2p+1, 2p+1)\), where the generic rank is \(r_0 + 1\). Friedland's conjecture, stated here as isGenericRank_of_le_critical, is that these are the only exceptions. The boundary case \(m_3 = (m_1-1)(m_2-1)\) is settled in [Fri12, Corollary 6.4(2)] and recorded as isGenericRank_of_eq_critical.

The maximal rank is much less well understood. It is known for the formats \(2 \times m \times n\) and for a range of small formats, but no formula is known even for \((n, n, n)\), and \(\operatorname{mrank}(3, 3, 5)\) is undetermined.

Tensor rank is invariant under permuting the three factors, but Holor ℂ [m₁, m₂, m₃] and its permutations are different types and Mathlib has no transport lemma between them. Each statement below therefore writes the format in the order its own source uses.

References: * [Fri12] S. Friedland, On the generic and typical ranks of 3-tensors, Linear Algebra Appl. 436 (2012), 478-497, https://doi.org/10.1016/j.laa.2011.05.008 (arxiv/0805.3777). Conjecture 5.1, and the survey of known values in Section 5. * [BFZ24] W. Bruzda, S. Friedland, K. Życzkowski, Rank of a tensor and quantum entanglement, Linear Multilinear Algebra 72 (2024), 1796-1859, https://doi.org/10.1080/03081087.2023.2211717 (arxiv/1912.06854v4). A survey; the numbering used below is that of the arXiv v4 PDF. Conjecture 4.12 restates [Fri12, Conjecture 5.1], and Sections 4.5 and 4.6 collect the current status. * [CGG02] M. V. Catalisano, A. V. Geramita, A. Gimigliano, Ranks of tensors, secant varieties of Segre varieties and fat points, Linear Algebra Appl. 355 (2002), 263-285, https://doi.org/10.1016/S0024-3795(02)00352-X. Used for isGenericRank_of_gt_critical. * [Str83] V. Strassen, Rank and optimal computation of generic tensors, Linear Algebra Appl. 52/53 (1983), 645-685, https://doi.org/10.1016/0024-3795(83)80041-X. Used for isGenericRank_three_even and isGenericRank_three_odd. * [AOP09] H. Abo, G. Ottaviani, C. Peterson, Induction for secant varieties of Segre varieties, Trans. Amer. Math. Soc. 361 (2009), 767-792, https://doi.org/10.1090/S0002-9947-08-04725-9. Used for isGenericRank_four. * [Lic85] T. Lickteig, Typical tensorial rank, Linear Algebra Appl. 69 (1985), 95-120, https://doi.org/10.1016/0024-3795(85)90070-9. Used for isGenericRank_cube. * [AS79] M. D. Atkinson, N. M. Stephens, On the maximal multiplicative complexity of a family of bilinear forms, Linear Algebra Appl. 27 (1979), 1-8, https://doi.org/10.1016/0024-3795(79)90026-0. Used for isMaxRank_two, cprank_le_of_three_slices, cprank_le_of_square_slices, isMaxRank_of_le_min and isMaxRank_three_three_five_bounds. * [JaJa79] J. JáJá, Optimal evaluation of pairs of bilinear forms, SIAM J. Comput. 8 (1979), 443-462, https://doi.org/10.1137/0208037, and J. B. Kruskal, Rank, decomposition, and uniqueness for 3-way and N-way arrays, in Multiway Data Analysis, North-Holland (1989), 7-18. Cited by [Fri12] for isMaxRank_two. * [SMS10] T. Sumi, M. Miyazaki, T. Sakata, About the maximal rank of 3-tensors over the real and the complex number field, Ann. Inst. Statist. Math. 62 (2010), 807-822, https://doi.org/10.1007/s10463-010-0294-5 (arxiv/0806.4048). Theorem 4.5 proves the first of the two bounds that [AS79] states without proof; Proposition 4.9(1) is the special case used for isMaxRank_three. * [Ki26] K. Kitamura, A Lean proof that the maximal rank of complex \(3 \times 3 \times 5\) tensors is 6, GitHub repository (2026), https://github.com/KitaKen1/mrank-3-3-5-lean. Used for isMaxRank_three_three_five. * [BT15] G. Blekherman, Z. Teitler, On maximum, typical and generic ranks, Math. Ann. 362 (2015), 1021-1031, https://doi.org/10.1007/s00208-014-1150-3 (arxiv/1402.2371), Theorem 1. Used for isMaxRank_le_two_mul_isGenericRank.

Quoted from FormalConjectures/Arxiv/0805.3777/TensorRank.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, 15 solved and 1 textbook result. It also has 1 test statement and 5 API statements, counted here but not shown.

Arxiv.«0805.3777».isGenericRank_matrix

Textbook result, stated without proof.

The generic rank of an \(m \times n\) matrix is \(\min(m, n)\): the 2-tensor case.

theorem isGenericRank_matrix (m n : ℕ) : IsGenericRank [m, n] (min m n)

Category textbook; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 183.

Arxiv.«0805.3777».isGenericRank_of_gt_critical

Solved: stated here without proof.

Above the critical range, a generic tensor of format \((m_1, m_2, m_3)\) has rank \(\min(m_3, m_1m_2)\) [Fri12, (5.1)].

theorem isGenericRank_of_gt_critical {m₁ m₂ m₃ : ℕ} (h₁ : 1 ≤ m₁) (h₁₂ : m₁ ≤ m₂) (h₂₃ : m₂ ≤ m₃)
    (h : (m₁ - 1) * (m₂ - 1) < m₃) :
    IsGenericRank [m₁, m₂, m₃] (min m₃ (m₁ * m₂))

Category research solved; AMS 14 Algebraic geometry, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 191.

Arxiv.«0805.3777».isGenericRank_three_even

Solved: stated here without proof.

The generic rank of a \(3 \times 2p \times 2p\) tensor is \(\lceil 12p^2 / (4p + 1) \rceil\), the value \(r_0\) predicted by a dimension count [Fri12, (5.3)]. The hypothesis \(2 \leq p\) is the ordering \(3 \leq 2p\) of the format.

theorem isGenericRank_three_even {p : ℕ} (hp : 2 ≤ p) :
    IsGenericRank [3, 2 * p, 2 * p] (12 * p ^ 2 ⌈/⌉ (4 * p + 1))

Category research solved; AMS 14 Algebraic geometry, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 200.

Arxiv.«0805.3777».isGenericRank_three_odd

Solved: stated here without proof.

The generic rank of a \(3 \times (2p+1) \times (2p+1)\) tensor is \(\lceil 3(2p+1)^2 / (4p + 3) \rceil + 1\), one more than the value \(r_0\) predicted by a dimension count [Fri12, (5.4)]. These are the only formats in the critical range known to exceed \(r_0\). The case \(p = 1\) says that the generic rank of a \(3 \times 3 \times 3\) tensor is 5, not 4.

theorem isGenericRank_three_odd {p : ℕ} (hp : 1 ≤ p) :
    IsGenericRank [3, 2 * p + 1, 2 * p + 1] (3 * (2 * p + 1) ^ 2 ⌈/⌉ (4 * p + 3) + 1)

Category research solved; AMS 14 Algebraic geometry, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 211.

Arxiv.«0805.3777».isGenericRank_four

Solved: stated here without proof.

The generic rank of a \(4 \times m \times m\) tensor is \(\lceil 4m^2 / (2m + 2) \rceil\) [Fri12, (5.7)]. This is the case \((4, m, m)\) of isGenericRank_of_le_critical, settled in [AOP09]; see [BFZ24, Section 4.5].

theorem isGenericRank_four {m : ℕ} (hm : 3 ≤ m) :
    IsGenericRank [4, m, m] (4 * m ^ 2 ⌈/⌉ (2 * m + 2))

Category research solved; AMS 14 Algebraic geometry, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 219.

Arxiv.«0805.3777».isGenericRank_cube

Solved: stated here without proof.

For \(n \neq 3\) the generic rank of an \(n \times n \times n\) tensor is \(\lceil n^3 / (3n - 2) \rceil\) [Fri12, (5.8)].

theorem isGenericRank_cube {n : ℕ} (hn : 1 ≤ n) (hn3 : n ≠ 3) :
    IsGenericRank [n, n, n] (n ^ 3 ⌈/⌉ (3 * n - 2))

Category research solved; AMS 14 Algebraic geometry, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 226.

Arxiv.«0805.3777».isGenericRank_of_eq_critical

Solved: stated here without proof.

The generic rank at the critical boundary is \((m_1-1)(m_2-1)+1\) [Fri12, Corollary 6.4(2)]. By critical_ceilDiv, this is the dimension-count value in isGenericRank_of_le_critical.

theorem isGenericRank_of_eq_critical {m₁ m₂ : ℕ} (h₁ : 3 ≤ m₁) (h₁₂ : m₁ ≤ m₂) :
    IsGenericRank [m₁, m₂, (m₁ - 1) * (m₂ - 1)] ((m₁ - 1) * (m₂ - 1) + 1)

Category research solved; AMS 14 Algebraic geometry, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 263.

Arxiv.«0805.3777».isGenericRank_of_le_critical

Open: stated without proof.

Friedland's conjecture. In the critical range \(m_3 \leq (m_1 - 1)(m_2 - 1)\), and away from the formats \((3, 2p+1, 2p+1)\), the generic rank of a tensor of format \((m_1, m_2, m_3)\) is the value \(\lceil m_1m_2m_3 / (m_1 + m_2 + m_3 - 2) \rceil\) predicted by a dimension count [Fri12, Conjecture 5.1]. The boundary \(m_3 = (m_1-1)(m_2-1)\) is settled by isGenericRank_of_eq_critical [Fri12, (5.11)]. It is known for \(m_1 \leq 4\) and for \((n, n, n)\), and has been verified numerically throughout the critical range for \(m_3 \leq 20\) [BFZ24, Section 4.5].

theorem isGenericRank_of_le_critical {m₁ m₂ m₃ : ℕ} (h₁ : 3 ≤ m₁) (h₁₂ : m₁ ≤ m₂) (h₂₃ : m₂ ≤ m₃)
    (h : m₃ ≤ (m₁ - 1) * (m₂ - 1)) (hexc : ∀ p : ℕ, (m₁, m₂, m₃) ≠ (3, 2 * p + 1, 2 * p + 1)) :
    IsGenericRank [m₁, m₂, m₃] (m₁ * m₂ * m₃ ⌈/⌉ (m₁ + m₂ + m₃ - 2))

Category research open; AMS 14 Algebraic geometry, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 277.

Arxiv.«0805.3777».isMaxRank_two

Solved: stated here without proof.

The maximal rank of a \(2 \times m \times n\) tensor is \(m + \min(m, \lfloor n/2 \rfloor)\) [Fri12, (5.13)]; equivalently [BFZ24, (4.9)].

theorem isMaxRank_two {m n : ℕ} (hm : 2 ≤ m) (hmn : m ≤ n) :
    IsMaxRank [2, m, n] (m + min m (n / 2))

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 285.

Arxiv.«0805.3777».cprank_le_of_three_slices

Solved: stated here without proof.

Every \(n \times n \times 3\) tensor has rank at most \(2n - 1\) [SMS10, Theorem 4.5].

theorem cprank_le_of_three_slices {n : ℕ} (hn : 1 ≤ n) (T : Holor ℂ [n, n, 3]) :
    T.cprank ≤ 2 * n - 1

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 291.

Arxiv.«0805.3777».isMaxRank_three

Solved: stated here without proof.

The maximal rank of a \(3 \times 3 \times 3\) tensor is 5. The upper bound is [SMS10, Proposition 4.9(1)], a special case of cprank_le_of_three_slices; the lower bound is the generic rank isGenericRank_three_odd at \(p = 1\).

theorem isMaxRank_three : IsMaxRank [3, 3, 3] 5

Category research solved; AMS 14 Algebraic geometry, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 299.

Arxiv.«0805.3777».isMaxRank_of_le_min

Solved: stated here without proof.

For \(u \leq \min(4, m)\) the maximal rank of an \(m \times n \times (mn - u)\) tensor is \(mn - \lceil u/2 \rceil\) [BFZ24, (4.24)].

theorem isMaxRank_of_le_min {m n u : ℕ} (hm : 3 ≤ m) (hmn : m ≤ n) (hu : u ≤ min 4 m) :
    IsMaxRank [m, n, m * n - u] (m * n - u ⌈/⌉ 2)

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 305.

Arxiv.«0805.3777».isMaxRank_three_three_five_bounds

Solved: stated here without proof.

The maximal rank of a \(3 \times 3 \times 5\) tensor is 6 or 7 [BFZ24, (4.20)].

theorem isMaxRank_three_three_five_bounds {R : ℕ} (hR : IsMaxRank [3, 3, 5] R) :
    6 ≤ R ∧ R ≤ 7

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 311.

Arxiv.«0805.3777».isMaxRank_three_three_five

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/mrank-3-3-5-lean/blob/fbec93aa021bd994380cd27eb60e444e7cc85e93/lean/TensorRank335FC.lean#L3365-L3367.

Determine the maximal rank of a \(3 \times 3 \times 5\) tensor. It was the one undetermined entry of the table of \(\operatorname{mrank}(3, 3, p)\) for \(p \leq 9\) [BFZ24, (4.20)]. The answer is 6. A Lean proof is given in [Ki26].

theorem isMaxRank_three_three_five : IsMaxRank [3, 3, 5] isMaxRank_three_three_five.answer

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 324.

Arxiv.«0805.3777».isMaxRank_le_two_mul_isGenericRank

Solved: stated here without proof.

The maximal rank is at most twice the generic rank [BT15, Theorem 1].

theorem isMaxRank_le_two_mul_isGenericRank {ds : List ℕ} {r R : ℕ} (hr : IsGenericRank ds r)
    (hR : IsMaxRank ds R) : R ≤ 2 * r

Category research solved; AMS 14 Algebraic geometry, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 329.

Arxiv.«0805.3777».cprank_le_of_square_slices

Solved: stated here without proof.

Every complex \(m \times n \times n\) tensor has rank at most \(\lfloor (m+1)n/2 \rfloor\) for \(m,n \geq 3\) [BFZ24, (4.22)].

theorem cprank_le_of_square_slices {m n : ℕ} (hm : 3 ≤ m) (hn : 3 ≤ n)
    (T : Holor ℂ [m, n, n]) : T.cprank ≤ (m + 1) * n / 2

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 336.

Arxiv.«0805.3777».isMaxRank_cube_bounds

Proved here.

For \(n \geq 4\), the maximal rank \(R\) of a complex cubic tensor satisfies \(\lceil n^3/(3n-2) \rceil \leq R \leq n(n+1)/2\) [BFZ24, (4.22), (4.25)-(4.28)]. The lower bound is the generic rank; the upper bound is the square-slice estimate.

theorem isMaxRank_cube_bounds {n R : ℕ} (hn : 4 ≤ n) (hR : IsMaxRank [n, n, n] R) :
    n ^ 3 ⌈/⌉ (3 * n - 2) ≤ R ∧ R ≤ n * (n + 1) / 2

Category research solved; AMS 14 Algebraic geometry, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 344.

Arxiv.«0805.3777».isMaxRank_cube

Open: stated without proof.

Open problem. Determine the maximal rank of a complex \(n \times n \times n\) tensor. No formula is known: for \(n = 1, 2, 3\) the values are 1, 3 and 5, while for \(4 \leq n \leq 7\) only the bounds in isMaxRank_cube_bounds, such as \(7 \leq \operatorname{mrank}(4,4,4) \leq 10\), are available [BFZ24, (4.25)-(4.28)].

theorem isMaxRank_cube {n : ℕ} (hn : 1 ≤ n) :
    IsMaxRank [n, n, n] (isMaxRank_cube.answer n)

Category research open; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/0805.3777/TensorRank.lean, line 361.

Sources

• FormalConjectures/Arxiv/0805.3777/TensorRank.lean at 2055e5ad
• https://doi.org/10.1016/j.laa.2011.05.008

LeanArxiv.«0805.3777».isGenericRank_matrix · Arxiv.«0805.3777».isGenericRank_of_gt_critical · Arxiv.«0805.3777».isGenericRank_three_even · Arxiv.«0805.3777».isGenericRank_three_odd · Arxiv.«0805.3777».isGenericRank_four · Arxiv.«0805.3777».isGenericRank_cube · Arxiv.«0805.3777».isGenericRank_of_eq_critical · Arxiv.«0805.3777».isGenericRank_of_le_critical · Arxiv.«0805.3777».isMaxRank_two · Arxiv.«0805.3777».cprank_le_of_three_slices · Arxiv.«0805.3777».isMaxRank_three · Arxiv.«0805.3777».isMaxRank_of_le_min · Arxiv.«0805.3777».isMaxRank_three_three_five_bounds · Arxiv.«0805.3777».isMaxRank_three_three_five · Arxiv.«0805.3777».isMaxRank_le_two_mul_isGenericRank · Arxiv.«0805.3777».cprank_le_of_square_slices · Arxiv.«0805.3777».isMaxRank_cube_bounds · Arxiv.«0805.3777».isMaxRank_cube

TheoremCentral Binomial Tail Bounds, Conjecture 6.3#

Reference: arxiv/0911.2077 Central Binomial Tail Bounds by Matus Telgarsky

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

The file states 1 research or textbook statement: 1 solved.

Arxiv.«0911.2077».arxiv.id0911_2077.conjecture6_3

Solved: stated here; a Lean proof is at https://github.com/logical-intelligence/proofs/blob/0dbb9215f472c532ca8af1376ed58a7ebca6dec2/LI/Conj63.lean#L8845.

Empirical evidence seems to suggest that Slud's bound does not hold for all \(p\), and in fact, as \(n\to\infty\), the maximal permissible \(p\) shrinks to \(\frac{1}{2}\). Also, the following appears to be true:

When \(p\in(0,1/2)\) and \(m = 2k\) is even, and \(\sigma := \sqrt{p(1-p)}\),

\[ \mathbb{P}[B(p,m) \geq m/2] \geq 1 - \Phi\left(\frac{(1/2-p)\sqrt{m}}{\sigma}\right) + \frac 1 2\binom{m}{m/2}\sigma^{m}. \]

A solution of this statement has been put out by Logical Intelligence https://github.com/logical-intelligence/proofs, see here for and informal sketch of the proof.

theorem arxiv.id0911_2077.conjecture6_3
    (p : ℝ) (h_p : p ∈ Set.Ioo 0 (1 / 2)) (k : ℕ) (hk : 0 < k)
    (σ : ℝ) (h_σ : σ = (p * (1 - p)).sqrt) :
    letI hp' : (⟨p, le_of_lt h_p.1⟩ : ℝ≥0) ≤ 1 := by
      have : p ≤ 1 :=  le_trans (le_of_lt (Set.mem_Ioo.mp h_p).right) (by linarith)
      exact this
    1 - Φ ((1 / 2 - p) * sqrt (2 * k : ℝ≥0) / σ)
      + (1 / 2) * ((2 * k).choose k) * σ ^ (2 * k)
      ≤ (binomial (2 * k) ⟨p, h_p.1.le, hp'⟩).real (Set.Icc k (2 * k))

Category research solved; AMS 60 Probability theory and stochastic processes. Declared in FormalConjectures/Arxiv/0911.2077/Conjecture6_3.lean, line 52.

Sources

• FormalConjectures/Arxiv/0911.2077/Conjecture6_3.lean at 2055e5ad
• arxiv/0911.2077

LeanArxiv.«0911.2077».arxiv.id0911_2077.conjecture6_3

TheoremThe Curling Number Conjecture#

Reference: arxiv/0912.2382 The Curling Number Conjecture by Benjamin Chaffin and N. J. A. Sloane

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

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

Arxiv.«0912.2382».curling_number_conjecture

Open: stated without proof.

Starting from any nonempty finite integer sequence, repeatedly appending its curling number eventually gives a sequence with curling number \(1\) [Chaffin and Sloane, Conjecture 1].

theorem curling_number_conjecture (S₀ : List ℤ) (h : S₀ ≠ []) : ∃ m, k (S S₀ m) = 1

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/0912.2382/CurlingNumberConjecture.lean, line 130.

Sources

• FormalConjectures/Arxiv/0912.2382/CurlingNumberConjecture.lean at 2055e5ad
• arxiv/0912.2382

LeanArxiv.«0912.2382».curling_number_conjecture

TheoremThe first Atiyah--Sutcliffe conjecture#

Atiyah and Sutcliffe associate a homogeneous binary polynomial to each point in a configuration of distinct points in Euclidean three-space. Their first conjecture says that these polynomials are always linearly independent.

References: - M. F. Atiyah and P. M. Sutcliffe, The Geometry of Point Particles - Marcin Mazur and Bogdan V. Petrenko, On the conjectures of Atiyah and Sutcliffe

Quoted from FormalConjectures/Arxiv/1102.4662/AtiyahSutcliffe.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 6 test statements, counted here but not shown.

AtiyahSutcliffe.conjecture_one

Open: stated without proof.

Atiyah–Sutcliffe Conjecture 1, stated as Conjecture 1.1 in Mazur–Petrenko: the configuration polynomials are linearly independent.

theorem conjecture_one {n : ℕ} (x : Fin n → Point) (hx : Function.Injective x) :
    LinearIndependent ℂ (pointPolynomial x)

Category research open; AMS 51 Geometry, 70 Mechanics of particles and systems. Declared in FormalConjectures/Arxiv/1102.4662/AtiyahSutcliffe.lean, line 115.

Sources

• FormalConjectures/Arxiv/1102.4662/AtiyahSutcliffe.lean at 2055e5ad
• The Geometry of Point Particles

LeanAtiyahSutcliffe.conjecture_one

TheoremCunningham chains — Jones's conjecture#

A Cunningham chain is a sequence of primes satisfying either \(p_{i+1}=2p_i+1\) (first kind) or \(p_{i+1}=2p_i-1\) (second kind). It is conjectured that there are infinitely many chains of every positive exact length, of both kinds.

A chain has exact length k when its first \(k\) terms are prime and the \((k+1)\)-th generated term is composite.

Lenny Jones conjectures that for every positive integer \(k\), infinitely many primes start a chain of exact length \(k\), for each of the two kinds.

References: - Lenny Jones, Polynomial Cunningham Chains - OEIS A181697, first-kind chain lengths - OEIS A181715, second-kind chain lengths

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

The file states 2 research or textbook statements: 2 open. It also has 2 test statements, counted here but not shown.

CunninghamChain.infinitely_many_firstKind_chains

Open: stated without proof.

Jones's conjecture (first kind): for every positive integer \(k\), there are infinitely many primes \(p\) that start a first-kind Cunningham chain of exactly length \(k\).

theorem infinitely_many_firstKind_chains (k : ℕ) (hk : 0 < k) :
    Set.Infinite {p : ℕ | IsFirstKindChainOfLength p k}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/1104.1579/CunninghamChain.lean, line 83.

CunninghamChain.infinitely_many_secondKind_chains

Open: stated without proof.

Jones's conjecture (second kind): for every positive integer \(k\), there are infinitely many primes \(p\) that start a second-kind Cunningham chain of exactly length \(k\).

theorem infinitely_many_secondKind_chains (k : ℕ) (hk : 0 < k) :
    Set.Infinite {p : ℕ | IsSecondKindChainOfLength p k}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/1104.1579/CunninghamChain.lean, line 93.

Sources

• FormalConjectures/Arxiv/1104.1579/CunninghamChain.lean at 2055e5ad
• Polynomial Cunningham Chains

LeanCunninghamChain.infinitely_many_firstKind_chains · CunninghamChain.infinitely_many_secondKind_chains

TheoremConway's subprime Fibonacci sequences#

A subprime Fibonacci sequence starts from two positive integers. Each new term is the sum of the previous two terms if that sum is prime; if the sum is composite, it is divided once by its least prime factor. This file formalizes the no-infinite-chains component of the conjecture: every such sequence eventually enters a cycle. It does not assert that the seven known loops are complete or unique.

References: - R. K. Guy, T. Khovanova, and J. Salazar, "Conway's subprime Fibonacci sequences", Mathematics Magazine 87 (2014), no. 5, 323–337. - A214897, Conway's subprime Fibonacci sequence: cycle lengths.

Quoted from FormalConjectures/Arxiv/1207.5099/SubprimeFibonacci.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 10 test statements and 1 API statement, counted here but not shown.

Arxiv.«1207.5099».conjecture

Open: stated without proof.

Every subprime Fibonacci sequence starting from two positive integers eventually enters a cycle. This is the "no infinite chains" conjecture recorded in A214897, associated with Guy–Khovanova–Salazar.

theorem conjecture (x y : ℕ) (hx : 0 < x) (hy : 0 < y) : EventuallyPeriodic (x, y)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/1207.5099/SubprimeFibonacci.lean, line 110.

Sources

• FormalConjectures/Arxiv/1207.5099/SubprimeFibonacci.lean at 2055e5ad
• "Conway's subprime Fibonacci sequences"

LeanArxiv.«1207.5099».conjecture

TheoremBoxdot Conjecture#

The Boxdot Conjecture was originally formulated by French and Humberstone and has been studied in several works. In particular, see:

References: - arxiv/1308.0994 Cluster Expansion and the Boxdot Conjecture by Emil Jeřábek - The Boxdot Conjecture and the Generalized McKinsey Axiom by Christopher Steinsvold, Australasian Journal of Logic

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

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

Arxiv.«1308.0994».BoxdotConjecture

Solved: stated here; a Lean proof is at https://github.com/FormalizedFormalLogic/ModalLogic/blob/bdadfabed4167bc8b947cc368451ce83cd30a017/ModalLogicArchive/Modal/Boxdot/Jerabek.lean.

Boxdot Conjecture: every normal modal logic that faithfully interprets KT by the boxdot translation is included in KT.

theorem BoxdotConjecture (L : NormalModalLogic) (H : ∀ φ, L ⊢ ■ φ ↔ KT ⊢ φ) : L.thms ⊆ KT.thms

Category research solved; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/Arxiv/1308.0994/BoxdotConjecture.lean, line 238.

Sources

• FormalConjectures/Arxiv/1308.0994/BoxdotConjecture.lean at 2055e5ad
• arxiv/1308.0994

LeanArxiv.«1308.0994».BoxdotConjecture

TheoremUnique Crystal Components#

Reference: arxiv/1601.03081 The Biharmonic mean by Marco Abrate, Stefano Barbero, Umberto Cerruti, Nadir Murru

Quoted from FormalConjectures/Arxiv/1601.03081/UniqueCrystalComponents.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 and 6 API statements, counted here but not shown.

Arxiv.«1601.03081».crystals_components_unique

Open: stated without proof.

If \(n = ab\) is a crystal, then there are no other pairs of positive integers \(c, d > 1\), different from the couple \(a, b\), such that \(n = cd\) and \(B(c, d) ∈ ℕ\), i.e., the components of the crystals are unique.

theorem crystals_components_unique (n a b c d : ℕ)
    (hab : IsCrystalWithComponents n a b) (hcd : IsCrystalWithComponents n c d) :
    ({a, b} : Finset ℕ) = {c, d}

Category research open; AMS 11 Number theory, 26 Real functions. Declared in FormalConjectures/Arxiv/1601.03081/UniqueCrystalComponents.lean, line 122.

Sources

• FormalConjectures/Arxiv/1601.03081/UniqueCrystalComponents.lean at 2055e5ad
• arxiv/1601.03081

LeanArxiv.«1601.03081».crystals_components_unique

TheoremThe length of an \(s\)-increasing sequence of \(r\)-tuples#

This file contains the formalisation of [GoLo21] up to and including Conjecture 1.8.

References: - arxiv/1609.08688 The length of an \(s\)-increasing sequence of \(r\)-tuples by W. T. Gowers, J. Long - GoLo21 The length of an \(s\)-increasing sequence of \(r\)-tuples by W. T. Gowers, J. Long, Combinatorics, Probability and Computing (2021), 686-721

Quoted from FormalConjectures/Arxiv/1609.08688/sIncreasingrTuples.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 9 test statements and 11 API statements, counted here but not shown.

Arxiv.«1609.08688».maximalLength_le

Proved here.

For all \(n\) we have \(F(n) \leq n^2\).

This is the upper bound in [GoLo21, Proposition 1.4], proved by applying the pigeonhole principle to the first two coordinates.

theorem maximalLength_le (n : ℕ) : F n ≤ n ^ 2

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/1609.08688/sIncreasingrTuples.lean, line 190.

Arxiv.«1609.08688».maximalLength_ge_of_isSquare

Solved: stated here without proof.

Moreover, whenever \(n\) is a perfect square we have \(F(n) \geq n^{3/2}\).

theorem maximalLength_ge_of_isSquare {n : ℕ} (h : IsSquare n) :
    n.sqrt ^ 3 ≤ F n

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/1609.08688/sIncreasingrTuples.lean, line 217.

Arxiv.«1609.08688».maximalLength_le_isBigO

Solved: stated here without proof.

\(F(n) \leq n^2 / \exp(\Omega(\log^*(n)))\), i.e. there is a constant \(c > 0\) such that \(F(n) \leq n^2 / \exp(c \log^*(n))\) for all sufficiently large \(n\).

theorem maximalLength_le_isBigO : ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
    (F n : ℝ) ≤ (n : ℝ) ^ 2 / Real.exp (c * (Real.iteratedLog n : ℝ))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/1609.08688/sIncreasingrTuples.lean, line 234.

Arxiv.«1609.08688».maximalLength_pow

Solved: stated here without proof.

Suppose that for some \(n\) we have \(F(n) = n ^ {\alpha}\). Then there are arbitrarily large \(m\) such that \(F(m) \geq m^{\alpha}\).

theorem maximalLength_pow {n : ℕ} {e : ℝ} (hn : 1 < n) (h : F n = (n : ℝ) ^ e) :
    ∃ᶠ m : ℕ in Filter.atTop, (m : ℝ) ^ e ≤ F m

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/1609.08688/sIncreasingrTuples.lean, line 279.

Arxiv.«1609.08688».maximalLength_pow_eventually

Solved: stated here without proof.

Moreover, for every \(\beta < \alpha\) and all sufficiently large \(m\) we have \(F(m) \geq m^{\beta}\).

theorem maximalLength_pow_eventually {n : ℕ} {e : ℝ} (hn : 1 < n) (h : F n = (n : ℝ) ^ e)
    {b : ℝ} (hb : b < e) :
    ∀ᶠ m : ℕ in Filter.atTop, (m : ℝ) ^ b ≤ F m

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/1609.08688/sIncreasingrTuples.lean, line 286.

Arxiv.«1609.08688».maximalLength_le_strong

Open: stated without proof.

\(F(n) \leq n^{3/2}\).

theorem maximalLength_le_strong (n : ℕ) : F n ≤ Real.sqrt n ^ 3

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/1609.08688/sIncreasingrTuples.lean, line 293.

Sources

• FormalConjectures/Arxiv/1609.08688/sIncreasingrTuples.lean at 2055e5ad
• arxiv/1609.08688

LeanArxiv.«1609.08688».maximalLength_le · Arxiv.«1609.08688».maximalLength_ge_of_isSquare · Arxiv.«1609.08688».maximalLength_le_isBigO · Arxiv.«1609.08688».maximalLength_pow · Arxiv.«1609.08688».maximalLength_pow_eventually · Arxiv.«1609.08688».maximalLength_le_strong

TheoremRingel's Conjecture and Kotzig's Conjecture for large \(n\)#

Reference: arxiv/2001.02665 A proof of Ringel's Conjecture by Richard Montgomery, Alexey Pokrovskiy, Benny Sudakov

The original conjecture of Ringel (1963), which remains open, is stated in Paper/RingelConjecture.lean. The referenced paper proves it for all sufficiently large \(n\).

Montgomery–Pokrovskiy–Sudakov actually prove the strictly stronger statement conjectured by Kotzig: the decomposition can always be realized by cyclic shifts of a single copy of \(T\). Kotzig's conjecture (all \(n\)) remains open; see Paper/KotzigConjecture.lean.

Quoted from FormalConjectures/Arxiv/2001.02665/RingelConjecture.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.

Arxiv.«2001.02665».ringel_conjecture_large

Solved: stated here without proof.

For all sufficiently large \(n\), the complete graph \(K_{2n+1}\) decomposes into \(2n+1\) edge-disjoint copies of any tree \(T\) with \(n\) edges.

A "copy" of \(T\) is the image \(T.\text{map}(f_i)\) of \(T\) under a vertex embedding \(f_i : V \hookrightarrow \text{Fin}(2n+1)\); the copies are pairwise edge-disjoint and together cover every edge of \(K_{2n+1}\).

This follows from kotzig_conjecture_large; see Paper/RingelConjecture.lean for the open form.

theorem ringel_conjecture_large :
    ∀ᶠ (n : ℕ) in Filter.atTop, ∀ {V : Type} [Finite V] (T : SimpleGraph V),
      T.IsTree → T.edgeSet.ncard = n →
      ∃ f : Fin (2 * n + 1) → (V ↪ Fin (2 * n + 1)),
        Pairwise (fun i j => Disjoint (T.map (f i)).edgeSet (T.map (f j)).edgeSet) ∧
        ⨆ i, T.map (f i) = (⊤ : SimpleGraph (Fin (2 * n + 1)))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2001.02665/RingelConjecture.lean, line 51.

Arxiv.«2001.02665».kotzig_conjecture_large

Solved: stated here without proof.

For all sufficiently large \(n\), the complete graph \(K_{2n+1}\) decomposes into \(2n+1\) edge-disjoint copies of any tree \(T\) with \(n\) edges via cyclic shifts of a single embedding.

The \(2n+1\) copies are \(f_0, f_1, \dots, f_{2n}\) where \(f_i(v) = f_0(v) + i\) for all vertices \(v\) — that is, each copy is obtained by adding \(i \pmod{2n+1}\) to every vertex of the base copy. This is strictly stronger than ringel_conjecture_large.

Kotzig conjectured this holds for all \(n\); see Paper/KotzigConjecture.lean. Montgomery, Pokrovskiy, and Sudakov prove it for all sufficiently large \(n\).

theorem kotzig_conjecture_large :
    ∀ᶠ (n : ℕ) in Filter.atTop, ∀ {V : Type} [Finite V] (T : SimpleGraph V),
      T.IsTree → T.edgeSet.ncard = n →
      ∃ f : Fin (2 * n + 1) → (V ↪ Fin (2 * n + 1)),
        (∀ i v, f i v = f 0 v + i) ∧
        Pairwise (fun i j => Disjoint (T.map (f i)).edgeSet (T.map (f j)).edgeSet) ∧
        ⨆ i, T.map (f i) = (⊤ : SimpleGraph (Fin (2 * n + 1)))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2001.02665/RingelConjecture.lean, line 72.

Sources

• FormalConjectures/Arxiv/2001.02665/RingelConjecture.lean at 2055e5ad
• arxiv/2001.02665

LeanArxiv.«2001.02665».ringel_conjecture_large · Arxiv.«2001.02665».kotzig_conjecture_large

TheoremBarker sequences#

A Barker sequence is a finite sequence of \(\pm 1\) values whose nontrivial aperiodic autocorrelations all have magnitude at most one. The Barker conjecture says that no such sequence has length greater than \(13\).

References: * J. Willms, A note on Barker sequences of even length * Barker code * OEIS A091704

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

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

Arxiv.«2104.00502».barker_conjecture

Open: stated without proof.

Every Barker sequence has length at most \(13\).

theorem barker_conjecture (a : List ℤ) (ha : IsBarkerSequence a) : a.length ≤ 13

Category research open; AMS 05 Combinatorics, 11 Number theory, 94 Information and communication, circuits. Declared in FormalConjectures/Arxiv/2104.00502/BarkerSequence.lean, line 50.

Sources

• FormalConjectures/Arxiv/2104.00502/BarkerSequence.lean at 2055e5ad
• A note on Barker sequences of even length

LeanArxiv.«2104.00502».barker_conjecture

TheoremIndependent Domination of Regular Graphs, Conjecture 1.6#

Reference: arxiv/2107.00295 On independent domination of regular graphs by Eun-Kyung Cho, Ilkyoo Choi, Boram Park

The conjecture was subsequently proved by Cho, Kim, Kim and Oum, as Corollary 1.3 of:

Reference: arxiv/2202.09594 Independent domination of graphs with bounded maximum degree by Eun-Kyung Cho, Jinha Kim, Minki Kim, Sang-il Oum, J. Combin. Theory Ser. B 158 (2023), 341-352.

Corollary 1.3 states that every graph \(G\) with maximum degree at most \(\Delta\) and no isolated vertices has an independent dominating set of size at most \(\left(1 - \frac{\Delta}{\lfloor (\Delta+2)^2/4 \rfloor}\right)\lvert V(G)\rvert\). Expanding the floor for even and odd \(\Delta\) gives exactly the two statements below.

Quoted from FormalConjectures/Arxiv/2107.00295/IndependentDomination.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.

Arxiv.«2107.00295».independentDominationEven

Solved: stated here without proof.

Conjecture 1.6 (Even case). For a nonempty isolate-free graph \(G\) on \(n\) vertices, if \(D\) is even, then \((D + 2)^2 \cdot i(G) \leq (D^2 + 4) \cdot n\).

Proved by Cho, Kim, Kim and Oum (arxiv/2202.09594, Corollary 1.3).

theorem independentDominationEven (hIso : 0 < G.minDegree) (hEven : Even G.maxDegree) :
    let D := G.maxDegree
    let i := G.indepDominationNumber
    let n := Fintype.card V
    (D + 2)^2 * i ≤ (D^2 + 4) * n

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2107.00295/IndependentDomination.lean, line 55.

Arxiv.«2107.00295».independentDominationOdd

Solved: stated here without proof.

Conjecture 1.6 (Odd case). For a nonempty isolate-free graph \(G\) on \(n\) vertices, if \(D\) is odd, then \((D + 1)(D + 3) \cdot i(G) \leq (D^2 + 3) \cdot n\).

Proved by Cho, Kim, Kim and Oum (arxiv/2202.09594, Corollary 1.3).

theorem independentDominationOdd (hIso : 0 < G.minDegree) (hOdd : Odd G.maxDegree) :
    let D := G.maxDegree
    let i := G.indepDominationNumber
    let n := Fintype.card V
    (D + 1) * (D + 3) * i ≤ (D^2 + 3) * n

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2107.00295/IndependentDomination.lean, line 71.

Sources

• FormalConjectures/Arxiv/2107.00295/IndependentDomination.lean at 2055e5ad
• arxiv/2107.00295

LeanArxiv.«2107.00295».independentDominationEven · Arxiv.«2107.00295».independentDominationOdd

TheoremDigit \(2\) in base \(3\) representation of \(2^n\)#

References: - Some Unconventional Problems in Number Theory by Paul Erdös, Mathematics Magazine 52, no. 2, p. 67, 1979 - arxiv/2107.12475 Hardness of busy beaver value BB(15) by Tristan Stérin, Damien Woods - Hardness of Busy Beaver Value BB(15) by Tristan Stérin, Damien Woods, Reachability Problems, Lecture Notes in Computer Science 15050, Springer, Cham (2024)

Quoted from FormalConjectures/Arxiv/2107.12475/CollatzLike.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.

Arxiv.«2107.12475».CollatzLike

Open: stated without proof.

For \(n > 8\), \(2^n\) is not the sum of distinct powers of \(3\). Expressed here in terms of the base \(3\) digits of \(2^n\).

This conjecture is equivalent to the non-halting of a \(15\)-state \(2\)-symbol Turing Machine. The Turing Machine version is formalized in cryptids: ConjectureMachines.ErdosTernary15.halts_erdosTernary15_iff_exists_counterexample proves that this machine halts on the blank tape if and only if some \(2^n\) with \(n > 8\) has no digit \(2\) in base \(3\). The repository also proves this for Tristan Stérin's \(14\)-state machine.

Source: Hardness of Busy Beaver Value BB(15): https://link.springer.com/chapter/10.1007/978-3-031-72621-7_9 This is also https://arxiv.org/abs/2107.12475.

theorem CollatzLike (n : ℕ) (hn : 8 < n) : 2 ∈ Nat.digits 3 (2^n)

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/Arxiv/2107.12475/CollatzLike.lean, line 51.

Sources

• FormalConjectures/Arxiv/2107.12475/CollatzLike.lean at 2055e5ad
• Some Unconventional Problems in Number Theory

LeanArxiv.«2107.12475».CollatzLike

TheoremZariski Cancellation#

References: - arxiv/2208.14736 The Zariski Cancellation Problem and related problems in Affine Algebraic Geometry by Neena Gupta - [OAI26a] OpenAI, An explicit failure of complex affine-space cancellation. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-explicit-failure-of-complex-affine-space-cancellation-September-23-2026/paper.pdf

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

The file states 5 research or textbook statements: 5 solved.

Arxiv.«2208.14736».zariski_cancellation_problem

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

The Zariski Cancellation Problem: is every polynomial ring over a field k of characteristic 0 cancellative?

The answer is no: the polynomial ring in four variables over \(\mathbb{C}\) is not cancellative. This was disproved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof and zariski_cancellation_problem.variants.false_complex_four.

theorem zariski_cancellation_problem :
    ¬ ∀ {k : Type} [Field k] [CharZero k] {ι : Type} [Fintype ι],
      IsCancellative k (MvPolynomial ι k)

Category research solved; AMS 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Arxiv/2208.14736/ZariskiCancellation.lean, line 58.

Arxiv.«2208.14736».zariski_cancellation_problem.variants.false_complex_four

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

The polynomial ring in four variables over \(\mathbb{C}\) is not cancellative: there is a finitely generated \(\mathbb{C}\)-domain \(A\) of Krull dimension \(4\) with \(A[w] \cong \mathbb{C}[x_1, \dots, x_5]\) but \(A \not\cong \mathbb{C}[x_1, \dots, x_4]\). This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.

theorem zariski_cancellation_problem.variants.false_complex_four :
    ¬ IsCancellative ℂ (MvPolynomial (Fin 4) ℂ)

Category research solved; AMS 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Arxiv/2208.14736/ZariskiCancellation.lean, line 72.

Arxiv.«2208.14736».zariski_cancellation_problem.variants.dim_one

Solved: stated here without proof.

The single variable polynomial ring k[X] is cancellative in any characteristic

theorem zariski_cancellation_problem.variants.dim_one
    {k : Type*} [Field k] : IsCancellative k k[X]

Category research solved; AMS 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Arxiv/2208.14736/ZariskiCancellation.lean, line 80.

Arxiv.«2208.14736».zariski_cancellation_problem.variants.dim_two

Solved: stated here without proof.

The two variable polynomial ring k[X] is cancellative in any characteristic

theorem zariski_cancellation_problem.variants.dim_two {k : Type*} [Field k] :
    IsCancellative k (MvPolynomial (Fin 2) k)

Category research solved; AMS 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Arxiv/2208.14736/ZariskiCancellation.lean, line 88.

Arxiv.«2208.14736».zariski_cancellation_problem.variants.false_pos_card

Solved: stated here without proof.

The positive characteristic case of the Zariski Cancellation Problem is false in dimension 3

theorem zariski_cancellation_problem.variants.false_pos_card
    (p : ℕ) [hp : Fact p.Prime] {ι : Type*} [Fintype ι] (hι : Fintype.card ι = 3) :
    ¬ IsCancellative (ZMod p) (MvPolynomial ι (ZMod p))

Category research solved; AMS 13 Commutative algebra, 14 Algebraic geometry. Declared in FormalConjectures/Arxiv/2208.14736/ZariskiCancellation.lean, line 96.

Sources

• FormalConjectures/Arxiv/2208.14736/ZariskiCancellation.lean at 2055e5ad
• arxiv/2208.14736

LeanArxiv.«2208.14736».zariski_cancellation_problem · Arxiv.«2208.14736».zariski_cancellation_problem.variants.false_complex_four · Arxiv.«2208.14736».zariski_cancellation_problem.variants.dim_one · Arxiv.«2208.14736».zariski_cancellation_problem.variants.dim_two · Arxiv.«2208.14736».zariski_cancellation_problem.variants.false_pos_card

TheoremSpectral sets and weak tiling#

This file formalizes Problems 7.1 and 7.2 from Kolountzakis, Lev, and Matolcsi.

References: - [KLM2023] Mihail N. Kolountzakis, Nir Lev, and Máté Matolcsi, Spectral sets and weak tiling. - [GL16] Rachel Greenfeld and Nir Lev, Spectrality and tiling by cylindric domains, Journal of Functional Analysis 271 (2016), 2808–2821. - [GL20] Rachel Greenfeld and Nir Lev, Spectrality of product domains and Fuglede's conjecture for convex polytopes, Journal d'Analyse Mathématique 140 (2020), 409–441. - [Ki26] Kenta Kitamura, A Lean proof of Problem 7.2 of Kolountzakis–Lev–Matolcsi in dimension three, GitHub repository (2026).

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

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

NowhereDenseSpectralSet.exists_nowhereDense_spectralSet

Open: stated without proof.

[KLM2023, Problem 7.1] asks whether a bounded, measurable, nowhere dense subset \(\Omega \subset \mathbb{R}^d\) of positive measure can be spectral. The answer is known to be negative for \(d = 1\), so the dimension is restricted to \(d \ge 2\), where the problem is open.

theorem exists_nowhereDense_spectralSet :
    ∃ d : ℕ, 2 ≤ d ∧
      ∃ Ω : Set (Fin d → ℝ), Bornology.IsBounded Ω ∧ MeasurableSet Ω ∧
        IsNowhereDense Ω ∧ 0 < volume Ω ∧ isSpectral Ω

Category research open; AMS 42 Harmonic analysis on Euclidean spaces, 46 Functional analysis. Declared in FormalConjectures/Arxiv/2209.04540/SpectralSetsAndWeakTiling.lean, line 48.

SpectralSetProduct.isSpectral_right_of_product_one_dimensional

Solved: stated here without proof.

[KLM2023, Problem 7.2; GL16] For a one-dimensional convex body \(A\) and a bounded, measurable set \(B\), if \(A \times B\) is spectral, then \(B\) is spectral.

theorem isSpectral_right_of_product_one_dimensional :
    ∀ (m : ℕ), 0 < m → spectralProductImpliesRightSpectral 1 m

Category research solved; AMS 42 Harmonic analysis on Euclidean spaces, 46 Functional analysis. Declared in FormalConjectures/Arxiv/2209.04540/SpectralSetsAndWeakTiling.lean, line 79.

SpectralSetProduct.isSpectral_right_of_product_two_dimensional

Solved: stated here without proof.

[KLM2023, Problem 7.2; GL20] For a two-dimensional convex body \(A\) and a bounded, measurable set \(B\), if \(A \times B\) is spectral, then \(B\) is spectral.

theorem isSpectral_right_of_product_two_dimensional :
    ∀ (m : ℕ), 0 < m → spectralProductImpliesRightSpectral 2 m

Category research solved; AMS 42 Harmonic analysis on Euclidean spaces, 46 Functional analysis. Declared in FormalConjectures/Arxiv/2209.04540/SpectralSetsAndWeakTiling.lean, line 88.

SpectralSetProduct.isSpectral_right_of_product_three_dimensional

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/klm-7-2-spectral-product-3d/blob/2874890904e117df17d8abf1dd27254eebfb2829/lean/SpectralProduct3DFC.lean#L20962-L20966.

[KLM2023, Problem 7.2] For a three-dimensional convex body \(A\) and a bounded, measurable set \(B\), must spectrality of \(A \times B\) imply spectrality of \(B\)?

The answer is yes. For the Lean proof, see [Ki26].

theorem isSpectral_right_of_product_three_dimensional :
    ∀ (m : ℕ), 0 < m → spectralProductImpliesRightSpectral 3 m

Category research solved; AMS 42 Harmonic analysis on Euclidean spaces, 46 Functional analysis. Declared in FormalConjectures/Arxiv/2209.04540/SpectralSetsAndWeakTiling.lean, line 102.

SpectralSetProduct.isSpectral_right_of_product_of_convexBody

Open: stated without proof.

[KLM2023, Problem 7.2] For every positive dimension \(n\), a convex body \(A\) and a bounded, measurable set \(B\), must spectrality of \(A \times B\) imply spectrality of \(B\)?

theorem isSpectral_right_of_product_of_convexBody :
    ∀ (n m : ℕ), 0 < n → 0 < m →
      spectralProductImpliesRightSpectral n m

Category research open; AMS 42 Harmonic analysis on Euclidean spaces, 46 Functional analysis. Declared in FormalConjectures/Arxiv/2209.04540/SpectralSetsAndWeakTiling.lean, line 111.

Sources

• FormalConjectures/Arxiv/2209.04540/SpectralSetsAndWeakTiling.lean at 2055e5ad
• Spectral sets and weak tiling

LeanNowhereDenseSpectralSet.exists_nowhereDense_spectralSet · SpectralSetProduct.isSpectral_right_of_product_one_dimensional · SpectralSetProduct.isSpectral_right_of_product_two_dimensional · SpectralSetProduct.isSpectral_right_of_product_three_dimensional · SpectralSetProduct.isSpectral_right_of_product_of_convexBody

TheoremFurstenberg's `times p, times q` conjectures#

Reference: arxiv/2303.01089 Around Furstenberg's times \(p\), times \(q\) conjecture: times \(p\)-invariant measures with some large Fourier coefficients by Catalin Badea, Sophie Grivaux

Quoted from FormalConjectures/Arxiv/2303.01089/FurstenbergTimesPTimesQ.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 API statement, counted here but not shown.

Arxiv.id2303_01089.conjecture_1_3

Open: stated without proof.

Conjecture 1.3 (the \(\times p, \times q\) conjecture): the only atomless Borel probability measure on \(\mathbb{T}\) which is both \(T_p\)- and \(T_q\)-invariant is the Lebesgue measure.

theorem conjecture_1_3 {p q : ℕ} (hp : 2 <= p) (hq : 2 <= q) (hpq : MultiplicativelyIndependent p q)
    {μ : Measure 𝕋} [IsProbabilityMeasure μ] [MeasureTheory.IsAtomLess μ]
    (hmup : MeasurePreserving (Tn p) μ μ)
    (hmuq : MeasurePreserving (Tn q) μ μ) :
    μ = volume

Category research open; AMS 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Arxiv/2303.01089/FurstenbergTimesPTimesQ.lean, line 75.

Arxiv.id2303_01089.conjecture_1_4

Solved: stated here without proof.

Conjecture 1.4: if \(\mu\) is an atomless \(T_p\)-invariant Borel probability measure on \(\mathbb{T}\), then \(T_{q^n}\mu\) converges weak-star to Lebesgue measure. This paper disproves the conjecture.

theorem conjecture_1_4 :
    ¬ ∀ p q : ℕ, 2 <= p → 2 <= q → MultiplicativelyIndependent p q →
      ∀ μ : ProbabilityMeasure 𝕋,
        MeasureTheory.IsAtomLess μ.1 → MeasurePreserving (Tn p) μ μ →
        Tendsto (fun n : ℕ => μ.map (Tn_continuous (q ^ n)).aemeasurable) atTop
          (𝓝 UnitAddCircle.ProbabilityMeasure)

Category research solved; AMS 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Arxiv/2303.01089/FurstenbergTimesPTimesQ.lean, line 88.

Sources

• FormalConjectures/Arxiv/2303.01089/FurstenbergTimesPTimesQ.lean at 2055e5ad
• arxiv/2303.01089

LeanArxiv.id2303_01089.conjecture_1_3 · Arxiv.id2303_01089.conjecture_1_4

TheoremThe circulant Hadamard conjecture#

A circulant matrix is generated by cyclically shifting one row. The circulant Hadamard conjecture, also attributed to Ryser, says that no circulant Hadamard matrix has order greater than \(4\).

References: * S. Steinerberger, A note on approximate Hadamard matrices * [OAI26a] OpenAI, The circulant Hadamard conjecture. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-circulant-Hadamard-conjecture-September-23-2026/paper.pdf

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

The file states 1 research or textbook statement: 1 solved. It also has 1 test statement, counted here but not shown.

CirculantHadamard.circulant_hadamard_conjecture

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/LinearAlgebra/CirculantHadamard/Main.lean#L21.

Every circulant Hadamard matrix has order at most four.

This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof, which shows that a real circulant Hadamard matrix of positive order \(n\) exists exactly when \(n = 1\) or \(n = 4\).

theorem circulant_hadamard_conjecture {n : ℕ} (v : Fin n → ℝ)
    (hv : Hadamard.IsHadamard' (Matrix.circulant v)) : n ≤ 4

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/Arxiv/2402.13202/CirculantHadamard.lean, line 65.

Sources

• FormalConjectures/Arxiv/2402.13202/CirculantHadamard.lean at 2055e5ad
• A note on approximate Hadamard matrices

LeanCirculantHadamard.circulant_hadamard_conjecture

TheoremAn Arithmetic Sum Associated with the Classical Theta Function#

Reference: arxiv/2501.03234 An Arithmetic Sum Associated with the Classical Theta Function by Bruce C. Berndt, Raghavendra N. Bhat, Jeffrey L. Meyer, Likun Xie, Alexandru Zaharescu

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

The file states 5 research or textbook statements: 5 open. It also has 5 test statements, counted here but not shown.

Arxiv.«2501.03234».conjecture_1_1

Open: stated without proof.

Conjecture 1.1: For any odd prime \(k\), the sum associated with the classical theta function \(θ_3\), \(S(k)\) is positive.

theorem conjecture_1_1 (k : ℕ) (hprim : k.Prime) (hodd : Odd k) : 0 < S k

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2501.03234/ArithmeticSumS.lean, line 65.

Arxiv.«2501.03234».conjecture_4_1

Open: stated without proof.

Conjecture 4.1: For any prime \(k\) larger than \(5\), \(S(k) > k\).

theorem conjecture_4_1 (k : ℕ) (hprim : k.Prime) (hodd : Odd k) (hgt : k > 5) : k < S k

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2501.03234/ArithmeticSumS.lean, line 72.

Arxiv.«2501.03234».conjecture_4_2

Open: stated without proof.

Conjecture 4.2: For any prime \(k\) larger than \(233\), \(S(k) > 2k\).

theorem conjecture_4_2 (k : ℕ) (hprim : k.Prime) (hodd : Odd k) (hgt : k > 233) : 2 * k < S k

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2501.03234/ArithmeticSumS.lean, line 79.

Arxiv.«2501.03234».conjecture_4_3

Open: stated without proof.

Conjecture 4.3: For any prime \(k\) larger than \(3119\), \(S(k) > 3k\).

theorem conjecture_4_3 (k : ℕ) (hprim : k.Prime) (hodd : Odd k) (hgt : k > 3119) : 3 * k < S k

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2501.03234/ArithmeticSumS.lean, line 86.

Arxiv.«2501.03234».conjecture_4_4

Open: stated without proof.

Conjecture 4.4: Given a natural number \(n ∈ ℕ\), for all large enough odd prime \(k\) (depending on \(n\)), \(nk < S(k)\).

theorem conjecture_4_4 (n : ℕ) : ∀ᶠ (k : ℕ) in Filter.atTop, k.Prime → Odd k → n * k < S k

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Arxiv/2501.03234/ArithmeticSumS.lean, line 94.

Sources

• FormalConjectures/Arxiv/2501.03234/ArithmeticSumS.lean at 2055e5ad
• arxiv/2501.03234

LeanArxiv.«2501.03234».conjecture_1_1 · Arxiv.«2501.03234».conjecture_4_1 · Arxiv.«2501.03234».conjecture_4_2 · Arxiv.«2501.03234».conjecture_4_3 · Arxiv.«2501.03234».conjecture_4_4

TheoremA conjecture by Margulis on matrix groups#

Reference: arxiv/2504.17644v3 Bounded diagonal orbits in homogeneous spaces over function fields by Qianlin Huang, Ronggang Shi

Quoted from FormalConjectures/Arxiv/2504.17644/Margulis.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.

Margulis.conjecture_1_1

Open: stated without proof.

Let D be the diagonal group of SL_n(ℝ) where n ≥ 3. Then any relatively compact D-orbit in SL_n(ℝ) / SL_n(ℤ) is closed.

theorem conjecture_1_1 {n : ℕ} (hn : 3 ≤ n)
    (g : SL(n, ℝ) ⧸ Subgroup.map (map (Int.castRingHom ℝ)) ⊤)
    (hg : IsCompact <| closure (MulAction.orbit (diagonalSubgroup (Fin n) ℝ) g)) :
    IsClosed <| MulAction.orbit (diagonalSubgroup (Fin n) ℝ) g

Category research open; AMS 11 Number theory, 15 Linear and multilinear algebra; matrix theory, 22 Topological groups, Lie groups. Declared in FormalConjectures/Arxiv/2504.17644/Margulis.lean, line 42.

Margulis.huang_shi_theorem_1_2

Solved: stated here without proof.

Huang–Shi, Theorem 1.2

Let F be a finite field of characteristic p ∈ {3, 5, 7, 11}, and set K = F((t⁻¹)), A = F[t]. Here K is modelled by the Laurent series field F⸨X⸩ with X = t⁻¹, so that A is embedded via t ↦ X⁻¹. Let

• D be the diagonal subgroup of SL₄(K),
• Γ = SL₄(A) the lattice subgroup embedded into SL₄(K) via the natural inclusion A →+* K.

Then there exists z : SL₄(K)/Γ such that the D-orbit of z has compact closure but is not closed.

theorem huang_shi_theorem_1_2
    (hchar : ringChar F ∈ ({3, 5, 7, 11} : Finset ℕ)) :
    ∃ z : SL(4, F⸨X⸩) ⧸ (  Matrix.SpecialLinearGroup.map
    (polyToLaurent F)).range,
      IsCompact (closure (MulAction.orbit (diagonalSubgroup (Fin 4) (F⸨X⸩)) z)) ∧
      ¬ IsClosed (MulAction.orbit (diagonalSubgroup (Fin 4) (F⸨X⸩)) z)

Category research solved; AMS 11 Number theory, 15 Linear and multilinear algebra; matrix theory, 22 Topological groups, Lie groups. Declared in FormalConjectures/Arxiv/2504.17644/Margulis.lean, line 97.

Sources

• FormalConjectures/Arxiv/2504.17644/Margulis.lean at 2055e5ad
• arxiv/2504.17644v3

LeanMargulis.conjecture_1_1 · Margulis.huang_shi_theorem_1_2

TheoremTxGraffiti Conjecture 1: independence, annihilation, and residue#

Reference: arxiv/2507.17780 In Reverie Together: Ten Years of Mathematical Discovery with a Machine Collaborator by Randy Davila, Boris Brimkov, Ryan Pepper

Conjecture 1, the oldest of the four TxGraffiti conjectures in the cited collection (open since 2016), asserts that every nontrivial connected graph \(G\) with maximum degree \(\Delta \ge 2\) satisfies

\[\alpha(G) \ge \frac{a(G) + R(G)}{\Delta(G)},\]

where \(\alpha\) is the independence number, \(a\) the annihilation number, \(R\) the Havel–Hakimi residue, and \(\Delta\) the maximum degree.

This conjecture is true, proved in arXiv:2606.29553 (C. Gupta).

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

The file states 1 research or textbook statement: 1 solved.

Arxiv.«2507.17780».tx_graffiti_conjecture_1

Solved: stated here without proof.

TxGraffiti Conjecture 1: for every nontrivial connected graph \(G\) with \(\Delta(G) \ge 2\),

\[\alpha(G) \ge \frac{a(G) + R(G)}{\Delta(G)}.\]

This conjecture is true.

Proof sketch. Substitute the Caro–Wei lower bound \(\alpha \ge W\) for \(\alpha\) and reduce to \(a \le (\Delta - 1) \alpha\). The case \(\Delta = 2\) is trivial (\(a = \alpha\)). For \(\Delta \ge 4\) an AM–HM argument with \(m \le (n - a)\Delta\) yields a quadratic whose discriminant is negative. For \(\Delta = 3\) the annihilation number has a closed form in the degree counts \((n_1, n_2, n_3)\) and \(a \le 2W\) is verified in three regimes. See arXiv:2606.29553.

theorem tx_graffiti_conjecture_1 (V : Type) [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (_hConn : G.Connected)
    (_hDeg : 2 ≤ G.maxDegree) :
    (G.annihilationNumber + residue G : ℝ) / G.maxDegree ≤ G.indepNum

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Arxiv/2507.17780/1.lean, line 60.

Sources

• FormalConjectures/Arxiv/2507.17780/1.lean at 2055e5ad
• arxiv/2507.17780

LeanArxiv.«2507.17780».tx_graffiti_conjecture_1

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.