Green's Open Problem 28 to Ben Green's Open Problem 50

TheoremGreen's Open Problem 28#

References: - Green, Ben. "100 open problems." (2024). - Mathoverflow/339137 asked by user Sil - MathStackexchange/3325163 asked by user Emmanuel Amiot

Quoted from FormalConjectures/GreensOpenProblems/28.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.

Green28.green_28

Open: stated without proof.

Suppose that \(X, Y\) are two finitely-supported independent random variables taking integer values, and such that \(X + Y\) is uniformly distributed on its range. Are \(X\) and \(Y\) themselves uniformly distributed on their ranges?

theorem green_28 :
  ∀ (X Y : PMF ℤ), -- marginals, independence is built into indepSum
    X.support.Finite ∧ Y.support.Finite ∧ IsUniformOnSupport (indepSum X Y) →
      IsUniformOnSupport X ∧ IsUniformOnSupport Y

Category research open; AMS 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/28.lean, line 52.

Sources

• FormalConjectures/GreensOpenProblems/28.lean at 2055e5ad
• Green, Ben. "100 open problems." (2024).

LeanGreen28.green_28

TheoremBen Green's Open Problem 29#

References: - Ben Green's Open Problem 29 - [Gr12] Green, Ben. "What is... an approximate group." Notices Amer. Math. Soc 59.5 (2012): 655-656. - [Br13] Breuillard, Emmanuel, Ben Green, and Terence Tao. "Small doubling in groups." Erdős Centennial. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013. 129-151. - [Sa10] Sanders, Tom. "On a nonabelian Balog–Szemerédi-type lemma." Journal of the Australian Mathematical Society 89.1 (2010): 127-132. - [CrSi10] Croot, Ernie, and Olof Sisask. "A probabilistic technique for finding almost-periods of convolutions." Geometric and functional analysis 20.6 (2010): 1367-1396.

Quoted from FormalConjectures/GreensOpenProblems/29.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.

Green29.green_29

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/green-29-counterexample/blob/1cbf80c3d5a333b2b79c203c0d60129924c8c712/lean/Green29FC.lean#L280-L287.

Suppose that \(A\) is a \(K\)-approximate group (not necessarily abelian). Is there \(S \subset A\), \(|S| \gg K^{-O(1)} |A|\), with \(S^8 \subset A^4\)?

The answer is negative. A counterexample is given, for arbitrarily large finite groups H, by A = ({-1} × H) ∪ ({1} × H) ∪ {(0, 1)} in Multiplicative ℤ × H.

theorem green_29 :
    ¬ ∃ C c : ℝ, 0 < C ∧ 0 < c ∧
      ∀ {G : Type*} [Group G] [DecidableEq G] (K : ℝ) (A : Finset G),
        1 ≤ K → IsApproximateSubgroup K (A : Set G) →
          ∃ S ⊆ A, C * K ^ (-c) * (A.card : ℝ) ≤ (S.card : ℝ) ∧
          S ^ 8 ⊆ A ^ 4

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/GreensOpenProblems/29.lean, line 50.

Green29.green_29.variant

Solved: stated here without proof.

Such a conclusion is known with \(|S| \gg_K |A|\) [Br13 Problem 6.5, CrSi10, Sa10].

theorem green_29.variant :
    ∀ K : ℝ, 1 ≤ K →
      ∃ c : ℝ, 0 < c ∧ -- Allow c to depend on K.
        ∀ {G : Type*} [Group G] [DecidableEq G] (A : Finset G),
          IsApproximateSubgroup K (A : Set G) →
            ∃ S : Finset G, -- No S ⊆ A requirement in this variant.
              c * (A.card : ℝ) ≤ (S.card : ℝ) ∧
              S ^ 8 ⊆ A ^ 4

Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/GreensOpenProblems/29.lean, line 60.

Sources

• FormalConjectures/GreensOpenProblems/29.lean at 2055e5ad
• Ben Green's Open Problem 29

LeanGreen29.green_29 · Green29.green_29.variant

TheoremBen Green's Open Problem 31#

Write \(F(N)\) for the largest Sidon subset of \([N]\). Improve, at least for infinitely many \(N\), the bounds \(N^{1/2} + O(1) \le F(N) \le N^{1/2} + N^{1/4} + O(1)\).

Note: the upper bound was improved to \(N^{1/2} + 0.98183 N^{1/4} + O(1)\) in [CHO25], and then to \(N^{1/2} + 0.94349\ldots N^{1/4} + O(1)\) in [HZ26].

Related to Erdős Problem 30.

References: - [Gr24] Ben Green's Open Problem 31 - [Gr01] Green, Ben. "The number of squares and $ B_h [g] $ sets." Acta Arithmetica 100.4 (2001): 365-390. - [BFR23] Balogh, József, Zoltán Füredi, and Souktik Roy. "An upper bound on the size of Sidon sets." The American Mathematical Monthly 130.5 (2023): 437-445. - [CHO25] Carter, Daniel, Zach Hunter, and Kevin O’Bryant. "On the diameter of finite Sidon sets." Acta Mathematica Hungarica 175.1 (2025): 108-126. - [HZ26] Hou, Jianfeng, and Hongbin Zhao. "An Improved Upper Bound for Finite Sidon Sets via Vector-Valued Smoothing." arXiv:2607.01169 (2026). - [ET41] Erdos, Paul, and Pál Turán. "On a problem of Sidon in additive number theory, and on some related problems." J. London Math. Soc 16.4 (1941): 212-215. - [Li69] Lindström, Bernt. “A remark on B4-Sequences.” Journal of Combinatorial Theory, Series A 7 (1969): 276-277. - [CLZ01] Cohen, G.D., Litsyn, S., & Zémor, G. (2001). Binary B2-Sequences : A New Upper Bound. J. Comb. Theory A, 94, 152-155. - [BS85] Babai, László, and Vera T. Sós. "Sidon sets in groups and induced subgraphs of Cayley graphs." European Journal of Combinatorics 6.2 (1985): 101-114. doi:10.1016/S0195-6698(85)80001-9

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

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

Green31.green_31.lower

Open: stated without proof.

Can we improve the lower bound \(N^{1/2} + O(1)\), at least for infinitely many \(N\)?

theorem green_31.lower :
    -- Break the O(1) barrier
    Filter.Tendsto (fun N ↦ green_31.lower.answer N - Real.sqrt (N : ℝ)) atTop atTop ∧
    ∃ᶠ N in atTop, green_31.lower.answer N ≤ F N

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/31.lean, line 65.

Green31.green_31.variants.lower_eventually

Open: stated without proof.

Can we improve the lower bound \(N^{1/2} + O(1)\), for all sufficiently large \(N\)?

theorem green_31.variants.lower_eventually :
    -- Break the O(1) barrier
    Filter.Tendsto (fun N ↦ green_31.variants.lower_eventually.answer N - Real.sqrt (N : ℝ)) atTop
      atTop ∧
    ∀ᶠ N in atTop, green_31.variants.lower_eventually.answer N ≤ F N

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/31.lean, line 75.

Green31.green_31.upper

Open: stated without proof.

Can we improve the upper bound \(N^{1/2} + 0.94349 N^{1/4} + O(1)\) [HZ26], at least for infinitely many \(N\)?

theorem green_31.upper :
    (∃ᶠ N in atTop, F N ≤ green_31.upper.answer N) ∧
    ∃ c < (0.94349 : ℝ), ∃ C : ℝ, ∀ᶠ N in atTop, green_31.upper.answer N - Real.sqrt (N : ℝ) ≤ c *
      (N : ℝ) ^ (4⁻¹ : ℝ) + C

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/31.lean, line 89.

Green31.green_31.variants.upper_eventually

Open: stated without proof.

Can we improve the upper bound \(N^{1/2} + 0.94349 N^{1/4} + O(1)\) [HZ26], for all sufficiently large \(N\)?

theorem green_31.variants.upper_eventually :
    (∀ᶠ N in atTop, F N ≤ green_31.variants.upper_eventually.answer N) ∧
    ∃ c < (0.94349 : ℝ), ∃ C : ℝ, ∀ᶠ N in atTop, green_31.variants.upper_eventually.answer N -
      Real.sqrt (N : ℝ) ≤ c * (N : ℝ) ^ (4⁻¹ : ℝ) + C

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/31.lean, line 102.

Green31.green_31.variants.upper_li69

Solved: stated here without proof.

[Li69] proved \(F(n) \le n^{1/2} + n^{1/4} + O(1)\).

theorem green_31.variants.upper_li69 :
    ∃ C : ℝ, ∀ᶠ N in atTop, F N ≤ Real.sqrt (N : ℝ) + (N : ℝ) ^ (4⁻¹ : ℝ) + C

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/31.lean, line 110.

Green31.green_31.variants.upper_bfr23

Solved: stated here without proof.

