Other

The 10 problem files in FormalConjectures/Other that state a research or textbook statement, at commit 2055e5ad, one article each.

Their docstrings and Lean statements are quoted from Formal Conjectures (Google DeepMind) at that commit, under its Apache-2.0 license.

TheoremBeaver Math Olympiad (BMO)#

The Beaver Math Olympiad (BMO) is a set of mathematical reformulations of the halting/nonhalting problem of specific Turing machines from all-0 tape. These problems came from studying small Busy Beaver values. Some problems are open and have a conjectured answer, some are open and don't have a conjectured answer, and, some are solved.

Among these problems is the Collatz-like Antihydra problem which is open and coming from a 6-state Turing machine, and a testament to the difficulty of knowing the sixth Busy Beaver value.

For some BMO problem, the equivalence between the mathematical formulation and the corresponding Turing machine non-termination has been formally proved in Rocq, we indicate it when done.

References:

Quoted from FormalConjectures/Other/BeaverMathOlympiad.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: 5 open and 2 solved.

BeaverMathOlympiad.beaver_math_olympiad_problem_1

Open: stated without proof.

BMO#1

Let \((a_n)_{n \ge 1}\) and \((b_n)_{n \ge 1}\) be two sequences such that \((a_1, b_1) = (1, 2)\) and

\[(a_{n+1}, b_{n+1}) = \begin{cases} (a_n-b_n, 4b_n+2) & \text{if }a_n \ge b_n \cr (2a_n+1, b_n-a_n) & \text{if }a_n < b_n \end{cases}\]

for all positive integers \(n\). Does there exist a positive integer \(i\) such that \(a_i = b_i\)?

The first 10 values of \((a_n, b_n)\) are \((1, 2), (3, 1), (2, 6), (5, 4), (1, 18), (3, 17), (7, 14), (15, 7), (8, 30), (17, 22)\).

BMO#1 is equivalent to asking whether the 6-state Turing machine 1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE halts or not.

There is presently no consensus on whether the machine halts or not, hence the problem is tagged as a question.

The machine was discovered by bbchallenge.org contributor Jason Yuen on June 25th 2024.

theorem beaver_math_olympiad_problem_1 :
    ∀ᵉ (a : ℕ → ℕ) (b : ℕ → ℕ)
    (a_ini : a 0 = 1)
    (a_rec : ∀ n, a (n + 1) = if b n ≤ a n then a n - b n else 2 * a n + 1)
    (b_ini : b 0 = 2)
    (b_rec : ∀ n, b (n + 1) = if b n ≤ a n then 4 * b n + 2 else b n - a n),
    ∃ i, a i = b i

Category research open; AMS 05 Combinatorics, 11 Number theory, 68 Computer science. Declared in FormalConjectures/Other/BeaverMathOlympiad.lean, line 71.

BeaverMathOlympiad.beaver_math_olympiad_problem_2_antihydra

Open: stated without proof.

BMO#2

Antihydra is a sequence starting at 8, and iterating the function

\[H(n) = \left\lfloor \frac {3n}2 \right\rfloor.\]

The conjecture states that the cumulative number of odd values in this sequence is never more than twice the cumulative number of even values. It is a relatively new open problem with, so it might be solvable, although seems quite hard because of its Collatz-like flavor. The underlying Collatz-like map has been studied independently in the past, see doi:10.1017/S0017089508004655 (Corollary 4).

It is equivalent to non-termination of the 1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA 6-state Turing machine (from all-0 tape). Note that the conjecture that the machine does not halt is based on a probabilistic argument.

This machine and its mathematical reformulations were found by bbchallenge.org contributors mxdys and Rachel Hunter on June 28th 2024.

theorem beaver_math_olympiad_problem_2_antihydra
    (a : ℕ → ℕ) (b : ℕ → ℤ)
    (a_ini : a 0 = 8)
    (a_rec : ∀ n, a (n + 1) = (3 * a n) / 2)
    (b_ini : b 0 = 0)
    (b_rec : ∀ n, b (n + 1) = if a n % 2 = 0 then b n + 2 else b n - 1) :
    ∀ n, b n ≥ 0

Category research open; AMS 05 Combinatorics, 11 Number theory, 68 Computer science. Declared in FormalConjectures/Other/BeaverMathOlympiad.lean, line 98.

BeaverMathOlympiad.beaver_math_olympiad_problem_2_antihydra.variants.set

Open: stated without proof.

BMO#2 formulation variant

Alternative statement of beaver_math_olympiad_problem_2_antihydra using set size comparison instead of a recurrent sequence b.

theorem beaver_math_olympiad_problem_2_antihydra.variants.set
    (a : ℕ → ℕ) (a_ini : a 0 = 8)
    (a_rec : ∀ n, a (n + 1) = (3 * a n) / 2) (n : ℕ) :
    ((Finset.Ico 0 n).filter fun x ↦ Odd (a x)).card ≤
      2 * ((Finset.Ico 0 n).filter fun x ↦ Even (a x)).card

Category research open; AMS 05 Combinatorics, 11 Number theory, 68 Computer science. Declared in FormalConjectures/Other/BeaverMathOlympiad.lean, line 114.

BeaverMathOlympiad.beaver_math_olympiad_problem_3

Solved: stated here; a Lean proof is at https://github.com/gotrevor/collatz-cryptid/blob/62a4b7b0c0af9400098694cb5c5e65120ad4dc67/lean/Collatz/BMO/Problem3.lean#L296.

BMO#3

Let \(v_2(n)\) be the largest integer \(k\) such that \(2^k\) divides \(n\). Let \((a_n)_{n \ge 0}\) be a sequence such that

\[a_n = \begin{cases} 2 & \text{if } n=0 \cr a_{n-1}+2^{v_2(a_{n-1})+2}-1 & \text{if } n \ge 1 \end{cases}\]

for all non-negative integers \(n\). Is there an integer \(n\) such that \(a_n=4^k\) for some positive integer \(k\)?

BMO#3 is equivalent to the non-termination of 2-state 5-symbol Turing machine 1RB0RB3LA4LA2RA_2LB3RA---3RA4RB (from all-0 tape).

The machine was found and informally proven not to halt by bbchallenge.org contributor Daniel Yuan on June 18th 2024; see Discord discussion.

theorem beaver_math_olympiad_problem_3
    (a : ℕ → ℕ)
    (a_ini : a 0 = 2)
    (a_rec : ∀ n, a (n + 1) = (a n) + 2 ^ ((padicValNat 2 (a n)) + 2) - 1) :
    ¬ (∃ n k, a n = 4 ^ k)

Category research solved; AMS 05 Combinatorics, 11 Number theory, 68 Computer science. Declared in FormalConjectures/Other/BeaverMathOlympiad.lean, line 144.

BeaverMathOlympiad.beaver_math_olympiad_problem_4

Solved: stated here; a Lean proof is at https://github.com/gotrevor/collatz-cryptid/blob/62a4b7b0c0af9400098694cb5c5e65120ad4dc67/lean/Collatz/BMO/Problem4.lean#L106.

BMO#4

Bonnie the beaver was bored, so she tried to construct a sequence of integers \(\{a_n\}_{n \ge 0}\). She first defined \(a_0=2\), then defined \(a_{n+1}\) depending on \(a_n\) and \(n\) using the following rules:

  • If \(a_n \equiv 0\text{ (mod 3)}\), then \(a_{n+1}=\frac{a_n}{3}+2^n+1\).
  • If \(a_n \equiv 2\text{ (mod 3)}\), then \(a_{n+1}=\frac{a_n-2}{3}+2^n-1\).

With these two rules alone, Bonnie calculates the first few terms in the sequence: \(2, 0, 3, 6, 11, 18, 39, 78, 155, 306, \dots\). At this point, Bonnie plans to continue writing terms until a term becomes \(1\text{ (mod 3)}\). If Bonnie sticks to her plan, will she ever finish?

BMO#4 is equivalent to the non-termination of 2-state 5-symbol Turing machine 1RB3RB---1LB0LA_2LA4RA3LA4RB1LB (from all-0 tape).

The machine was informally proven not to halt bbchallenge.org contributor Daniel Yuan on July 19th 2024; see sketched proof and Discord discussion.

theorem beaver_math_olympiad_problem_4
    (a : ℕ → ℕ)
    (a_ini : a 0 = 2)
    (a_rec : ∀ n, a (n+1)
      = if a n % 3 = 0 then a n / 3 + 2 ^ n + 1 else (a n - 2) / 3 + 2 ^ n - 1) :
    ¬ (∃ n, a n % 3 = 1)

Category research solved; AMS 05 Combinatorics, 11 Number theory, 68 Computer science. Declared in FormalConjectures/Other/BeaverMathOlympiad.lean, line 176.

BeaverMathOlympiad.beaver_math_olympiad_problem_5

Open: stated without proof.

BMO#5

Let \((a_n)_{n \ge 1}\) and \((b_n)_{n \ge 1}\) be two sequences such that \((a_1, b_1) = (0, 5)\) and

\[(a_{n+1}, b_{n+1}) = \begin{cases} (a_n+1, b_n-f(a_n)) & \text{if } b_n \ge f(a_n) \cr (a_n, 3b_n+a_n+5) & \text{if } b_n < f(a_n) \end{cases}\]

where \(f(x)=10\cdot 2^x-1\) for all non-negative integers \(x\).

Does there exist a positive integer \(i\) such that \(b_i = f(a_i)-1\)?

BMO#5 is equivalent to asking whether the 6-state Turing machine 1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE halts or not.

There is presently no consensus on whether the machine halts or not, hence the problem is tagged as a question.

The machine was discovered by bbchallenge.org contributor mxdys on August 7th 2024.

The correspondence between the machine's halting problem and the below reformulation has been proven in Rocq.

theorem beaver_math_olympiad_problem_5 :
    ∀ (a b f : ℕ → ℕ), ∀ᵉ (hf : f = fun x ↦ 10 * 2 ^ x - 1)
    (a_ini : a 0 = 0) (b_ini : b 0 = 5)
    (a_rec : ∀ n, a (n + 1) = if f (a n) ≤ b n then a n + 1 else a n)
    (b_rec : ∀ n, b (n+1) = if f (a n) ≤ b n then b n - f (a n) else 3 * b n + a n + 5),
    ∃ i, b i = f (a i) - 1

Category research open; AMS 05 Combinatorics, 11 Number theory, 68 Computer science. Declared in FormalConjectures/Other/BeaverMathOlympiad.lean, line 211.

BeaverMathOlympiad.beaver_math_olympiad_problem_8

Open: stated without proof.

BMO#8

Let \((a_n)_{n \ge 1}\) and \((b_n)_{n \ge 1}\) be two sequences such that \((a_1, b_1) = (10, 12)\) and

\[(a_{n+1}, b_{n+1}) = \begin{cases} (a_n - \lfloor b_n/2 \rfloor - 3, 3 \lfloor (b_n+1)/2 \rfloor + 6) & \text{if } a_n > \lfloor b_n/2 \rfloor \cr (3 a_n + 5, b_n - 2 a_n) & \text{if } a_n \le \lfloor b_n/2 \rfloor \end{cases}\]

for all positive integers \(n\). Does there exist a positive integer \(i\) such that \(a_i = \lfloor b_i/2 \rfloor + 1\)?

BMO#8 is equivalent to asking whether the 6-state Turing machine 1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA halts or not.

There is presently no consensus on whether the machine halts or not, hence the problem is tagged as a question.

theorem beaver_math_olympiad_problem_8 :
    ∀ᵉ (a : ℕ → ℤ) (b : ℕ → ℤ)
    (a_ini : a 0 = 10)
    (a_rec : ∀ n, a (n + 1) =
      if b n / 2 < a n then a n - b n / 2 - 3 else 3 * a n + 5)
    (b_ini : b 0 = 12)
    (b_rec : ∀ n, b (n + 1) =
      if b n / 2 < a n then 3 * ((b n + 1) / 2) + 6 else b n - 2 * a n),
    ∃ i, a i = b i / 2 + 1

Category research open; AMS 05 Combinatorics, 11 Number theory, 68 Computer science. Declared in FormalConjectures/Other/BeaverMathOlympiad.lean, line 239.

Sources
LeanBeaverMathOlympiad.beaver_math_olympiad_problem_1 · BeaverMathOlympiad.beaver_math_olympiad_problem_2_antihydra · BeaverMathOlympiad.beaver_math_olympiad_problem_2_antihydra.variants.set · BeaverMathOlympiad.beaver_math_olympiad_problem_3 · BeaverMathOlympiad.beaver_math_olympiad_problem_4 · BeaverMathOlympiad.beaver_math_olympiad_problem_5 · BeaverMathOlympiad.beaver_math_olympiad_problem_8

TheoremEquational Theories#

Reference: Equational Theories project site

Quoted from FormalConjectures/Other/EquationalTheories_677_255.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.

EquationalTheories_677_255.Equation255_not_implies_Equation677

Proved here.

Equation 255 does not imply Equation 677.

theorem Equation255_not_implies_Equation677 :
    ∃ (G : Type) (_ : Magma G), Equation255 G ∧ ¬ Equation677 G