[BFR23] obtained a small improvement, getting an upper bound of \(F(N) \le N^{1/2} + 0.998 N^{1/4}\) for large \(N\).

theorem green_31.variants.upper_bfr23 :
    ∀ᶠ N in atTop, F N ≤ Real.sqrt (N : ℝ) + (0.998 : ℝ) * (N : ℝ) ^ (4⁻¹ : ℝ)

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/31.lean, line 119.

Green31.green_31.variants.upper_cho25

Solved: stated here without proof.

The upper bound was further improved to \(N^{1/2} + 0.98183 N^{1/4} + O(1)\) [CHO25].

theorem green_31.variants.upper_cho25 :
    ∃ C : ℝ, ∀ᶠ N in atTop, F N ≤ Real.sqrt (N : ℝ) + (0.98183 : ℝ) * (N : ℝ) ^ (4⁻¹ : ℝ) + C

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/31.lean, line 125.

Green31.green_31.variants.upper_hz26

Solved: stated here without proof.

[HZ26] improved the upper bound to \(N^{1/2} + \gamma_0 N^{1/4} + O(1)\) with \(\gamma_0 = 0.94349\ldots < 0.9435\).

theorem green_31.variants.upper_hz26 :
    ∃ C : ℝ, ∀ᶠ N in atTop, F N ≤ Real.sqrt (N : ℝ) + (0.9435 : ℝ) * (N : ℝ) ^ (4⁻¹ : ℝ) + C

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/31.lean, line 134.

Green31.green_31.variants.zmod_p

Open: stated without proof.

It is not known whether or not there exists a Sidon subset of \(\mathbb{Z}/p\mathbb{Z}\) of size \((1 + o(1))\sqrt{p}\), for all \(p\) [Gr24].

theorem green_31.variants.zmod_p :
    ∃ S : (n : ℕ) → Finset (ZMod n),
    ∃ o : ℕ → ℝ,
      (o =o[atTop] fun _ : ℕ ↦ (1 : ℝ)) ∧
      (∀ p, p.Prime → IsSidon (S p : Set (ZMod p))) ∧
      (∀ p, p.Prime → ((S p).card : ℝ) = (1 + o p) * Real.sqrt (p : ℝ))

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/31.lean, line 143.

Green31.green_31.variants.abelian

Open: stated without proof.

It is not known whether, if \(G\) is an abelian group of size \(n\), there always exists a Sidon subset of \(G\) of size \(0.01\sqrt{n}\) [Gr24].

Green defines a Sidon set by \(r_A(n) \le 1\) [Gr24, Section 4]. Read literally, this forbids \(a + a = b + b\) with \(a \ne b\), and the answer is trivially negative: a Sidon subset of a group of exponent \(2\) then has at most one element. We use the definition of Babai and Sós [BS85] instead, see IsGroupSidon.

theorem green_31.variants.abelian :
    ∀ (G : Type) [AddCommGroup G] [Fintype G],
      ∃ S : Finset G, IsGroupSidon (S : Set G) ∧
        0.01 * Real.sqrt (Fintype.card G) ≤ S.card

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/31.lean, line 213.

Green31.green_31.variants.sidon_01n

Open: stated without proof.

Another very nice old problem is whether there is a Sidon subset of \(\{0, 1\}^n\) of size \(N^{0.51}\), where \(N = 2^n\) [Gr24].

theorem green_31.variants.sidon_01n :
    ∃ S : (n : ℕ) → Finset (𝔽₂ n),
      (∀ n, IsBinarySidon (S n : Set (𝔽₂ n))) ∧
      ∀ᶠ n in atTop, ((2 : ℝ) ^ n) ^ (0.51 : ℝ) ≤ (S n).card

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/31.lean, line 233.

Green31.green_31.variants.sidon_01n_clz01

Solved: stated here without proof.

The best-known upper bound for a Sidon subset of \(\{0, 1\}^n\) (\(N = 2^n\)) is \(N^{0.5753}\) [CLZ01].

theorem green_31.variants.sidon_01n_clz01 :
    ∃ C : ℝ, ∀ n, ∀ S : Finset (𝔽₂ n),
      IsBinarySidon (S : Set (𝔽₂ n)) →
        (S.card : ℝ) ≤ C * ((2 : ℝ) ^ n) ^ (0.5753 : ℝ)

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/31.lean, line 243.

Sources

• FormalConjectures/GreensOpenProblems/31.lean at 2055e5ad
• https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#section.7

LeanGreen31.green_31.lower · Green31.green_31.variants.lower_eventually · Green31.green_31.upper · Green31.green_31.variants.upper_eventually · Green31.green_31.variants.upper_li69 · Green31.green_31.variants.upper_bfr23 · Green31.green_31.variants.upper_cho25 · Green31.green_31.variants.upper_hz26 · Green31.green_31.variants.zmod_p · Green31.green_31.variants.abelian · Green31.green_31.variants.sidon_01n · Green31.green_31.variants.sidon_01n_clz01

TheoremGreen's Open Problem 32#

Reference: - [Gr24] Green, Ben. "100 open problems." (2024). - [Sh20] Shakan, George. "A Large Gap in a Dilate of a Set." SIAM Journal on Discrete Mathematics 34.4 (2020): 2553-2555.

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

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

Green32.green_32

Open: stated without proof.

Let \(p\) be a prime and let \(A \subset \mathbb{Z}/p\mathbb{Z}\) be a set of size \(\lfloor \sqrt{p} \rfloor\). Is there a dilate of \(A\) containing a gap of length \(100\sqrt{p}\)?

theorem green_32 :
    HasLargeGapDilate (fun p ↦ Real.sqrt p)

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/32.lean, line 86.

Green32.green_32.variants.sh20_general

Solved: stated here without proof.

[Sh20, Theorem 1] implies a gap of at least \(\lfloor 2p/|A| - 2 \rfloor\).

theorem green_32.variants.sh20_general :
    ∀ (p : ℕ), p.Prime → -- Theorem 1 is for any prime p, not just asymptotically
      ∀ A : Finset (ZMod p), 1 < A.card →
      ∃ c : (ZMod p)ˣ, HasGap (c • A) ⌊2 * (p : ℝ) / A.card - 2⌋₊

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/32.lean, line 92.

Green32.green_32.variants.sh20_sqrt

Solved: stated here without proof.

[Sh20] has used the polynomial method to show that this is true with 100 replaced by 2 [Gr24].

Note: More precisely [Sh20, Theorem 1] implies a gap of at least \(\lfloor 2p/|A| - 2 \rfloor\). For a set \(A\) of size \(\lfloor \sqrt{p} \rfloor\), this guarantees a gap of at least \(\lfloor 2\sqrt{p} \rfloor - 2\).

theorem green_32.variants.sh20_sqrt :
    ∀ᶠ p in atTop, p.Prime →
      ∀ A : Finset (ZMod p), A.card = ⌊Real.sqrt p⌋₊ →
      ∃ c : (ZMod p)ˣ, HasGap (c • A) (⌊2 * Real.sqrt p⌋₊ - 2)

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/32.lean, line 106.

Green32.green_32.variants.szemeredi_regime

Solved: stated here without proof.

In the regime \(\omega(p) \sim c p\), this is Szemerédi's theorem [Gr24].

theorem green_32.variants.szemeredi_regime :
    ∀ c, 0 < c ∧ c < 1 → ∀ ω : ℕ → ℝ, ω ~[atTop] (fun p ↦ c * p) →
      HasLargeGapDilate ω

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/32.lean, line 114.

Green32.green_32.variants.dirichlet_regime

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Green32_green_32_variants_dirichlet_regime.lean#L260.

In the regime \(\omega(p) \le c \log p\), this is basically Dirichlet's lower bound for the size of Bohr sets [Gr24].

The lower bound \(101 \le \omega(p)\) makes the set size \(\lfloor \omega(p) \rfloor\) exceed \(100\). With only \(100 < \omega(p)\), a function with \(100 < \omega(p) < 101\) asks for sets of size \(100\) with a gap of length \(p - 1\) in some dilate, which is impossible.

theorem green_32.variants.dirichlet_regime :
    ∃ c > 0, ∀ ω : ℕ → ℝ, (∀ᶠ p in atTop, 101 ≤ ω p ∧ ω p ≤ c * Real.log p) →
      HasLargeGapDilate ω

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/32.lean, line 129.

Green32.green_32.variants.log_regime

Open: stated without proof.

Even what happens in the regime \(\omega(p) \sim 10 \log p\) is unclear [Gr24].

theorem green_32.variants.log_regime :
    (∀ ω : ℕ → ℝ, ω ~[atTop] (fun p ↦ 10 * Real.log p) →
      HasLargeGapDilate ω)

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/32.lean, line 136.

Green32.green_32.variants.finite_field

Solved: stated here without proof.

Tom Sanders' finite field variant [Gr24]. If \(N = 2^n\) and \(A\) is a subset of size \(\lfloor \sqrt{N} \rfloor\), then \(A^c\) contains a coset of size at least \(100\sqrt{N}\) for sufficiently large \(n\).

theorem green_32.variants.finite_field :
    ∀ᶠ n in atTop,
      ∀ A : Finset (𝔽₂ n), A.card = ⌊Real.sqrt (2^n : ℝ)⌋₊ →
      HasCosetHole A ⌊100 * Real.sqrt (2^n : ℝ)⌋₊

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/32.lean, line 161.

Sources

• FormalConjectures/GreensOpenProblems/32.lean at 2055e5ad
• Green, Ben. "100 open problems." (2024).

LeanGreen32.green_32 · Green32.green_32.variants.sh20_general · Green32.green_32.variants.sh20_sqrt · Green32.green_32.variants.szemeredi_regime · Green32.green_32.variants.dirichlet_regime · Green32.green_32.variants.log_regime · Green32.green_32.variants.finite_field

TheoremBen Green's Open Problem 33#

References: - [Gr24] Ben Green's Open Problem 33 - [CaHa20] Caprace, Pierre-Emmanuel, and Pierre de la Harpe. "Groups with irreducibly unfaithful subsets for unitary representations." Confluentes Mathematici 12.1 (2020): 31-68. - [CrLe07] Croot, Ernie, and Vsevolod F. Lev. "Open problems in additive combinatorics." Additive combinatorics 43.207-233 (2007): 1.

Quoted from FormalConjectures/GreensOpenProblems/33.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.

Green33.green_33

Open: stated without proof.

Are there infinitely many \(q\) for which there is a set \(A \subset \mathbb{Z}/q\mathbb{Z}\), \(|A| = (\sqrt{2} + o(1))q^{1/2}\), with \(A + A = \mathbb{Z}/q\mathbb{Z}\)? [Gr24]

theorem green_33 :
    ∀ ε : ℝ, 0 < ε →
      ∃ᶠ q : ℕ+ in atTop,
        ∃ A : Finset (ZMod q),
          A + A = Finset.univ ∧
          |((A.card : ℝ) / Real.sqrt q - Real.sqrt 2)| < ε

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/33.lean, line 43.

Sources

• FormalConjectures/GreensOpenProblems/33.lean at 2055e5ad
• Ben Green's Open Problem 33

LeanGreen33.green_33

TheoremBen Green's Open Problem 35#

Estimate the infimum of the \(L^p\) norm of the self-convolution of a nonnegative integrable function supported on \([0,1]\) with total integral \(1\).

We model a function f : [0,1] → ℝ≥0 as a function f : ℝ → ℝ that is nonnegative, integrable, supported on [0,1], and has total integral 1.

References: - Ben Green's Open Problem 35 - Gr01 B. J. Green, The number of squares and \(B_h[g]\)-sets, Acta Arith. 100 (2001), no. 4, 365-390. - CS17 A. Cloninger and S. Steinerberger, On suprema of autoconvolutions with an application to Sidon sets, Proc. Amer. Math. Soc. 145 (2017), no. 8, 3191-3200. - MV10 M. Matolcsi and C. Vinuesa, Improved bounds on the supremum of autoconvolutions, J. Math. Anal. Appl. 372 (2010), 439-447. - AE25 A. Novikov et al., AlphaEvolve: A coding agent for scientific and algorithmic discovery, arXiv:2506.13131 (2025), Appendix B.1. - GGTW25 B. Georgiev, J. Gómez-Serrano, T. Tao and A. Z. Wagner, Mathematical exploration and discovery at scale, arXiv:2511.02864 (2025), Section 6.2.

The constants of [CS17], [MV10], [AE25] and [GGTW25] are stated for functions supported on \([-1/4, 1/4]\); rescaling to \([0, 1]\) halves them.

Quoted from FormalConjectures/GreensOpenProblems/35.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: 2 open, 5 solved and 1 textbook result.

Green35.green_35.lower

Open: stated without proof.

Lower bound for \(c(p)\) for \(1 < p \le \infty\), improving the known value \(\sqrt{4/7}\) at \(p = 2\) or the known value \(0.64\) at \(p = \infty\).

theorem green_35.lower :
    (∀ p, 1 < p → green_35.lower.answer p ≤ c p) ∧
      (ENNReal.ofReal (Real.sqrt (4 / 7)) < green_35.lower.answer 2 ∨
        0.64 < green_35.lower.answer ∞)

Category research open; AMS 26 Real functions, 28 Measure and integration, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/GreensOpenProblems/35.lean, line 70.

Green35.green_35.upper

Open: stated without proof.

Upper bound for \(c(p)\) for \(1 < p \le \infty\), improving the best-known value \(0.7516\) at \(p = \infty\).

theorem green_35.upper :
    (∀ p, 1 < p → c p ≤ green_35.upper.answer p) ∧ green_35.upper.answer ∞ < 0.7516

Category research open; AMS 26 Real functions, 28 Measure and integration, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/GreensOpenProblems/35.lean, line 81.

Green35.variants.c_2_lower

Solved: stated here without proof.

Lower bound for \(c(2)\) from Green's first paper ([Gr01]); the constant is sqrt(4/7) (about 0.7559).

theorem c_2_lower : ENNReal.ofReal (Real.sqrt (4 / 7)) ≤ c 2

Category research solved; AMS 26 Real functions, 28 Measure and integration, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/GreensOpenProblems/35.lean, line 90.

Green35.variants.c_inf_lower

Solved: stated here without proof.

Best-known lower bound for \(c(\infty)\) due to Cloninger and Steinerberger ([CS17]).

theorem c_inf_lower : 0.64 ≤ c ∞

Category research solved; AMS 26 Real functions, 28 Measure and integration, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/GreensOpenProblems/35.lean, line 95.

Green35.variants.c_inf_upper

Solved: stated here without proof.

Upper bound for \(c(\infty)\) due to Matolcsi and Vinuesa ([MV10]); their step function has autoconvolution supremum \(1.50972\ldots\), which rescales to \(0.75486\ldots\).

theorem c_inf_upper : c ∞ ≤ 0.7549

Category research solved; AMS 26 Real functions, 28 Measure and integration, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/GreensOpenProblems/35.lean, line 101.

Green35.variants.c_inf_upper_ae25

Solved: stated here without proof.

Upper bound for \(c(\infty)\) found by AlphaEvolve ([AE25]) and recorded in Green's 2025 update; the step function there has autoconvolution supremum at most \(1.5053\), which rescales to \(0.75265\).

theorem c_inf_upper_ae25 : c ∞ ≤ 0.75265

Category research solved; AMS 26 Real functions, 28 Measure and integration, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/GreensOpenProblems/35.lean, line 108.

Green35.variants.c_inf_upper_ggtw25

Solved: stated here without proof.

Best-known upper bound for \(c(\infty)\) ([GGTW25], §6.2): a step function with autoconvolution supremum at most \(1.5032\), which rescales to \(0.7516\).

theorem c_inf_upper_ggtw25 : c ∞ ≤ 0.7516

Category research solved; AMS 26 Real functions, 28 Measure and integration, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/GreensOpenProblems/35.lean, line 114.

Green35.variants.c_inf_lower_young

Textbook result, stated without proof.

A comparison bound from Young's inequality.

theorem c_inf_lower_young : (c 2) ^ 2 ≤ c ∞

Category textbook; AMS 26 Real functions, 28 Measure and integration, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/GreensOpenProblems/35.lean, line 119.

Sources

• FormalConjectures/GreensOpenProblems/35.lean at 2055e5ad
• Ben Green's Open Problem 35

LeanGreen35.green_35.lower · Green35.green_35.upper · Green35.variants.c_2_lower · Green35.variants.c_inf_lower · Green35.variants.c_inf_upper · Green35.variants.c_inf_upper_ae25 · Green35.variants.c_inf_upper_ggtw25 · Green35.variants.c_inf_lower_young

TheoremGreen's Open Problem 36#

References: * [Gr24] Green's Open Problems #36 * [CKS05] Cohn, H., Kleinberg, R., Szegedy, B., and Umans, C. "Group-theoretic Algorithms for Matrix Multiplication" (Problem 4.7)

Quoted from FormalConjectures/GreensOpenProblems/36.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.

Green36.green_36

Open: stated without proof.

Do the following exist, for arbitrarily large \(n\)? An abelian group \(H\) with \(|H| = n^{2+o(1)}\), together with subsets \(A_1, ..., A_n, B_1, ..., B_n\) satisfying \(|A_i||B_i| \ge n^{2-o(1)}\) and \(|A_i + B_i| = |A_i||B_i|\), such that the sets \(A_i + B_i\) are disjoint from the sets \(A_j + B_k\) (\(j \neq k\))?

NOTE: according to [CKS05, 4.1], the conditions should be \(A_i + B_j\) disjoint from \(A_j + B_k\) for \(i \neq k\). See green_36.variants.cks05.