Category research solved; AMS 08 General algebraic systems. Declared in FormalConjectures/Other/EquationalTheories_677_255.lean, line 41.

EquationalTheories_677_255.Equation677_not_implies_Equation255

Solved: stated here without proof.

Equation 677 does not imply Equation 255.

theorem Equation677_not_implies_Equation255 :
    ∃ (G : Type) (_ : Magma G), Equation677 G ∧ ¬ Equation255 G

Category research solved; AMS 08 General algebraic systems. Declared in FormalConjectures/Other/EquationalTheories_677_255.lean, line 48.

EquationalTheories_677_255.Finite.Equation255_not_implies_Equation677

Proved here.

Note that this is a stronger form of Equation255_not_implies_Equation677.

theorem Finite.Equation255_not_implies_Equation677 :
    ∃ (G : Type) (_ : Magma G), Finite G ∧ Equation255 G ∧ ¬ Equation677 G

Category research solved; AMS 08 General algebraic systems. Declared in FormalConjectures/Other/EquationalTheories_677_255.lean, line 54.

EquationalTheories_677_255.Finite.Equation677_implies_Equation255

Open: stated without proof.

Equational Theories, Problem 8.1. Does Equation 677 imply Equation 255 in every finite magma? The project tentatively conjectures that the answer is no; a false answer is equivalent to the existence of a finite countermodel satisfying Equation 677 but not Equation 255.

Discussion thread: https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/FINITE.3A.20677.20-.3E.20255

theorem Finite.Equation677_implies_Equation255 :
    ∀ (G : Type) (_ : Magma G), Finite G → Equation677 G → Equation255 G

Category research open; AMS 08 General algebraic systems. Declared in FormalConjectures/Other/EquationalTheories_677_255.lean, line 67.

Sources
LeanEquationalTheories_677_255.Equation255_not_implies_Equation677 · EquationalTheories_677_255.Equation677_not_implies_Equation255 · EquationalTheories_677_255.Finite.Equation255_not_implies_Equation677 · EquationalTheories_677_255.Finite.Equation677_implies_Equation255

TheoremThe Gerstenhaber problem for three commuting matrices#

Gerstenhaber proved in 1961 [Ger61] that the unital algebra generated by two commuting \(n \times n\) matrices over a field has dimension at most \(n\). It is an open problem, known as the Gerstenhaber problem, whether the same bound holds for three pairwise commuting matrices. The bound fails for four or more pairwise commuting matrices.

References: - [Ger61] M. Gerstenhaber, On dominance and varieties of commuting matrices. Annals of Mathematics (2) 73 (1961), no. 2, 324–348. https://doi.org/10.2307/1970336 - arXiv:2402.16334, M. Satriano and W. Zhang, On the algebra generated by three commuting matrices: combinatorial cases. - arXiv:2006.08588, J. Holbrook and M. Omladič, A computing strategy and programs to resolve the Gerstenhaber Problem for commuting triples of matrices.

Quoted from FormalConjectures/Other/GerstenhaberThreeMatrices.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.

Gerstenhaber.finrank_adjoin_pair_le

Solved: stated here without proof.

Gerstenhaber's theorem [Ger61]: if \(A\) and \(B\) are commuting \(n \times n\) matrices over a field \(K\), then the unital \(K\)-algebra \(K[A, B]\) they generate has dimension at most \(n\).

theorem finrank_adjoin_pair_le (A B : Matrix (Fin n) (Fin n) K) (hAB : Commute A B) :
    Module.finrank K (Algebra.adjoin K {A, B}) ≤ n

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory, 16 Associative rings and algebras. Declared in FormalConjectures/Other/GerstenhaberThreeMatrices.lean, line 51.

Gerstenhaber.finrank_adjoin_triple_le

Open: stated without proof.

The Gerstenhaber problem: if \(A\), \(B\), and \(C\) are pairwise commuting \(n \times n\) matrices over a field \(K\), is the dimension of the unital \(K\)-algebra \(K[A, B, C]\) they generate always at most \(n\)?

theorem finrank_adjoin_triple_le :
    ∀ (K : Type*) [Field K] (n : ℕ) (A B C : Matrix (Fin n) (Fin n) K),
      ({A, B, C} : Set (Matrix (Fin n) (Fin n) K)).Pairwise Commute →
        Module.finrank K (Algebra.adjoin K {A, B, C}) ≤ n

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 16 Associative rings and algebras. Declared in FormalConjectures/Other/GerstenhaberThreeMatrices.lean, line 61.

Gerstenhaber.exists_finrank_adjoin_quadruple_gt

Proved here.

The analogue of Gerstenhaber's theorem fails for four pairwise commuting matrices: over any field there are four pairwise commuting \(4 \times 4\) matrices generating a unital algebra of dimension greater than \(4\). The standard example is \(e_{13}, e_{14}, e_{23}, e_{24}\), whose pairwise products all vanish, so the algebra they generate has dimension \(5\).

theorem exists_finrank_adjoin_quadruple_gt (K : Type*) [Field K] :
    ∃ A B C D : Matrix (Fin 4) (Fin 4) K,
      ({A, B, C, D} : Set (Matrix (Fin 4) (Fin 4) K)).Pairwise Commute ∧
      4 < Module.finrank K (Algebra.adjoin K {A, B, C, D})

Category research solved; AMS 15 Linear and multilinear algebra; matrix theory, 16 Associative rings and algebras. Declared in FormalConjectures/Other/GerstenhaberThreeMatrices.lean, line 75.

Sources
LeanGerstenhaber.finrank_adjoin_pair_le · Gerstenhaber.finrank_adjoin_triple_le · Gerstenhaber.exists_finrank_adjoin_quadruple_gt

TheoremResidual finiteness of hyperbolic groups#

Is every hyperbolic group residually finite? Kapovich and Wise [KaWi00] proved that this question is equivalent to asking whether every nontrivial hyperbolic group has a proper subgroup of finite index. Both questions were answered negatively by an internal OpenAI model in September 2026 [OAI26a].

References: - [BMS] G. Baumslag, A. G. Myasnikov and V. Shpilrain, Open problems in combinatorial group theory, Problem (H1), online. - [Be04] M. Bestvina, Questions in geometric group theory, updated July 2004, Q 1.15, pdf. - [KaWi00] I. Kapovich and D. T. Wise, The equivalence of some residual properties of word-hyperbolic groups, J. Algebra 223 (2000), 562–583, doi:10.1006/jabr.1999.8104. - [OAI26a] OpenAI, A torsion-free hyperbolic group that is not residually finite. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/a-torsion-free-hyperbolic-group-that-is-not-residually-finite-September-23-2026/paper.pdf

Quoted from FormalConjectures/Other/HyperbolicGroupsResiduallyFinite.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.