theorem green_36 :
    ∀ ε > (0 : ℝ), ∃ᶠ n in atTop,
      ∃ (H : Type) (_ : AddCommGroup H) (_ : Finite H) (A B : Fin n → Finset H),
        (n : ℝ) ^ (2 - ε) ≤ Nat.card H ∧ Nat.card H ≤ (n : ℝ) ^ (2 + ε) ∧
        (∀ i, (n : ℝ) ^ (2 - ε) ≤ (A i).card * (B i).card) ∧
        Green36Property A B

Category research open; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/GreensOpenProblems/36.lean, line 60.

Green36.green_36.variants.cks05

Open: stated without proof.

Variant using the exact simultaneous double product property from [CKS05, 4.1].

theorem green_36.variants.cks05 :
    ∀ ε > (0 : ℝ), ∃ᶠ n in atTop,
      ∃ (H : Type) (_ : AddCommGroup H) (_ : Finite H) (A B : Fin n → Finset H),
        (n : ℝ) ^ (2 - ε) ≤ Nat.card H ∧ Nat.card H ≤ (n : ℝ) ^ (2 + ε) ∧
        (∀ i, (n : ℝ) ^ (2 - ε) ≤ (A i).card * (B i).card) ∧
        SimultaneousDoubleProduct A B

Category research open; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/GreensOpenProblems/36.lean, line 70.

Sources

• FormalConjectures/GreensOpenProblems/36.lean at 2055e5ad
• Green's Open Problems #36

LeanGreen36.green_36 · Green36.green_36.variants.cks05

TheoremBen Green's Open Problem 37#

What is the smallest subset of ℕ containing, for each d = 1, …, N, an arithmetic progression of length k with common difference d?

References: - Ben Green's Open Problem 37 - Green & Tao, The primes contain arbitrarily long arithmetic progressions (arXiv:math/0404188)

Quoted from FormalConjectures/GreensOpenProblems/37.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: 4 open. It also has 1 API statement, counted here but not shown.

Green37.green_37

Open: stated without proof.

Given a natural number N, what is the smallest size of a subset of ℕ that contains, for each d = 1, …, N, an arithmetic progression of length k with common difference d.

theorem green_37 (N k : ℕ) :
    IsLeast { m | ∃ A : Finset ℕ, A.card = m ∧ IsAPCover (A : Set ℕ) N k }
      (green_37.answer N k)

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/37.lean, line 53.

Green37.green_37_asymptotic

Open: stated without proof.

Asymptotic version: determine the asymptotic behavior of m(N, k) as N grows. The solver should determine a function f : ℕ → ℕ → ℝ such that, for each k, f k eventually equals (fun N ↦ (m N k : ℝ)).

theorem green_37_asymptotic (k : ℕ) :
    ∀ᶠ N in atTop, (m N k : ℝ) = green_37_asymptotic.answer k N

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/37.lean, line 66.

Green37.green_37_theta

Open: stated without proof.

Determine, for each k, the asymptotic equivalence class (theta) of m(N, k) as N grows.

theorem green_37_theta (k : ℕ) :
    (fun N ↦ (m N k : ℝ)) =Θ[atTop] green_37_theta.answer k

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/37.lean, line 74.

Green37.green_37_lower_bound

Open: stated without proof.

Writing F_k(N) for m(N, k), Green conjectures that F_k(N) ≫_k N^(1 - c_k) for some sequence c_k with c_k → 0 as k → ∞. The restriction to 0 < k excludes the degenerate case m(N, 0) = 0.

theorem green_37_lower_bound :
    ∃ c : ℕ → ℝ, Tendsto c atTop (nhds 0) ∧
      ∀ k, 0 < k → (fun N : ℕ ↦ (N : ℝ) ^ (1 - c k)) =O[atTop] fun N ↦ (m N k : ℝ)

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/37.lean, line 101.

Sources

• FormalConjectures/GreensOpenProblems/37.lean at 2055e5ad
• Ben Green's Open Problem 37

LeanGreen37.green_37 · Green37.green_37_asymptotic · Green37.green_37_theta · Green37.green_37_lower_bound

TheoremGreen's Open Problem 38#

References: - 100 open problems - [La79] Lovász, László. "On the Shannon capacity of a graph." IEEE Transactions on Information theory 25.1 (1979): 1-7. - [Po20] Polak, Sven. "New methods in coding theory: Error-correcting codes and the Shannon capacity." arXiv preprint arXiv:2005.02945 (2020). - [IRCR26] Itty, Nathaniel and Rosin, Christopher D. and Carstensen, Chase and Reichman, Daniel. "Improved lower bounds for the Shannon capacity of odd cycles." arXiv:2607.21517 (2026). - [Ga26] Gao, Yu. "A recursive construction improving the lower bound on the Shannon capacity of \(C_7\)." arXiv:2607.27869 (2026). - [BPZ26] Buys, Pjotr and Polak, Sven and Zuiddam, Jeroen. "Lean-verified lower bounds for the Shannon capacity of odd cycles." arXiv:2607.29681 (2026). Lean formalisation: https://github.com/spectra-research/shannon-capacity-lean

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

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

Green38.green_38.lower

Solved: stated here without proof.

Can we improve the lower bound? The answer sequence must be eventually nonnegative, since =O compares norms.

Yes. Itty, Rosin, Carstensen and Reichman [IRCR26] found a valid set of size \(134753\) in \(\mathbb{F}_7^{10}\) (an independent set in the tenth strong power of \(C_7\)). Taking products gives valid sets of size \(134753^{\lfloor n/10 \rfloor}\) in \(\mathbb{F}_7^n\), see green_38.variants.lower_itty_rosin_carstensen_reichman, so the growth rate is at least \(134753^{1/10} > 3.258020 > C_1\) (note \(134753 > 367^2 = 134689\)). Gao [Ga26] and then Buys, Polak and Zuiddam [BPZ26] improved the rate further, to \(3.258789\ldots\) and \(3.2588\ldots\) respectively; the latter is formalised in Lean. The exact growth rate remains open.

theorem green_38.lower :
    (∀ᶠ n in atTop, 0 ≤ green_38.lower.answer n) ∧ green_38.lower.answer ≤ᶠ[atTop]
      LargestAdmissibleCardinality ∧
    ∃ c > C₁, (fun n ↦ c ^ n) =O[atTop] green_38.lower.answer

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/38.lean, line 95.

Green38.green_38.upper

Open: stated without proof.

Can we improve the best upper bound? The base c must be positive, since =O compares norms.

theorem green_38.upper :
    LargestAdmissibleCardinality ≤ᶠ[atTop] green_38.upper.answer ∧
    ∃ c : ℝ, 0 < c ∧ c < C₂ ∧ green_38.upper.answer =O[atTop] (fun n ↦ c ^ n)

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/38.lean, line 106.

Green38.green_38.variants.best_lower

Solved: stated here without proof.

The lower bound \((C_1 - o(1))^n \leqslant |A|\) where \(C_1 = 367^{1/5} \approx 3.2578\), from a valid set of size \(367\) in \(\mathbb{F}_7^5\) [Po20, Section 9.1]. This was the best known bound when Green's list was written; it has since been improved, see green_38.lower.

theorem green_38.variants.best_lower :
    ∀ ε ∈ Set.Ioo (0 : ℝ) C₁, ∀ᶠ n in atTop, (C₁ - ε) ^ n ≤ LargestAdmissibleCardinality n

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/38.lean, line 116.

Green38.green_38.variants.lower_itty_rosin_carstensen_reichman

Solved: stated here without proof.

Itty, Rosin, Carstensen and Reichman [IRCR26] found a valid set of size \(134753\) in \(\mathbb{F}_7^{10}\). Products of copies of it, padded with zero coordinates, give \(134753^{\lfloor n/10 \rfloor} \leqslant |A|\) in \(\mathbb{F}_7^n\).

theorem green_38.variants.lower_itty_rosin_carstensen_reichman (n : ℕ) :
    (134753 : ℝ) ^ (n / 10) ≤ LargestAdmissibleCardinality n

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/38.lean, line 125.

Green38.green_38.variants.best_upper

Solved: stated here without proof.

The current best upper bound is \(|A| \leqslant (C_2 + o(1))^n\) where \(C_2 = \frac{7 \cos(\pi/7)}{1 + \cos(\pi/7)} \approx 3.3177\) [La79, Corollary 5].

theorem green_38.variants.best_upper :
    ∀ ε > 0, ∀ᶠ n in atTop, LargestAdmissibleCardinality n ≤ (C₂ + ε) ^ n

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/38.lean, line 132.

Sources

• FormalConjectures/GreensOpenProblems/38.lean at 2055e5ad
• 100 open problems

LeanGreen38.green_38.lower · Green38.green_38.upper · Green38.green_38.variants.best_lower · Green38.green_38.variants.lower_itty_rosin_carstensen_reichman · Green38.green_38.variants.best_upper

TheoremGreen's Open Problem 39#

References: - [Gr24] Green, Ben. "100 open problems." (2024). - [BJR11] Bollobás, Béla, Svante Janson, and Oliver Riordan. "On covering by translates of a set." Random Structures & Algorithms 38.1‐2 (2011): 33-67.

Quoted from FormalConjectures/GreensOpenProblems/39.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 open. It also has 8 test statements, counted here but not shown.

Green39.green_39

Open: stated without proof.

If \(A \subset \mathbb{Z}/p\mathbb{Z}\) is random, \(|A| = \sqrt{p}\), can we almost surely cover \(\mathbb{Z}/p\mathbb{Z}\) with \(100\sqrt{p}\) translates of \(A\)? [Gr24]

theorem green_39 :
    Tendsto
      (fun p : {q : ℕ // q.Prime} ↦
        let k := Nat.sqrt p
        let c := 100 * k
        (proportionCoverable p k c : ℝ))
      atTop (𝓝 1)

Category research open; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/39.lean, line 88.

Green39.green_39.variant_101

Open: stated without proof.

"I do not know how to answer this even with 100 replaced by 1.01." [Gr24]"

theorem green_39.variant_101 :
    Tendsto
      (fun p : {q : ℕ // q.Prime} ↦
        let k := Nat.sqrt p
        let c := ⌊1.01 * (k : ℝ)⌋₊
        (proportionCoverable p k c : ℝ))
      atTop (𝓝 1)

Category research open; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/39.lean, line 101.

Green39.green_39.variant_theta

Open: stated without proof.

Similar questions are interesting with \(\sqrt{p}\) replaced by \(p^\theta\) for any \(\theta \le 1/2\). [Gr24]

NOTE: using \(C p^\theta\) translates as stated makes the conjecture trivially false by the pigeonhole principle. Indeed for a set of size \(p^\theta\), we cover at most \(C p^{2\theta}\) elements, which is strictly less than \(p\) for \(\theta < 1/2\). We interpret the question as asking whether \(O(p^{1-\theta})\) translates suffice. This generalizes the main conjecture where \(\sqrt{p} = p^{1-1/2}\).

theorem green_39.variant_theta :
    ∀ (θ : ℝ), 0 < θ → θ ≤ 1/2 →
    ∃ C > 1, Tendsto
      (fun p : {q : ℕ // q.Prime} ↦
        let k := ⌊(p : ℝ) ^ θ⌋₊
        let c := ⌊C * (p : ℝ) ^ (1 - θ)⌋₊
        (proportionCoverable p k c : ℝ))
      atTop (𝓝 1)

Category research open; AMS 05 Combinatorics, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/39.lean, line 120.

Sources

• FormalConjectures/GreensOpenProblems/39.lean at 2055e5ad
• Green, Ben. "100 open problems." (2024).

LeanGreen39.green_39 · Green39.green_39.variant_101 · Green39.green_39.variant_theta

TheoremBen Green's Open Problem 40#

References: - [Gr24] Ben Green's Open Problem 40 - [Da90] Davydov, Alexander Abramovich. "Construction of linear covering codes." Problemy Peredachi Informatsii 26.4 (1990): 38-55. - [CHL97] Cohen, G., Honkala, I., Litsyn, S., & Lobstein, A. (1997). Covering codes (Vol. 54). Elsevier. - [St94] R. Struik, Covering codes, PhD Thesis, Eindhoven University of Technology, the Netherlands, 106 pp, 1994.

Quoted from FormalConjectures/GreensOpenProblems/40.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: 5 open and 5 solved.

Green40.green_40

Open: stated without proof.

Does \(f(r) \to \infty\)? [Gr24]

theorem green_40 : Tendsto f atTop (𝓝 ⊤)

Category research open; AMS 05 Combinatorics, 94 Information and communication, circuits. Declared in FormalConjectures/GreensOpenProblems/40.lean, line 64.

Green40.green_40.sanity_f_one

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Green40_green_40_sanity_f_one.lean#L216.

The only value known is \(f(1) = 1\), which follows from the existence of the Hamming code [Gr24].

theorem green_40.sanity_f_one : f 1 = 1

Category research solved; AMS 05 Combinatorics, 94 Information and communication, circuits. Declared in FormalConjectures/GreensOpenProblems/40.lean, line 70.

Green40.green_40.upper_bound

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Green40_green_40_upper_bound.lean#L245.

\(f(r) \le r^r / r! \sim e^r\) [Gr24].

theorem green_40.upper_bound (r : ℕ) : f r ≤ (r ^ r : ℝ≥0∞) / (r.factorial : ℝ≥0∞)

Category research solved; AMS 05 Combinatorics, 94 Information and communication, circuits. Declared in FormalConjectures/GreensOpenProblems/40.lean, line 76.

Green40.green_40.f_eq_one_for_all

Open: stated without proof.

The possibility that f(r) = 1 for all r has not been ruled out [Gr24]

theorem green_40.f_eq_one_for_all : ∀ r, f r = 1

Category research open; AMS 05 Combinatorics, 94 Information and communication, circuits. Declared in FormalConjectures/GreensOpenProblems/40.lean, line 81.

Green40.green_40.f_two_eq_one

Open: stated without proof.

It is not known whether f(2) = 1 [Gr24]

theorem green_40.f_two_eq_one : f 2 = 1

Category research open; AMS 05 Combinatorics, 94 Information and communication, circuits. Declared in FormalConjectures/GreensOpenProblems/40.lean, line 86.

Green40.green_40.upper_bound_f_two

Solved: stated here without proof.

The best-known upper bound for \(f(2)\) is \(1.4238\) [CHL97].

theorem green_40.upper_bound_f_two : f 2 ≤ (1.4238 : ℝ≥0∞)

Category research solved; AMS 05 Combinatorics, 94 Information and communication, circuits. Declared in FormalConjectures/GreensOpenProblems/40.lean, line 91.

Green40.green_40.variants.arbitrary_subsets

Open: stated without proof.

Does \(\tilde{f}(r) \to \infty\)? [Gr24]

theorem green_40.variants.arbitrary_subsets : Tendsto f_tilde atTop (𝓝 ⊤)

Category research open; AMS 05 Combinatorics, 94 Information and communication, circuits. Declared in FormalConjectures/GreensOpenProblems/40.lean, line 113.

Green40.green_40.variants.arbitrary_subsets_sanity_f_tilde_two

Solved: stated here without proof.

It is known that \(\tilde{f}(2) = 1\) [St94].

theorem green_40.variants.arbitrary_subsets_sanity_f_tilde_two : f_tilde 2 = 1

Category research solved; AMS 05 Combinatorics, 94 Information and communication, circuits. Declared in FormalConjectures/GreensOpenProblems/40.lean, line 118.

Green40.green_40.f_tilde_le_f

Proved here.

We evidently have \(\tilde{f}(r) \le f(r)\) [Gr24].

theorem green_40.f_tilde_le_f (r : ℕ) : f_tilde r ≤ f r

Category research solved; AMS 05 Combinatorics, 94 Information and communication, circuits. Declared in FormalConjectures/GreensOpenProblems/40.lean, line 123.

Green40.green_40.variants.all_n

Open: stated without proof.

Does \(f_{\text{all}}(r) \to \infty\)? [Gr24]

The target filter is 𝓝 ⊤, as in green_40 and green_40.variants.arbitrary_subsets. On ℝ≥0∞, atTop is the principal ultrafilter at ⊤, so Tendsto f_all atTop atTop would say that f_all r = ⊤ for all large r rather than that f_all r → ∞.

theorem green_40.variants.all_n : Tendsto f_all atTop (𝓝 ⊤)

Category research open; AMS 05 Combinatorics, 94 Information and communication, circuits. Declared in FormalConjectures/GreensOpenProblems/40.lean, line 161.

Sources

• FormalConjectures/GreensOpenProblems/40.lean at 2055e5ad
• Ben Green's Open Problem 40

LeanGreen40.green_40 · Green40.green_40.sanity_f_one · Green40.green_40.upper_bound · Green40.green_40.f_eq_one_for_all · Green40.green_40.f_two_eq_one · Green40.green_40.upper_bound_f_two · Green40.green_40.variants.arbitrary_subsets · Green40.green_40.variants.arbitrary_subsets_sanity_f_tilde_two · Green40.green_40.f_tilde_le_f · Green40.green_40.variants.all_n

TheoremBen Green's Open Problem 41#

References - [Gr24] Ben Green's Open Problem 41 - [Ma15] Manners, Freddie. "A solution to the pyjama problem." Inventiones mathematicae 202.1 (2015): 239-270. - [KrLe25] Kravitz, Noah, and James Leng. "Quantitative pyjama." arXiv preprint arXiv:2510.17744 (2025).

Quoted from FormalConjectures/GreensOpenProblems/41.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: 3 open and 2 solved.

Green41.minCopies_set_nonempty

Solved: stated here without proof.

[Ma15] proved that for any \(\varepsilon > 0\), finitely many rotations of the pyjama set of width \(\varepsilon\) cover the plane. This implies that the set we are taking the infimum over in minCopies is non-empty.

theorem minCopies_set_nonempty (ε : ℝ) (hε : 0 < ε) :
    (coveringCopies ε).Nonempty

Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/41.lean, line 58.

Green41.green_41

Open: stated without proof.

How many rotated (about the origin) copies of the 'pyjama set' \(\\{(x, y) \in \mathbb{R}^2 : \text{dist}(x, \mathbb{Z}) \leq \varepsilon\\}\) are needed to cover \(\mathbb{R}^2\)?

That is, determine the minimal number of rotations as a function of \(\varepsilon > 0\).

theorem green_41 : ∀ ε > 0, minCopies ε = green_41.answer ε

Category research open; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/41.lean, line 72.

Green41.green_41.variants.double_exponential_bound

Open: stated without proof.

Can the triple-exponential bound of [KrLe25] be improved by one exponential? That is, do \(\exp\exp(\varepsilon^{-C})\) rotations suffice for some \(C\) and all sufficiently small \(\varepsilon > 0\)? [KrLe25, Section 8.1] discusses where the three exponentials are lost and which of them one might hope to save.

theorem green_41.variants.double_exponential_bound :
    ∃ C : ℝ, ∃ ε₀ > 0, ∀ ε ∈ Ioc 0 ε₀, (minCopies ε : ℝ) ≤ Real.exp (Real.exp (ε ^ (-C)))

Category research open; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/41.lean, line 82.

Green41.green_41.variants.polynomial_bound

Open: stated without proof.

Is \(\varepsilon^{-C}\) rotations enough?

theorem green_41.variants.polynomial_bound :
    ∃ C : ℝ, ∃ ε₀ > 0, ∀ ε ∈ Ioc 0 ε₀, (minCopies ε : ℝ) ≤ ε ^ (-C)

Category research open; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/41.lean, line 88.

Green41.green_41.variants.kravitz_leng

Solved: stated here without proof.

[KrLe25] have established the first quantitative bound, showing via an analysis of [Ma15]'s method that \(\exp\exp\exp(\varepsilon^{-C})\) rotations suffice.

theorem green_41.variants.kravitz_leng :
    ∃ C : ℝ, ∃ ε₀ > 0, ∀ ε ∈ Ioc 0 ε₀, (minCopies ε : ℝ) ≤ Real.exp (Real.exp (Real.exp (ε ^ (-C))))

Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/41.lean, line 97.

Sources

• FormalConjectures/GreensOpenProblems/41.lean at 2055e5ad
• Ben Green's Open Problem 41

LeanGreen41.minCopies_set_nonempty · Green41.green_41 · Green41.green_41.variants.double_exponential_bound · Green41.green_41.variants.polynomial_bound · Green41.green_41.variants.kravitz_leng

TheoremGreen's Open Problem 42#

References: - [Gr24] Green, Ben. "100 open problems." (2024). - [CoEl03] Cohn, Henry, and Noam Elkies. "New upper bounds on sphere packings I." Annals of Mathematics (2003): 689-714. - [Vi17] Viazovska, Maryna S. "The sphere packing problem in dimension 8." Annals of mathematics (2017): 991-1015. - [CKM17] Cohn, H., Kumar, A., Miller, S., Radchenko, D., & Viazovska, M. (2017). The sphere packing problem in dimension 24. Annals of mathematics, 185(3), 1017-1033. - [Sa21] Sardari, Naser Talebizadeh. "Higher Fourier interpolation on the plane." arXiv preprint arXiv:2102.08753 (2021). - [OAI26a] OpenAI, A sharp Fourier certificate for planar circle packing. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-sharp-Fourier-certificate-for-planar-circle-packing-September-23-2026/paper.pdf

Quoted from FormalConjectures/GreensOpenProblems/42.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: 4 solved.

Green42.green_42

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

Can the Cohn-Elkies scheme be used to prove the optimal bound for circle-packings in 2 dimensions?

The answer is "yes". This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof, which constructs a radial Schwartz certificate normalised to minimum distance \(1\).

theorem green_42 :
    CohnElkiesOptimal 2 (Real.sqrt 3 / 6)

Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/42.lean, line 99.

Green42.green_42.variants.dimension_one

Solved: stated here without proof.

[CoEl03] proved this when \(d = 1\).

theorem green_42.variants.dimension_one :
    CohnElkiesOptimal 1 (1 / 2)

Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/42.lean, line 105.

Green42.green_42.variants.dimension_eight

Solved: stated here; a Lean proof is at https://github.com/math-inc/Sphere-Packing-Lean/blob/main/SpherePacking/Dim8/MainTheorem.lean.

[Vi17] established the case \(d = 8\).

theorem green_42.variants.dimension_eight :
    CohnElkiesOptimal 8 (1 / 16)

Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/42.lean, line 112.

Green42.green_42.variants.dimension_twenty_four

Solved: stated here; a Lean proof is at https://github.com/math-inc/Sphere-Packing-Lean/blob/main/SpherePacking/Dim24/MainTheorem.lean.

In [CKM17], [Vi17] was adapted to \(d = 24\).

theorem green_42.variants.dimension_twenty_four :
    CohnElkiesOptimal 24 1

Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/42.lean, line 119.

Sources

• FormalConjectures/GreensOpenProblems/42.lean at 2055e5ad
• Green, Ben. "100 open problems." (2024).

LeanGreen42.green_42 · Green42.green_42.variants.dimension_one · Green42.green_42.variants.dimension_eight · Green42.green_42.variants.dimension_twenty_four

TheoremBen Green's Open Problem 43#

References: - [Gr24] Ben Green's Open Problem 43 - [Gr18] Green, Ben. "A note on multiplicative functions on progressions to large moduli." Proc. Roy. Soc. Edinburgh Sect. A 148 (2018), no. 1, 63–77. (Problem 43 is formulated here, [Gr18, Section 4].) - [AP92] Alon, Noga, and Yuval Peres. "Uniform dilations." Geometric and Functional Analysis 2 (1992), no. 1, 1–28. (Source of the favourite variant in [Gr24, Comments to Problem 43].)

Quoted from FormalConjectures/GreensOpenProblems/43.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: 5 open and 1 solved. It also has 3 test statements, counted here but not shown.

Green43.green_43

Open: stated without proof.

Let \(N\) be a large integer. For each prime \(p\) with \(N^{0.51} \leq p < 2N^{0.51}\), pick some residue \(a(p) \in \mathbb{Z}/p\mathbb{Z}\). Is it true that

\[\#\{n \in [N] : n \equiv a(p) \pmod{p} \text{ for some } p\} \gg N^{1-o(1)}?\]

theorem green_43 : SievedLowerBoundExp (0.51 : ℝ)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/43.lean, line 69.

Green43.green_43.variants.alon_peres

Open: stated without proof.

[Gr24, Comments to Problem 43; AP92] One of Green's favourite related conjectures: if A ⊆ ℤ/pℤ is a set of size ⌊p/2⌋, does some dilation n A (n an integer) have no gaps of length more than p^{0.49}?

The question is asymptotic, so it is stated for all sufficiently large primes p (see the large-prime discussion in [AP92, §2]); for small primes it fails trivially, e.g. p = 3, A = {0}.

theorem green_43.variants.alon_peres :
    ∀ᶠ p : ℕ in atTop, p.Prime → ∀ A : Finset (ZMod p), A.card = p / 2 →
    ∃ n : ZMod p, ∀ L : ℕ, (p : ℝ) ^ (0.49 : ℝ) < (L : ℝ) → ¬ HasGap (Dilate n A) L

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/43.lean, line 140.

Green43.green_43.variants.range_N051_N052

Open: stated without proof.

[Gr24, Comments to Problem 43] A minor variant of Problem 43: the same question but with p ranging over N^{0.51} ≤ p < N^{0.52}. Obtaining the lower bound N^{1-o(1)} here is no harder than Problem 43, but is not known.

theorem green_43.variants.range_N051_N052 :
    SievedLowerBound (fun N => (N : ℝ) ^ (0.51 : ℝ)) (fun N => (N : ℝ) ^ (0.52 : ℝ))

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/43.lean, line 151.

Green43.green_43.variants.range_N051_N052_linear

Open: stated without proof.

[Gr24, Comments to Problem 43] For the range N^{0.51} ≤ p < N^{0.52} there may even be a linear lower bound c N.

theorem green_43.variants.range_N051_N052_linear :
    ∃ c : ℝ, 0 < c ∧ ∀ᶠ N : ℕ in atTop, ∀ a : ℕ → ℤ,
      c * N ≤ sievedCard N a ((N : ℝ) ^ (0.51 : ℝ)) ((N : ℝ) ^ (0.52 : ℝ))

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/43.lean, line 160.

Green43.green_43.variants.general_exponent

Open: stated without proof.

[Gr24, Comments to Problem 43] One can replace the exponent 0.51 by any other exponent α: does the lower bound N^{1-o(1)} hold for sieving primes in [N^α, 2 N^α) for every exponent 0 < α < 1? Problem 43 is the case α = 0.51; the regime α < 1/2 is the solved special case green_43.variants.general_exponent_lt_half, while progress for α ≈ 1 would imply Kakeya.

theorem green_43.variants.general_exponent :
    ∀ α : ℝ, 0 < α → α < 1 → SievedLowerBoundExp α

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/43.lean, line 173.

Green43.green_43.variants.general_exponent_lt_half

Solved: stated here without proof.

[Gr24, Comments to Problem 43] For exponents α < 1/2 the lower bound N^{1-o(1)} is straightforward (by an inclusion–exclusion or Cauchy–Schwarz argument). This is the solved special case of green_43.variants.general_exponent.

theorem green_43.variants.general_exponent_lt_half :
    ∀ α : ℝ, 0 < α → α < 1 / 2 → SievedLowerBoundExp α

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/43.lean, line 183.

Sources

• FormalConjectures/GreensOpenProblems/43.lean at 2055e5ad
• Ben Green's Open Problem 43

LeanGreen43.green_43 · Green43.green_43.variants.alon_peres · Green43.green_43.variants.range_N051_N052 · Green43.green_43.variants.range_N051_N052_linear · Green43.green_43.variants.general_exponent · Green43.green_43.variants.general_exponent_lt_half

TheoremGreen's Open Problem 44#

References: - [Gr24] Ben Green's 100 Open Problems - [Er80] Erdős, Paul. "A survey of problems in combinatorial number theory." Annals of Discrete Mathematics 6 (1980): 89-115.

Quoted from FormalConjectures/GreensOpenProblems/44.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.

Green44.green_44

Open: stated without proof.

Sieve \([N]\) by removing half the residue classes mod \(p_i\), for primes \(2 \leqslant p_1 < p_2 < \dots < p_{1000} < N^{9/10}\). Does the remaining set have size at most \(\frac{1}{10} N\)?

We interpret "half the residue classes" as \(\lfloor p_i / 2 \rfloor\).

theorem green_44 :
    ∀ (N : ℕ) (p : Fin 1000 → ℕ) (A : (i : Fin 1000) → Finset (ZMod (p i))),
      let remaining := (Finset.Icc 1 N).filter (fun x => ∀ i, (x : ZMod (p i)) ∉ A i)
      (∀ i, (p i).Prime) →
      StrictMono p →
      (p 999) ^ 10 < N ^ 9 →
      (∀ i, (A i).card = (p i) / 2) →
      10 * remaining.card ≤ N

Category research open; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/44.lean, line 43.

Green44.green_44.variants.less_than_sqrt

Solved: stated here without proof.

The answer is affirmative if the primes are all less than \(N^{1/2}\), by the large sieve. [Gr24]

theorem green_44.variants.less_than_sqrt :
    ∀ (N : ℕ) (p : Fin 1000 → ℕ) (A : (i : Fin 1000) → Finset (ZMod (p i))),
      let remaining := (Finset.Icc 1 N).filter (fun x => ∀ i, (x : ZMod (p i)) ∉ A i)
      (∀ i, (p i).Prime) →
      StrictMono p →
      (p 999) ^ 2 < N →
      (∀ i, (A i).card = (p i) / 2) →
      10 * remaining.card ≤ N

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/44.lean, line 55.

Sources

• FormalConjectures/GreensOpenProblems/44.lean at 2055e5ad
• Ben Green's 100 Open Problems

LeanGreen44.green_44 · Green44.green_44.variants.less_than_sqrt

TheoremBen Green's Open Problem 45#

Can we pick residue classes \(a_p \pmod{p}\), one for each prime \(p \leq N\), such that every integer \(\leq N\) lies in at least 10 of them?

References: - Ben Green's Open Problem 45 - erdosproblems.com/689

The version of this problem with \(10\) replaced by \(2\) is Erdos689.erdos_689 in FormalConjectures.ErdosProblems.«689».

Quoted from FormalConjectures/GreensOpenProblems/45.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.

Green45.green_45

Open: stated without proof.

Can we pick residue classes \(a_p \pmod{p}\), one for each prime \(p \leq N\), such that every integer \(\leq N\) lies in at least \(10\) of them?

Erdős remarks that he does not know how to answer it with \(10\) replaced by \(2\); this is Erdos689.erdos_689.

theorem green_45 :
    ∀ᶠ N in .atTop, ∃ a : ℕ → ℕ, ∀ m ∈ Finset.Icc 1 N,
      10 ≤ (Finset.Icc 1 N |>.filter fun p => p.Prime ∧ a p ≡ m [MOD p]).card

Category research open; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/45.lean, line 47.

Sources

• FormalConjectures/GreensOpenProblems/45.lean at 2055e5ad
• Ben Green's Open Problem 45

LeanGreen45.green_45

TheoremBen Green's Open Problem 46#

What is the largest \(y\) for which one may cover the interval \([y]\) by residue classes \(a_p \pmod{p}\), one for each prime \(p \leq x\)?

References: - [Gr24] Ben Green's Open Problem 46 - [FGK18] Ford, K., Green, B., Konyagin, S., Maynard, J., & Tao, T. (2018). Long gaps between primes. Journal of the American Mathematical Society, 31(1), 65-105. - [Iw78] Iwaniec, Henryk. "On the problem of Jacobsthal." Demonstratio Mathematica 11.1 (1978): 225-232. - [OAI26a] OpenAI, A quadratic bound for Jacobsthal's function. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-quadratic-bound-for-Jacobsthals-function-September-25-2026/paper.pdf - [Ra38] Rankin, R. A., The difference between consecutive prime numbers. J. London Math. Soc. (1938), 242--247.

This is the same problem as Erdős Problem 687.

Quoted from FormalConjectures/GreensOpenProblems/46.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.

Green46.green_46.improve_lower

Open: stated without proof.

We conjecture that the best-known lower bound can be improved.

theorem green_46.improve_lower :
    (bestLower =o[atTop] green_46.improve_lower.answer) ∧ (green_46.improve_lower.answer ≪ maxY)

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

Green46.green_46.improve_upper

Solved: stated here; a Lean proof is at https://github.com/30k30/scholia/blob/b072c89c3edac06521868e32cc15b2bc91bd8533/erdos-687/glue/JacobsthalTo687.lean#L319.

We conjecture that the best-known upper bound can be improved.

Yes. OpenAI [OAI26a] proved \(h(k) \ll k^2 / (\log\log 3k)^2\) for Jacobsthal's function \(h\) (Erdős Problem 970). By the Chinese remainder theorem \(\mathrm{maxY}(x) < h(\pi(x))\), which gives \(\mathrm{maxY}(x) \ll (x+1)^2 / (\log\log 3(x+1))^2 = o(x^2)\). Whether \(y \ll x^{1+o(1)}\) remains open, see green_46.improve_upper_conjectured.

theorem green_46.improve_upper :
    (green_46.improve_upper.answer =o[atTop] bestUpper) ∧ (maxY ≪ green_46.improve_upper.answer)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/46.lean, line 83.

Green46.green_46.improve_upper_conjectured

Open: stated without proof.

It seems very likely that we must have \(y \ll x^{1+o(1)}\) [Gr24].

theorem green_46.improve_upper_conjectured :
    ∃ o : ℕ → ℝ, (o =o[atTop] fun _ : ℕ ↦ (1 : ℝ)) ∧
      maxY ≪ fun x ↦ (x : ℝ) ^ (1 + o x)

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

Green46.green_46.variants.lower

Solved: stated here without proof.

Best known lower bound: \(y \gg x \frac{\log x \log \log \log x}{\log \log x}\) [FGK18].

theorem green_46.variants.lower :
    bestLower ≪ maxY

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/46.lean, line 97.

Green46.green_46.variants.upper

Solved: stated here without proof.

Best known upper bound: \(y \ll x^2\) [Iw78].

theorem green_46.variants.upper :
    maxY ≪ bestUpper

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/46.lean, line 103.

Sources

• FormalConjectures/GreensOpenProblems/46.lean at 2055e5ad
• Ben Green's Open Problem 46

LeanGreen46.green_46.improve_lower · Green46.green_46.improve_upper · Green46.green_46.improve_upper_conjectured · Green46.green_46.variants.lower · Green46.green_46.variants.upper

TheoremGreen's Open Problem 47#

References: - [Gr24] Ben Green's 100 Open Problems - [GH14] Green, Ben, and Adam J. Harper. "Inverse questions for the large sieve." Geometric and Functional Analysis 24.4 (2014): 1167-1203. - [HV09] Helfgott, Harald Andrés, and Akshay Venkatesh. "How small must ill-distributed sets be." Analytic number theory 2 (2009): 224-234. - [Wa12] Walsh, Miguel N. "The inverse sieve problem in high dimensions." (2012): 2001-2022. - [Wa14] Walsh, Miguel N. "The algebraicity of ill-distributed sets." Geometric and Functional Analysis 24.3 (2014): 959-967.

Quoted from FormalConjectures/GreensOpenProblems/47.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.

Green47.green_47

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/green-47-exact-containment-counterexample/blob/d6912b65cd04463ca81d2e7dfb52367718a3e3b2/lean/Green47ExactContainmentFC.lean#L19-L25.

Suppose that a large sieve process leaves a set of quadratic size. Is that set quadratic?

The following very particular instance is probably the simplest [Gr24]: Suppose that \(A \subset \mathbb{N}\) is a set with the property that \(|A \pmod p| \leqslant \frac{1}{2}(p + 1)\) for all sufficiently large \(p\). Is it true that either \(|A \cap [X]| \ll X^{1/2} / \log^{100} X\), or \(A\) is contained in the image of \(\mathbb{Z}\) under a quadratic map \(\phi : \mathbb{Q} \to \mathbb{Q}\)?

theorem green_47 :
    ¬ ∀ A : Set ℕ,
      (∀ᶠ p in atTop, Nat.Prime p → Set.ncard (Set.image (fun a : ℕ => (a : ZMod p)) A) ≤ (p + 1) / 2) →
      ((fun X : ℕ => ((A ∩ Set.Iic X).ncard : ℝ)) ≪ (fun X : ℕ => Real.sqrt (X : ℝ) / (Real.log (X : ℝ)) ^ 100))
      ∨ (∃ P : Polynomial ℚ, P.degree = 2 ∧ ∀ a ∈ A, ∃ z : ℤ, (a : ℚ) = P.eval (z : ℚ))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/47.lean, line 53.

Green47.green_47.variants.finite_exceptions

Open: stated without proof.

In Green and Harper's formulation [GH14, Conjecture 1.7], the quadratic containment is allowed to fail on a finite subset of \(A\).

theorem green_47.variants.finite_exceptions :
    ∀ A : Set ℕ,
      (∀ᶠ p in atTop, Nat.Prime p → Set.ncard (Set.image (fun a : ℕ => (a : ZMod p)) A) ≤ (p + 1) / 2) →
      ((fun X : ℕ => ((A ∩ Set.Iic X).ncard : ℝ)) ≪ (fun X : ℕ => Real.sqrt (X : ℝ) / (Real.log (X : ℝ)) ^ 100))
      ∨ (∃ P : Polynomial ℚ, P.degree = 2 ∧ {a ∈ A | ¬∃ z : ℤ, (a : ℚ) = P.eval (z : ℚ)}.Finite)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/47.lean, line 63.

Sources

• FormalConjectures/GreensOpenProblems/47.lean at 2055e5ad
• Ben Green's 100 Open Problems

LeanGreen47.green_47 · Green47.green_47.variants.finite_exceptions

TheoremGreen's Open Problem 49#

Also known as the Marton's conjecture or the Polynomial Freiman-Ruzsa conjecture (PFR).

References: - [Gr24] Ben Green's 100 Open Problems - [Aa19] Aaronson, James. "A counterexample to a strong variant of the Polynomial Freiman-Ruzsa conjecture." arXiv preprint arXiv:1902.00353 (2019). - [Fa00] I. Farah, Approximate homomorphisms. II. Group homomorphisms, Combinatorica 20 (2000), no. 1, 47–60. - [GGM25] W. T. Gowers, B. J. Green, F. Manners and T. C. Tao, On a conjecture of Marton, Ann. of Math. (2) 201 (2025), no. 2, 515–549. - [Gr05] B. J. Green, Finite field models in additive combinatorics, Surveys in combinatorics 2005, 1–27, London Math. Soc. Lecture Note Ser., 327, Cambridge Univ. Press, Cambridge, 2005. - [GrTa10] B. J. Green and T. C. Tao An equivalence between inverse sumset theorems and inverse conjectures for the U3 norm, Math. Proc. Cambridge Philos. Soc. 149 (2010), no. 1, 1–19. - [Lo12] S. Lovett, Equivalence of polynomial conjectures in additive combinatorics, Combinatorica 32 (2012), no. 5, 607–618. - [LoRe17] S. Lovett and O. Regev, A counterexample to a strong variant of the Polynomial Freiman Ruzsa conjecture in Euclidean space, Discrete Anal.(2017), Paper No. 8, 6 pp. - [Ma19] F. R. W. M. Manners, Formulations of the PFR conjecture over Z, Math. Proc. Cambridge Philos. Soc. 166 (2019), no. 2, 243–245. - [Sa12] T. Sanders, On the Bogolyubov-Ruzsa lemma, Anal. PDE 5 (2012), no. 3, 627–655. - [Ta08] T. C. Tao, A counterexample to a strong polynomial Freiman-Ruzsa conjecture, blog post November 2008, available at http://tinyurl.com/36j6hyxv.

Quoted from FormalConjectures/GreensOpenProblems/49.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.

Green49.green_49

Solved: stated here without proof.

Suppose that \(A \subset \mathbb{F}_2^n\) is a set with \(|A + A| \leq K|A|\). Is it true that \(A\) is covered by \(K^{O(1)}\) translates of a subspace of size \(\leq |A|\)?

Solved by [GGM25], with at most \(2K^{12}\) translates. The factor \(2\) cannot be omitted: for \(A = \mathbb{F}_2^n \setminus \{0\}\) one has \(K = 2^n / (2^n - 1)\), so \(K^C \to 1\) as \(n \to \infty\), while every subspace of size at most \(|A|\) is proper and two translates are needed.

theorem green_49 :
    ∃ C > 0,
      ∀ n (A : Finset (𝔽₂ n)), A.Nonempty →
      ∀ K ≥ (1 : ℝ), (#(A + A) : ℝ) ≤ K * #A →
        ∃ (W : Submodule (ZMod 2) (𝔽₂ n)) (T : Finset (𝔽₂ n)),
          Nat.card W ≤ #A ∧
          (#T : ℝ) ≤ 2 * K ^ C ∧
          (A : Set (𝔽₂ n)) ⊆ T + W

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/49.lean, line 55.

Sources

• FormalConjectures/GreensOpenProblems/49.lean at 2055e5ad
• Ben Green's 100 Open Problems

LeanGreen49.green_49

TheoremBen Green's Open Problem 50#

Suppose that \(A \subset \mathbb{F}_2^n\) is a set of density \(\alpha\). Does \(10A\) contain a coset of some subspace of dimension at least \(n - O(\log(1/\alpha))\)?

Here \(kA\) denotes the \(k\)-fold iterated sumset, i.e., the set of all sums of \(k\) elements from \(A\) (with repetition allowed). In Mathlib, this is denoted k • A using pointwise scalar multiplication on sets.

Reference: Ben Green's Open Problem 50

Quoted from FormalConjectures/GreensOpenProblems/50.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.

Green50.green_50

Open: stated without proof.

Let \(A \subset \mathbb{F}_2^n\) be a set of density \(\alpha > 0\). Does \(10A\) contain a coset of some subspace of dimension at least \(n - O(\log(1/\alpha))\)?

More precisely: does there exist an absolute constant \(C > 0\) such that for all \(n \geq 1\) and all nonempty \(A \subseteq \mathbb{F}_2^n\) with density \(\alpha > 0\), the sumset \(10A\) contains a coset of some subspace of dimension at least \(n - C \log_2(1/\alpha)\)?

The sumset \(10A\) is defined as \(\{a_1 + a_2 + \cdots + a_{10} : a_i \in A\}\), using the pointwise scalar multiplication notation 10 • A where • denotes the iterated addition of a set.

Note: We model \(\mathbb{F}_2^n\) as Fin n → ZMod 2, which is an \(n\)-dimensional vector space over \(\mathbb{F}_2\).

theorem green_50 :
    ∃ C > (0 : ℝ), ∀ n : ℕ, ∀ A : Finset (𝔽₂ n),
    A.Nonempty →
    let α : ℝ := A.dens
    ∃ (W : Submodule (ZMod 2) (𝔽₂ n)) (v : 𝔽₂ n),
      v +ᵥ (W : Set (𝔽₂ n)) ⊆ ↑(10 • A) ∧
      (n : ℝ) - C * Real.logb 2 (1 / α) ≤ Module.finrank (ZMod 2) W

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/50.lean, line 54.

Sources

• FormalConjectures/GreensOpenProblems/50.lean at 2055e5ad
• https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#section.6

LeanGreen50.green_50

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.