HyperbolicGroupsResiduallyFinite.hyperbolic_residuallyFinite

Solved: stated here without proof.

Is every hyperbolic group residually finite?

This is Problem (H1)(a) in [BMS] and Q 1.15 in [Be04].

No. This was disproved by an internal OpenAI model in September 2026 [OAI26a], which constructs a torsion-free hyperbolic group that is not residually finite. The Lean proof of [OAI26a] defines hyperbolicity by uniformly thin geodesic triangles in a Cayley graph. That definition is equivalent to Group.IsHyperbolic, but the equivalence is not part of the Lean proof.

theorem hyperbolic_residuallyFinite :
    ¬ ∀ (G : Type) [Group G] [Group.IsHyperbolic G], Group.ResiduallyFinite G

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Other/HyperbolicGroupsResiduallyFinite.lean, line 59.

HyperbolicGroupsResiduallyFinite.hyperbolic_exists_finiteIndex_ne_top

Solved: stated here without proof.

Does every nontrivial hyperbolic group have a proper subgroup of finite index?

This is Problem (H1)(b) in [BMS]. The trivial group has no proper subgroup, so we assume that \(G\) is nontrivial.

No. By [KaWi00] (see hyperbolic_residuallyFinite_iff_exists_finiteIndex_ne_top), this problem is equivalent to hyperbolic_residuallyFinite, which was disproved in [OAI26a].

theorem hyperbolic_exists_finiteIndex_ne_top :
    ¬ ∀ (G : Type) [Group G] [Group.IsHyperbolic G] [Nontrivial G],
      ∃ H : Subgroup G, H ≠ ⊤ ∧ H.FiniteIndex

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Other/HyperbolicGroupsResiduallyFinite.lean, line 73.

HyperbolicGroupsResiduallyFinite.hyperbolic_residuallyFinite_iff_exists_finiteIndex_ne_top

Solved: stated here without proof.

Every hyperbolic group is residually finite if and only if every nontrivial hyperbolic group has a proper subgroup of finite index.

This is the theorem of [KaWi00] that Problems (H1)(a) and (H1)(b) are equivalent.

theorem hyperbolic_residuallyFinite_iff_exists_finiteIndex_ne_top :
    (∀ (G : Type) [Group G] [Group.IsHyperbolic G], Group.ResiduallyFinite G) ↔
      ∀ (G : Type) [Group G] [Group.IsHyperbolic G] [Nontrivial G],
        ∃ H : Subgroup G, H ≠ ⊤ ∧ H.FiniteIndex

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/Other/HyperbolicGroupsResiduallyFinite.lean, line 85.

Sources
LeanHyperbolicGroupsResiduallyFinite.hyperbolic_residuallyFinite · HyperbolicGroupsResiduallyFinite.hyperbolic_exists_finiteIndex_ne_top · HyperbolicGroupsResiduallyFinite.hyperbolic_residuallyFinite_iff_exists_finiteIndex_ne_top

TheoremThe Rule 30 Prize Problems#

Rule 30 is the elementary cellular automaton with local update \(c' = l \oplus (c \lor r)\), the Boolean rule numbered \(30\) by Wolfram. Started from a single black cell on a bi-infinite row, its center column t ↦ (state t) 0 looks random — it was long Mathematica's default pseudorandom generator — yet nothing about that randomness is proven. In 2019 Wolfram offered the Rule 30 Prizes for three questions about it; we formalize the first two.

  • Problem 1. Is the center column non-periodic (never eventually periodic)?
  • Problem 2. Does each color occur on average equally often, i.e. does the running average of the values converge to \(1/2\)?

Problem 3 — whether computing the \(n\)-th cell requires at least \(O(n)\) work — is omitted. It is model-relative and has no canonical model-independent phrasing. All three are open.

References: - Announcing the Rule 30 Prizes, Stephen Wolfram, 2019. - Rule 30 Prizes. - Wikipedia: Rule 30.

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

Rule30.centerColumn_not_eventually_periodic

Open: stated without proof.

Rule 30 Prize, Problem 1 (non-periodicity). The center column of Rule 30 is not eventually periodic: there is no positive period \(p\) and threshold \(N\) past which the column repeats with period \(p\).

theorem centerColumn_not_eventually_periodic :
    ¬ ∃ p : ℕ, 0 < p ∧ ∃ N : ℕ, ∀ t : ℕ, N ≤ t → centerColumn (t + p) = centerColumn t

Category research open; AMS 37 Dynamical systems and ergodic theory, 68 Computer science. Declared in FormalConjectures/Other/Rule30.lean, line 81.

Rule30.centerColumn_frequency_half

Open: stated without proof.

Rule 30 Prize, Problem 2 (equal frequency). Each color occurs on average equally often in the center column: the set of times at which it is black has natural density \(1/2\). This is Wolfram's phrasing that the discrete limit of \(\mathrm{Total}[c[t]]/t\) as \(t \to \infty\) is \(1/2\).

theorem centerColumn_frequency_half :
    {t : ℕ | centerColumn t}.HasDensity (1 / 2)

Category research open; AMS 37 Dynamical systems and ergodic theory, 68 Computer science. Declared in FormalConjectures/Other/Rule30.lean, line 90.

Sources
LeanRule30.centerColumn_not_eventually_periodic · Rule30.centerColumn_frequency_half

TheoremSchur's theorem on Galois groups of truncated exponential polynomials#

Reference: (https://math.stackexchange.com/questions/2814220)

Reference (https://mathoverflow.net/questions/477077)

Quoted from FormalConjectures/Other/SchurTruncatedExponential.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.

SchurTruncatedExponential.schur_truncatedExp_galoisGroup_equiv

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/83f95df1123bfdc7937bb7358bb65f658c30d554/Proofs/T_SchurTruncatedExponential_schur_truncatedExp_galoisGroup_equiv.lean#L2204.

Schur's Theorem (1924): Let f_n(x) = ∑_{j=0}^n x^j/j! be the n-th truncated exponential polynomial over ℚ. Then for n ≥ 2:

  • If n ≡ 0 (mod 4), the Galois group of f_n is isomorphic to the alternating group A_n
  • If n ≢ 0 (mod 4), the Galois group of f_n is isomorphic to the symmetric group S_n
theorem schur_truncatedExp_galoisGroup_equiv (n : ℕ) (hn : n ≥ 2) :
  letI f := truncatedExp n
  if n % 4 = 0 then
    -- Galois group is alternating group A_n
    Nonempty (f.Gal ≃* alternatingGroup (Fin n))
  else
    -- Galois group is symmetric group S_n
    Nonempty (f.Gal ≃* Equiv.Perm (Fin n))

Category research solved; AMS 12 Field theory and polynomials. Declared in FormalConjectures/Other/SchurTruncatedExponential.lean, line 58.

Sources
LeanSchurTruncatedExponential.schur_truncatedExp_galoisGroup_equiv

TheoremSmarandache–Wellin primes#

The Smarandache–Wellin numbers are formed by concatenating the decimal expansions of the successive primes: \(2, 23, 235, 2357, \ldots\). It is conjectured that infinitely many members of this sequence are prime.

References: * Smarandache Problems * OEIS A019518 * OEIS A069151 * OEIS A046035

Quoted from FormalConjectures/Other/SmarandacheWellinPrime.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, counted here but not shown.

SmarandacheWellinPrime.conjecture

Open: stated without proof.

Smarandache Problems states: "There are infinitely many primes in the smarandache concatenated prime sequence."

theorem conjecture : {n : ℕ | (a n).Prime}.Infinite

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Other/SmarandacheWellinPrime.lean, line 100.

Sources
LeanSmarandacheWellinPrime.conjecture

TheoremSuffix-prefix avoidance bound#

Let \(A\) and \(B\) be sets of words of length \(n\) over an alphabet with \(q\) letters. If no (nonempty) suffix of any word in \(A\) coincides with a prefix of any word in \(B\), then

\[|A| \cdot |B| \leq \frac{q^{2n}}{en}.\]

References: - X post by Dmitry Rybin - [Maximal sets of strings with no prefix-suffix overlap] (https://mathoverflow.net/questions/508648/maximal-sets-of-strings-with-no-prefix-suffix-overlap) by Dmitry Rybin, MathOverflow (2026) - An isoperimetric inequality for word overlap by Dmitrii Zakharov (2026)

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

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

SuffixPrefixAvoidance.suffix_prefix_avoidance_bound

Solved: stated here without proof.

\(A\) and \(B\) are sets of words of length \(n\) over alphabet with \(q \geq 1\) letters. No suffix of a word in \(A\) coincides with a prefix of a word in \(B\). Then \(|A| \cdot |B|\) is at most \(\frac{q^{2n}}{en}\).

This problem is from Maximal sets of strings with no prefix-suffix overlap and was proved in An isoperimetric inequality for word overlap.

theorem suffix_prefix_avoidance_bound
    (A B : Finset (Fin n → Fin q))
    (hq : 0 < q) (hn : 0 < n)
    (h : IsSuffixPrefixAvoiding A B) :
    (A.card : ℝ) * B.card ≤ (q : ℝ) ^ (2 * n) / (exp 1 * n)

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/Other/SuffixPrefixAvoidance.lean, line 76.

SuffixPrefixAvoidance.suffix_prefix_avoidance_weaker_bound

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/102e47fee802d461946e3a4e0b47fdbe7db4c1ed/FormalConjectures/Other/SuffixPrefixAvoidance.lean#L157.

\(A\) and \(B\) are sets of words of length \(n\) over alphabet with \(q \geq 1\) letters. No suffix of a word in \(A\) coincides with a prefix of a word in \(B\). Then \(|A| \cdot |B|\) is at most \(\frac{q^{2n}}{n}\).

theorem suffix_prefix_avoidance_weaker_bound
    (A B : Finset (Fin n → Fin q))
    (_hq : 0 < q) (hn : 0 < n)
    (h : IsSuffixPrefixAvoiding A B) :
    (A.card : ℚ) * B.card ≤ (q : ℚ) ^ (2 * n) / n

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

Sources
LeanSuffixPrefixAvoidance.suffix_prefix_avoidance_bound · SuffixPrefixAvoidance.suffix_prefix_avoidance_weaker_bound

TheoremThe symbol length of \(K^M_n(\mathbb{C}(x_1, \dots, x_m))/p\)#

For a field \(F\) and \(\ell \ge 1\), the Milnor K-group \(K^M_n(F)/\ell\) is generated by the symbols \(\{a_1, \dots, a_n\}\) with \(a_i \in F^\times\), and the symbol length of a class is the least number of symbols in a decomposition of the class as a sum of symbols. The symbol length of \(K^M_n(F)/\ell\) is the supremum of the symbol lengths of its classes. When \(\ell\) is invertible in \(F\), the norm residue isomorphism theorem (the Bloch–Kato conjecture, [Voevodsky2011]) gives \(K^M_n(F)/\ell \cong H^n(F, \mu_\ell^{\otimes n})\), so this is also the symbol length of Galois cohomology.

The symbol length problem asks, for a given field \(F\) and integers \(n\) and \(\ell\), for a \(k\) such that the symbol length of every class in \(K^M_n(F)/\ell\) is at most \(k\), for example in terms of a dimension of the field. That a class is a sum of some number of symbols is part of the presentation of \(K^M_n(F)\) recalled above, so the content lies entirely in the bound. In degree \(2\), over a field containing a primitive \(\ell\)-th root of unity, Merkurjev and Suslin's theorem [MerkurjevSuslin1983] that the norm residue map is an isomorphism identifies \(K^M_2(F)/\ell\) with the \(\ell\)-torsion of the Brauer group and symbols with symbol algebras of degree \(\ell\); that is the form in which the question is usually studied, namely how many symbol algebras are needed to represent a central simple algebra of exponent \(\ell\). Becher and Hoffmann [BecherHoffmann2004] named the invariant \(\lambda_p\) in that degree and asked it for exactly the fields considered below (their Question 4.6). The general form stated here is Problem 2.1.3.12 of Krashen's PCMI notes; Krashen notes there that over complex function fields in at least three variables no bound is known beyond Matzri's in degree \(2\) and the case of \(\ell\) a power of \(2\), which comes from the theory of quadratic forms, and that very little is known in degree \(3\) and higher [Krashen2024, §2.1.3.4].

This file states the problem for the rational function fields \(\mathbb{C}(x_1, \dots, x_m)\) and a prime \(\ell = p\): determine the symbol length of \(K^M_n(\mathbb{C}(x_1, \dots, x_m))/p\) as a function of \(m\), \(n\) and \(p\), where the symbol length is infinite if there is no bound.

What is known: * in degree \(0\) every symbol is the empty product \(1\), so \(K^M_0(F)/p = \mathbb{Z}/p\) has symbol length \(p - 1\) for every field \(F\); * in degree \(1\) every class of \(K^M_1(F)/p = F^\times/(F^\times)^p\) is a single symbol, so the symbol length is at most \(1\); * \(\mathbb{C}(x_1, \dots, x_m)\) has cohomological dimension \(m\) [Serre1997, Ch. II, §4.2], so \(K^M_n(\mathbb{C}(x_1, \dots, x_m))/p = 0\) for \(n > m\) and the symbol length is \(0\); * \(\mathbb{C}(x_1, \dots, x_m)\) is a \(C_m\) field (Tsen–Lang, [Lang1952]), so by Matzri's theorem [Matzri2016, Theorem 8.2] every class in \(K^M_2(\mathbb{C}(x_1, \dots, x_m))/p^t\) is a sum of at most \(t(p^{m-1} - 1)\) symbols when \(m \ge 1\); * in degree \(2\) a tensor product of \(m - 1\) symbol algebras of degree \(p\) over \(\mathbb{C}(x_1, \dots, x_m)\) can be a division algebra, so the symbol length is at least \(m - 1\) for \(m \ge 1\) [BecherHoffmann2004, Proposition 4.5], by an argument going back to Nakayama.

In degree \(2\), Becher and Hoffmann ask whether that lower bound is the answer, that is whether the symbol length is exactly \(m - 1\) [BecherHoffmann2004, Question 4.6]. For \(m = n = 2\), the smallest case not settled above, this asks whether every class of \(K^M_2(\mathbb{C}(x_1, x_2))/p\) is a single symbol; they call it "a striking open question" and note that it holds for \(p \le 3\) by a theorem of Artin [BecherHoffmann2004, Introduction]. Since \(m - 1\) does not involve \(p\), their question is an instance of the expectation recorded in [Krashen2024, §2.1.3.4] that a bound can be taken independent of \(\ell\). See also the survey [Krashen2016].

The definitions MilnorK, MilnorK.symbol, MilnorK.grade and MilnorK.symbolLengthBounds are in FormalConjecturesForMathlib/FieldTheory/MilnorKTheory.lean.

References: - [Krashen2024] D. Krashen, PCMI Summer School (not quite) notes, notes for the minicourse Field arithmetic and the complexity of algebraic objects, PCMI Graduate Summer School on Motivic Homotopy Theory, 2024, draft of 24 July 2024, pdf. - [BecherHoffmann2004] K. J. Becher and D. W. Hoffmann, Symbol lengths in Milnor \(K\)-theory, Homology Homotopy Appl. 6 (2004), no. 1, 17–31, doi:10.4310/HHA.2004.v6.n1.a3. - [MerkurjevSuslin1983] A. S. Merkurjev and A. A. Suslin, K-cohomology of Severi–Brauer varieties and the norm residue homomorphism, Izv. Akad. Nauk SSSR Ser. Mat. 46 (1982), 1011–1046; English translation Math. USSR-Izv. 21 (1983), no. 2, 307–340, doi:10.1070/IM1983v021n02ABEH001793. - [Krashen2016] D. Krashen, Period and index, symbol lengths, and generic splittings in Galois cohomology, Bull. London Math. Soc. 48 (2016), 985–1000, doi:10.1112/blms/bdw060. - [Matzri2016] E. Matzri, Symbol length in the Brauer group of a field, Trans. Amer. Math. Soc. 368 (2016), 413–427, doi:10.1090/tran/6326, arXiv:1402.0332. - [Lang1952] S. Lang, On quasi algebraic closure, Ann. of Math. (2) 55 (1952), 373–390, doi:10.2307/1969785. - [Serre1997] J.-P. Serre, Galois cohomology, Springer Monographs in Mathematics, Springer, 1997, doi:10.1007/978-3-642-59141-9. - [Voevodsky2011] V. Voevodsky, On motivic cohomology with Z/l-coefficients, Ann. of Math. (2) 174 (2011), 401–438, doi:10.4007/annals.2011.174.1.11.

Quoted from FormalConjectures/Other/SymbolLengthMilnorKTheory.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, 3 solved and 3 textbook results.

SymbolLengthMilnorKTheory.symbol_length_problem

Open: stated without proof.

The symbol length problem for complex rational function fields [Krashen2024, Problem 2.1.3.12 and §2.1.3.4]: determine, as a function of \(m\), \(n\) and the prime \(p\), the symbol length of \(K^M_n(\mathbb{C}(x_1, \dots, x_m))/p\), that is the least \(k\) such that every class is a sum of at most \(k\) symbols, or \(\infty\) if there is no such \(k\). The answer sl m n p : ℕ∞ is characterised by: k is such a bound if and only if sl m n p ≤ k.

theorem symbol_length_problem :
    ∀ m n p : ℕ, p.Prime → ∀ k : ℕ,
      k ∈ symbolLengthBounds (MvRatFunc (Fin m) ℂ) p n ↔ symbol_length_problem.answer m n p ≤ k

Category research open; AMS 12 Field theory and polynomials, 19 K-theory. Declared in FormalConjectures/Other/SymbolLengthMilnorKTheory.lean, line 122.

SymbolLengthMilnorKTheory.symbol_length_problem.variants.bounded

Open: stated without proof.

The symbol length problem in the form of [Krashen2024, Problem 2.1.3.12]: is there, for every \(m\), \(n\) and prime \(p\), a bound \(k\) such that every class in \(K^M_n(\mathbb{C}(x_1, \dots, x_m))/p\) is a sum of at most \(k\) symbols?

theorem symbol_length_problem.variants.bounded :
    ∀ m n p : ℕ, p.Prime →
      (symbolLengthBounds (MvRatFunc (Fin m) ℂ) p n).Nonempty

Category research open; AMS 12 Field theory and polynomials, 19 K-theory. Declared in FormalConjectures/Other/SymbolLengthMilnorKTheory.lean, line 134.

SymbolLengthMilnorKTheory.symbol_length_problem.variants.uniform

Open: stated without proof.

The expectation recorded in [Krashen2024, §2.1.3.4] that the bound can be taken independent of the prime: is there, for every \(m\) and every \(n \ge 1\), a \(k\) such that every class in \(K^M_n(\mathbb{C}(x_1, \dots, x_m))/p\) is a sum of at most \(k\) symbols for every prime \(p\)? Degree \(0\) is excluded because \(K^M_0(F)/p = \mathbb{Z}/p\) has symbol length \(p - 1\) (symbol_length_problem.variants.degree_zero), which is not bounded independently of \(p\).

theorem symbol_length_problem.variants.uniform :
    ∀ m n : ℕ, 0 < n → ∃ k : ℕ, ∀ p : ℕ, p.Prime →
      k ∈ symbolLengthBounds (MvRatFunc (Fin m) ℂ) p n

Category research open; AMS 12 Field theory and polynomials, 19 K-theory. Declared in FormalConjectures/Other/SymbolLengthMilnorKTheory.lean, line 147.

SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_zero

Textbook result, proved here.

The degree-\(0\) case of symbol_length_problem: \(K^M_0(\mathbb{C}(x_1, \dots, x_m))/p = \mathbb{Z}/p\) has symbol length \(p - 1\), since every symbol of degree \(0\) is the empty product \(1\).

theorem symbol_length_problem.variants.degree_zero (m p : ℕ) (hp : p.Prime) :
    IsLeast (symbolLengthBounds (MvRatFunc (Fin m) ℂ) p 0) (p - 1)

Category textbook; AMS 12 Field theory and polynomials, 19 K-theory. Declared in FormalConjectures/Other/SymbolLengthMilnorKTheory.lean, line 157.

SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_one

Textbook result, proved here.

The degree-\(1\) case of symbol_length_problem: every class of \(K^M_1(\mathbb{C}(x_1, \dots, x_m))/p = F^\times/(F^\times)^p\) is a single symbol, so the symbol length in degree \(1\) is at most \(1\).

theorem symbol_length_problem.variants.degree_one (m p : ℕ) :
    1 ∈ symbolLengthBounds (MvRatFunc (Fin m) ℂ) p 1

Category textbook; AMS 12 Field theory and polynomials, 19 K-theory. Declared in FormalConjectures/Other/SymbolLengthMilnorKTheory.lean, line 167.

SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_two

Solved: stated here without proof.

Matzri's theorem [Matzri2016, Theorem 8.2] for \(\mathbb{C}(x_1, \dots, x_m)\), which is a \(C_m\) field by Tsen–Lang [Lang1952]: for \(m \ge 1\), every class in \(K^M_2(\mathbb{C}(x_1, \dots, x_m))/p^t\) is a sum of at most \(t(p^{m-1} - 1)\) symbols.

theorem symbol_length_problem.variants.degree_two (m : ℕ) (hm : 1 ≤ m) (p t : ℕ)
    (hp : p.Prime) :
    t * (p ^ (m - 1) - 1) ∈ symbolLengthBounds (MvRatFunc (Fin m) ℂ) (p ^ t) 2

Category research solved; AMS 12 Field theory and polynomials, 16 Associative rings and algebras, 19 K-theory. Declared in FormalConjectures/Other/SymbolLengthMilnorKTheory.lean, line 177.

SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_two_ge

Solved: stated here without proof.

The matching lower bound in degree \(2\) [BecherHoffmann2004, Proposition 4.5], by an argument going back to Nakayama: for distinct monic irreducibles \(f_1, \dots, f_{m-1}\) in \(\mathbb{C}[x_1]\) the tensor product of the symbol algebras \((f_i, x_{i+1})_p\) is a division algebra over \(\mathbb{C}(x_1, \dots, x_m)\), so no \(k < m - 1\) bounds the symbol length of \(K^M_2(\mathbb{C}(x_1, \dots, x_m))/p\).

theorem symbol_length_problem.variants.degree_two_ge (m : ℕ) (hm : 1 ≤ m) (p : ℕ)
    (hp : p.Prime) :
    ∀ k ∈ symbolLengthBounds (MvRatFunc (Fin m) ℂ) p 2, m - 1 ≤ k

Category research solved; AMS 12 Field theory and polynomials, 16 Associative rings and algebras, 19 K-theory. Declared in FormalConjectures/Other/SymbolLengthMilnorKTheory.lean, line 190.

SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_two_isLeast

Open: stated without proof.

Becher and Hoffmann's question [BecherHoffmann2004, Question 4.6]: is the symbol length of \(K^M_2(\mathbb{C}(x_1, \dots, x_m))/p\) exactly \(m - 1\)? Their Proposition 4.5 gives the lower bound (symbol_length_problem.variants.degree_two_ge), and Matzri's theorem the much weaker upper bound \(p^{m-1} - 1\) (symbol_length_problem.variants.degree_two). For \(m \le 1\) the group vanishes and the answer is \(0\); for \(m = 2\) the question is whether every class is a single symbol, which holds for \(p \le 3\) by a theorem of Artin and is open for \(p \ge 5\). Since \(m - 1\) does not involve \(p\), an affirmative answer would settle symbol_length_problem.variants.uniform in degree \(2\).

theorem symbol_length_problem.variants.degree_two_isLeast :
    ∀ m p : ℕ, 1 ≤ m → p.Prime →
      IsLeast (symbolLengthBounds (MvRatFunc (Fin m) ℂ) p 2) (m - 1)

Category research open; AMS 12 Field theory and polynomials, 16 Associative rings and algebras, 19 K-theory. Declared in FormalConjectures/Other/SymbolLengthMilnorKTheory.lean, line 206.

SymbolLengthMilnorKTheory.symbol_length_problem.variants.zero_mem_of_lt

Solved: stated here without proof.

\(K^M_n(\mathbb{C}(x_1, \dots, x_m))/p = 0\) for \(n > m\): the field has cohomological dimension \(m\) [Serre1997, Ch. II, §4.2], so \(H^n(\mathbb{C}(x_1, \dots, x_m), \mu_p^{\otimes n}) = 0\), and \(K^M_n/p \cong H^n(-, \mu_p^{\otimes n})\) by the norm residue isomorphism theorem [Voevodsky2011].

theorem symbol_length_problem.variants.zero_mem_of_lt (m n p : ℕ) (hmn : m < n) (hp : p.Prime) :
    0 ∈ symbolLengthBounds (MvRatFunc (Fin m) ℂ) p n

Category research solved; AMS 12 Field theory and polynomials, 19 K-theory. Declared in FormalConjectures/Other/SymbolLengthMilnorKTheory.lean, line 217.

SymbolLengthMilnorKTheory.symbol_length_problem.variants.isAlgClosed

Textbook result, proved here.

\(K^M_n(F)/\ell = 0\) for an algebraically closed field \(F\) and \(n, \ell \ge 1\), since every unit is an \(\ell\)-th power: every symbol \(\{a_1, \dots, a_n\}\) with \(a_1 = b^\ell\) equals \(\ell \{b, a_2, \dots, a_n\} = 0\). This generalizes the case \(m = 0\) of symbol_length_problem.variants.zero_mem_of_lt, which concerns a prime \(\ell\) and the field \(\mathbb{C}(x_1, \dots, x_0) \cong \mathbb{C}\).

theorem symbol_length_problem.variants.isAlgClosed (F : Type*) [Field F] [IsAlgClosed F]
    (n ℓ : ℕ) (hn : 0 < n) (hℓ : 0 < ℓ) : 0 ∈ symbolLengthBounds F ℓ n

Category textbook; AMS 12 Field theory and polynomials, 19 K-theory. Declared in FormalConjectures/Other/SymbolLengthMilnorKTheory.lean, line 229.

Sources
LeanSymbolLengthMilnorKTheory.symbol_length_problem · SymbolLengthMilnorKTheory.symbol_length_problem.variants.bounded · SymbolLengthMilnorKTheory.symbol_length_problem.variants.uniform · SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_zero · SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_one · SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_two · SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_two_ge · SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_two_isLeast · SymbolLengthMilnorKTheory.symbol_length_problem.variants.zero_mem_of_lt · SymbolLengthMilnorKTheory.symbol_length_problem.variants.isAlgClosed

LemmaVCₙ dimension of convex sets in ℝⁿ, ℝⁿ⁺¹, ℝⁿ⁺²#

In the literature it is known that every convex set in ℝ² has VC dimension at most 3, and there exists a convex set in ℝ³ with infinite VC dimension (even more strongly, which shatters an infinite set).

This file states that every convex set in ℝⁿ has finite VCₙ dimension, constructs a convex set in ℝⁿ⁺² with infinite VCₙ dimension (even more strongly, which n-shatters an infinite set), and conjectures that every convex set in ℝⁿ⁺¹ has finite VCₙ dimension.

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

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

VCDimConvex.hasAddVCDimAtMost_three_of_convex_r2

Solved: stated here without proof.

Every convex set in \(\mathbb R^2\) has VC dimension at most 3.

lemma hasAddVCDimAtMost_three_of_convex_r2 {C : Set ℝ²} (hC : Convex ℝ C) : HasAddVCDimAtMost C 3

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/Other/VCDimConvex.lean, line 42.

VCDimConvex.exists_infinite_convex_r3_shatters

Solved: stated here without proof.

There exists a set in \(\mathbb R^3\) shattering an infinite set.

lemma exists_infinite_convex_r3_shatters :
    ∃ A C : Set ℝ³, A.Infinite ∧ Convex ℝ C ∧ Shatters {t +ᵥ C | t : ℝ³} A

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/Other/VCDimConvex.lean, line 47.

VCDimConvex.exists_convex_rn_add_two_vc_n_forall_not_hasAddVCNDimAtMost

Solved: stated here without proof.

There exists a set of infinite \(\mathrm{VC}_n\) dimension in \(\mathbb R^{n + 2}\).

lemma exists_convex_rn_add_two_vc_n_forall_not_hasAddVCNDimAtMost (n : ℕ) :
    ∃ C : Set (Fin (n + 2) → ℝ), Convex ℝ C ∧ ∀ d, ¬ HasAddVCNDimAtMost C n d

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/Other/VCDimConvex.lean, line 54.

VCDimConvex.hasAddVCNDimAtMost_two_one_of_convex_r3

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/vcdim-convex-counterexample/blob/ad7ffff1514843c886633f5408c6456dfb2e2a49/formal-conjectures-v4.27.0/VCDimConvexCounterexample.lean.

Not every convex set in \(\mathbb R^3\) has \(\mathrm{VC}_2\) dimension at most 1.

lemma hasAddVCNDimAtMost_two_one_of_convex_r3 :
    ¬ ∀ {C : Set ℝ³} (hC : Convex ℝ C),
      HasAddVCNDimAtMost C 2 1

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/Other/VCDimConvex.lean, line 65.

VCDimConvex.hasAddVCNDimAtMost_two_two_of_convex_r3

Open: stated without proof.

Every convex set in \(\mathbb R^3\) has \(\mathrm{VC}_2\) dimension at most 2.

lemma hasAddVCNDimAtMost_two_two_of_convex_r3 {C : Set ℝ³} (hC : Convex ℝ C) :
    HasAddVCNDimAtMost C 2 2

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/Other/VCDimConvex.lean, line 71.

VCDimConvex.exists_hasAddVCNDimAtMost_n_of_convex_rn_add_one

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/vcdim-convex-finite-bound/blob/9d7685c7c7c8c8e82f47d59da5495a8d5374db99/lean/VCDimConvexBoundFC.lean#L14-L17.

For every \(n \ge 1\) there exists some \(d\) such that every convex set in \(\mathbb R^{n + 1}\) has \(\mathrm{VC}_n\) dimension at most \(d\).

This holds with the explicit bound \(d = 2^{8(n + 2)^n} - 1\); see Kitamura's Lean formalization.

lemma exists_hasAddVCNDimAtMost_n_of_convex_rn_add_one (n : ℕ) (hn : 1 ≤ n) :
    ∃ d : ℕ, ∀ C : Set (Fin (n + 1) → ℝ), Convex ℝ C → HasAddVCNDimAtMost C n d

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/Other/VCDimConvex.lean, line 84.

VCDimConvex.exists_exponential_bound_hasAddVCNDimAtMost_n_of_convex_rn_add_one

Open: stated without proof.

For every \(n \ge 1\) there exists some \(d\) such that every convex set in \(\mathbb R^{n + 1}\) has \(\mathrm{VC}_n\) dimension at most \(d\).

The bound can be taken to be \(d = c^n\) for some constant \(c \ge 2\) independent of \(n\).

lemma exists_exponential_bound_hasAddVCNDimAtMost_n_of_convex_rn_add_one :
    ∃ c : ℕ, 2 ≤ c ∧ ∀ (n : ℕ) (hn : 1 ≤ n),
      ∀ C : Set (Fin (n + 1) → ℝ), Convex ℝ C → HasAddVCNDimAtMost C n (c ^ n)

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/Other/VCDimConvex.lean, line 93.

VCDimConvex.hasAddVCNDimAtMost_n_two_of_convex_rn_add_one

Open: stated without proof.

Is it true that, for all \(n\), every convex set in \(\mathbb R^{n + 1}\) has \(\mathrm{VC}_n\) dimension at most 3?

lemma hasAddVCNDimAtMost_n_two_of_convex_rn_add_one :
    ∀ ⦃n : ℕ⦄, n ≠ 0 → ∀ ⦃C : Set (EuclideanSpace ℝ (Fin (n + 1)))⦄,
      Convex ℝ C → HasAddVCNDimAtMost C n 3

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/Other/VCDimConvex.lean, line 100.

Sources
LeanVCDimConvex.hasAddVCDimAtMost_three_of_convex_r2 · VCDimConvex.exists_infinite_convex_r3_shatters · VCDimConvex.exists_convex_rn_add_two_vc_n_forall_not_hasAddVCNDimAtMost · VCDimConvex.hasAddVCNDimAtMost_two_one_of_convex_r3 · VCDimConvex.hasAddVCNDimAtMost_two_two_of_convex_r3 · VCDimConvex.exists_hasAddVCNDimAtMost_n_of_convex_rn_add_one · VCDimConvex.exists_exponential_bound_hasAddVCNDimAtMost_n_of_convex_rn_add_one · VCDimConvex.hasAddVCNDimAtMost_n_two_of_convex_rn_add_one

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.