Green's Open Problem 51 to Green's Open Problem 85

TheoremGreen's Open Problem 51#

References: - [Gr24] Green's Open Problems - [Gr13] B. J. Green, Restriction and Kakeya phenomena, notes from a 2003 course. Available at http://people.maths.ox.ac.uk/greenbj/papers/rkp.pdf - [Sa11] Sanders, Tom. "Green's sumset problem at density one half." Acta Arithmetica 146.1 (2011): 91-101. - [Gr02] Green, Ben. "Arithmetic progressions in sumsets." Geometric & Functional Analysis GAFA 12.3 (2002): 584-597. - [Ruz91] Ruzsa, Imre Z. "Arithmetic progressions in sumsets." Acta Arithmetica 60.2 (1991): 191-202.

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

The file states 6 research or textbook statements: 2 open and 4 solved.

Green51.green_51

Open: stated without proof.

Suppose that \(A \subset \mathbb{F}_2^n\) is a set of density \(\alpha\). What is the largest size of coset guaranteed to be contained in \(2A\)?

We phrase this by asking for the exact function \(F(\alpha, n)\) giving the maximum dimension of a guaranteed coset.

theorem green_51 : green_51.answer = guaranteedMaxCosetDim

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

Green51.green_51.lower

Solved: stated here without proof.

It is known that \(A + A\) must contain a coset of dimension \(\gg_\alpha n\) [Gr13].

theorem green_51.lower :
    ∀ (α : ℝ), 0 < α → α ≤ 1 →
    ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, c * (n : ℝ) ≤ guaranteedMaxCosetDim n α

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

Green51.green_51.upper

Solved: stated here without proof.

It is known that \(A + A\) need not contain a coset of dimension \(n - \sqrt{n}\) [Gr13].

theorem green_51.upper :
    ∃ α > 0, α ≤ 1 ∧ ∀ᶠ (n : ℕ) in atTop, (guaranteedMaxCosetDim n α : ℝ) < (n : ℝ) - sqrt n

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

Green51.green_51.one_half

Open: stated without proof.

Suppose that \(A \subset \mathbb{F}_2^n\) has density \(\alpha > 1/2 - C/\sqrt{n}\). Does \(A + A\) contain a subspace of co-dimension \(O_C(1)\)? [Sa11, Question 5.1]

theorem green_51.one_half :
    ∀ (k : ℝ), 0 < k →
      ∃ (c : ℕ), ∀ᶠ (n : ℕ) in atTop,
        ∀ (α : ℝ), α > (1/2 : ℝ) - k / sqrt (n : ℝ) → α ≤ 1 →
          n ≤ guaranteedMaxCosetDim n α + c

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

Green51.green_51.lower_ap

Solved: stated here without proof.

It is known that \(A + A\) must contain an arithmetic progression of length \(\sim \exp(c (\log N)^{1/2})\) [Gr02].

theorem green_51.lower_ap :
    ∀ (α : ℝ), 0 < α → α ≤ 1 →
      ∃ c > 0, ∀ᶠ (N : ℕ) in atTop,
        exp (c * log (N : ℝ) ^ (1/2 : ℝ)) ≤ guaranteedMaxAPLength N α

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

Green51.green_51.upper_ap

Solved: stated here without proof.

It is known that \(A + A\) need not contain an arithmetic progression of length \(\sim \exp(c (\log N)^{2/3 + \varepsilon})\), for any \(\varepsilon > 0\) [Ruz91].

theorem green_51.upper_ap :
    ∀ (α : ℝ), 0 < α → α < 1/2 → ∀ (ε : ℝ), 0 < ε →
      ∃ c > 0, ∀ᶠ (N : ℕ) in atTop,
        guaranteedMaxAPLength N α ≤ exp (c * log (N : ℝ) ^ (2/3 + ε : ℝ))

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

Sources
LeanGreen51.green_51 · Green51.green_51.lower · Green51.green_51.upper · Green51.green_51.one_half · Green51.green_51.lower_ap · Green51.green_51.upper_ap

TheoremGreen's Open Problem 52#

Reference: Green's Open Problems

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

Green52.green_52

Open: stated without proof.

Suppose that \(A \subset \mathbb{F}_2^n\) is a set with an additive complement of size \(K\). Does \(2A\) contain a coset of codimension \(O_K(1)\)?

theorem green_52 :
    ∃ (c : ℕ → ℕ), ∀ (n K : ℕ) (A : Set (𝔽₂ n)) (S : Finset (𝔽₂ n)),
      S.card = K → A + (S : Set (𝔽₂ n)) = Set.univ →
      ∃ (V : AffineSubspace (ZMod 2) (𝔽₂ n)), (V : Set (𝔽₂ n)) ⊆ A + A ∧
        n ≤ Module.finrank (ZMod 2) V.direction + c K

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

Green52.green_52_log

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/green-52-log-counterexample/blob/16cb5d0/lean/Green52LogCounterexampleFC.lean#L661-L668.

Could \(2A\) even contain a coset of codimension \(O(\log K)\)?

From Green's 2025 update:

Update 2025. Kaave Hosseini and Ryan Alweiss have independently pointed out that the second question is far too optimistic. To see this, let \(A\) be a Hamming ball of radius \(n/2 - \sqrt{n}\). There is a set \(S\) of size \(O(n)\) such that \(A + S = \mathbb{F}_2^n\); a random choice of \(S\) will work. However, every subspace contained in \(A - A\) has codimension \(\gg \sqrt{n}\).

theorem green_52_log :
    ¬ ∃ (C D : ℝ), ∀ (n K : ℕ) (A : Set (𝔽₂ n)) (S : Finset (𝔽₂ n)),
      0 < K → S.card = K → A + (S : Set (𝔽₂ n)) = Set.univ →
      ∃ (V : AffineSubspace (ZMod 2) (𝔽₂ n)), (V : Set (𝔽₂ n)) ⊆ A + A ∧
        (n : ℝ) ≤ (Module.finrank (ZMod 2) V.direction : ℝ) + C * log (K : ℝ) + D

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

Sources
LeanGreen52.green_52 · Green52.green_52_log

TheoremGreen's Open Problem 53#

References: - [Gr24] Green's Open Problems

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

Green53.green_53

Open: stated without proof.

Suppose that \(\mathbb{F}_2^n\) is partitioned in to sets \(A_1, ..., A_K\). Does \(2A_i\) contain a coset of codimension \(O_K(1)\) for some \(i\)?

theorem green_53 :
    ∃ (c : ℕ → ℕ), ∀ (n K : ℕ) (A : Fin K → Set (𝔽₂ n)),
      (⋃ i, A i) = Set.univ →
      Pairwise (Disjoint on A) →
      ∃ (i : Fin K) (S : AffineSubspace (ZMod 2) (𝔽₂ n)),
        (S : Set (𝔽₂ n)) ⊆ A i + A i ∧
        n ≤ Module.finrank (ZMod 2) S.direction + c K

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

Sources
LeanGreen53.green_53

TheoremBen Green's Open Problem 54#

References:

Here \(nK = K + \cdots + K\) (\(n\) times) is the \(n\)-fold sumset of \(K\), written n • K for n : ℕ with open scoped Pointwise.

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

Green54.green_54

Solved: stated here without proof.

Let \(K \subset \mathbb{R}^{\mathbb{N}}\) be a balanced compact set (that is, \(\lambda K \subseteq K\) whenever \(|\lambda| \leq 1\)) and suppose that the normalised Gaussian measure \(\gamma_\infty(K) \geq 0.99\). Does the sumset \(10K = K + \cdots + K\) (\(10\) times) contain a compact convex set \(C\) with \(\gamma_\infty(C) \geq 0.01\)?

The answer is yes: Hua, Song and Tudose proved that if \(\gamma_n(A) > 5/6\) then \(3(A + A + A)\) contains a symmetric convex body \(C\) with \(\gamma_n(C) \geq 1/4\), uniformly in \(n\).

theorem green_54 :
    ∀ K : Set (ℕ → ℝ), IsCompact K → Balanced ℝ K → (0.99 : ℝ≥0∞) ≤
    gaussianMeasureInf K → ∃ C : Set (ℕ → ℝ), IsCompact C ∧ Convex ℝ C ∧ C ⊆ (10 : ℕ) • K ∧
    (0.01 : ℝ≥0∞) ≤ gaussianMeasureInf C

Category research solved; AMS 46 Functional analysis, 52 Convex and discrete geometry, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/54.lean, line 57.

Green54.green_54_known_case

Solved: stated here without proof.

The same statement is known to be false for the sumset \(2K = K + K\) instead of \(10K\).

theorem green_54_known_case : ¬ (∀ K : Set (ℕ → ℝ), IsCompact K → Balanced ℝ K → (0.99 : ℝ≥0∞) ≤
    gaussianMeasureInf K → ∃ C : Set (ℕ → ℝ), IsCompact C ∧ Convex ℝ C ∧ C ⊆ K + K ∧
    (0.01 : ℝ≥0∞) ≤ gaussianMeasureInf C)

Category research solved; AMS 46 Functional analysis, 52 Convex and discrete geometry, 60 Probability theory and stochastic processes. Declared in FormalConjectures/GreensOpenProblems/54.lean, line 67.

Sources
LeanGreen54.green_54 · Green54.green_54_known_case

TheoremBen Green's Open Problem 57#

Reference: Ben Green's Open Problem 57

Let \(G\) be a finite abelian group. Consider the space \(\Phi(G)\) of all functions on \(G\) which are "convex combinations" (in the sense of complex coefficients \(c_i\) with \(\sum |c_i| \le 1\)) of functions of the form

\[\phi(g) := \mathbb{E}_{x_1 + x_2 + x_3 = g} f_1(x_2, x_3) f_2(x_1, x_3) f_3(x_1, x_2)\]

with \(\|f_i\|_\infty \le 1\) (where \(f_i : G \times G \to \mathbb{C}\)).

Let \(\Phi'(G)\) be the space defined similarly, but with \(f_3(x_1, x_2)\) required to be a function of \(x_1 + x_2\). Do \(\Phi(G)\) and \(\Phi'(G)\) coincide?

Note: The "convex combination" here uses complex coefficients whose absolute values sum to at most 1 (cf. personal communication with B. Green, April 2026). Since the base sets are balanced (closed under multiplication by unit complex numbers), this absolutely convex hull equals the real convex hull of the complex-valued base set.

Motivation: \(\Phi(G)\) is a 'generalised convolution algebra' as considered by Conlon–Fox–Zhao, whereas \(\Phi'(G)\) consists of Tao's \(\text{UAP}_2(G)\)-functions.

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

Green57.green_57.variants.z3_functional

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/f5afe85e1e02611f63c32ae041b33c67b7938cba/FormalConjectures/GreensOpenProblems/57.lean#L1071.

For \(G = \mathbb{Z}/3\mathbb{Z}\) and the functional \(a(0) = -1\), \(a(1) = -3\), \(a(2) = 3\), does the support function of \(\Phi\) at \(a\) strictly exceed that of \(\Phi'\)?

Numerical evidence suggests the answer is yes:

\[\sup_{\varphi \in \Phi'(\mathbb{Z}/3\mathbb{Z})} \operatorname{Re}\langle a, \varphi \rangle \;\lt \; \sup_{\varphi \in \Phi(\mathbb{Z}/3\mathbb{Z})} \operatorname{Re}\langle a, \varphi \rangle.\]

The DeepMind prover agent provided a formal proof, showing that \(\frac{183095}{30000}\) separates the support functions.

theorem green_57.variants.z3_functional :
    let a : ZMod 3 → ℂ := ![(-1 : ℂ), -3, 3]
    supportFn (ZMod 3) a (Φ' (ZMod 3)) < supportFn (ZMod 3) a (Φ (ZMod 3))

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

Green57.green_57.variants.z3

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/f5afe85e1e02611f63c32ae041b33c67b7938cba/FormalConjectures/GreensOpenProblems/57.lean#L1100.

Do \(\Phi(\mathbb{Z}/3\mathbb{Z})\) and \(\Phi'(\mathbb{Z}/3\mathbb{Z})\) coincide?

Numerical evidence suggests the answer is no: the integer functional \(a = (-1, -3, 3)\) separates the two spaces. A branch-and-bound verification over the phase variables shows \(\max_{\Phi'} \operatorname{Re}\langle a, \varphi \rangle < 6.112 < 6.115 \approx \max_{\Phi} \operatorname{Re}\langle a, \varphi \rangle\).

theorem green_57.variants.z3 :
    ¬ (Φ (ZMod 3) = Φ' (ZMod 3))

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

Green57.green_57

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/f5afe85e1e02611f63c32ae041b33c67b7938cba/FormalConjectures/GreensOpenProblems/57.lean#L1120.

Is it true that for every finite abelian group \(G\) the spaces \(\Phi(G)\) and \(\Phi'(G)\), obtained from kernels \(\phi(g) = \mathbb{E}_{x_1 + x_2 + x_3 = g} f_1(x_2, x_3) f_2(x_1, x_3) f_3(x_1, x_2)\) with \(\lVert f_i \rVert_\infty \le 1\) (where \(f_i : G \times G \to \mathbb{C}\)), still coincide when the third kernel is required to depend only on \(x_1 + x_2\)?

Green guesses that the answer is probably 'no'.

theorem green_57 :
    ¬ ∀ (G : Type) [AddCommGroup G] [Fintype G] [DecidableEq G],
      Φ G = Φ' G

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

Sources
LeanGreen57.green_57.variants.z3_functional · Green57.green_57.variants.z3 · Green57.green_57

TheoremBen Green's Open Problem 58#

Reference: Ben Green's Open Problem 58

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

Green58.green_58

Open: stated without proof.

Suppose \(A, B ⊆ \{1, \dots, N\}\) both have size at least \(N^{0.49}\). Must the sumset \(A + B\) contain a composite number?

theorem green_58 :
    ∀ᶠ (N : ℕ) in Filter.atTop, ∀ᵉ (A ⊆ Finset.Icc 1 N) (B ⊆ Finset.Icc 1 N),
      (N : ℝ) ^ (0.49 : ℝ) ≤ (A.card : ℝ) →
      (N : ℝ) ^ (0.49 : ℝ) ≤ (B.card : ℝ) →
      ∃ m ∈ (A + B), m.Composite

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

Sources
LeanGreen58.green_58

TheoremBen Green's Open Problem 60#

Reference: Ben Green's Open Problem 60

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

Green60.green_60

Open: stated without proof.

Is there an absolute constant \(c > 0\) such that, whenever \(A ⊆ \mathbb{N}\) is a set of squares with \(|A| ≥ 2\), the sumset \(A + A\) satisfies \(|A + A| ≥ |A|^{1 + c}\)?

theorem green_60 :
    ∃ c > (0 : ℝ),
      ∀ (A : Finset ℕ),
        (∀ a ∈ A, IsSquare a) →
        2 ≤ A.card →
          ((A + A).card : ℝ) ≥ (A.card : ℝ) ^ (1 + c)

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

Sources
LeanGreen60.green_60

TheoremBen Green's Open Problem 61#

Reference: Ben Green's Open Problem 61

This problem was originally considered by Erdős and Newman.

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

Green61.green_61

Open: stated without proof.

Suppose that \(A + A\) contains the first \(n\) squares. Is \(|A| \geq n^{1 - o(1)}\)?

It is known that necessarily \(|A| \geq n^{2/3 - o(1)}\), whilst in the other direction there do exist such \(A\) with \(|A| \ll_C n / \log^C n\) for any \(C\).

theorem green_61 :
    ∃ f : ℕ → ℝ, Tendsto f atTop (𝓝 0) ∧
      ∀ n : ℕ, n ≥ 1 → ∀ (A : Finset ℕ),
        (Finset.Icc 1 n).image (· ^ 2) ⊆ A + A →
          (n : ℝ) ^ (1 - f n) ≤ A.card

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

Sources
LeanGreen61.green_61

TheoremBen Green's Open Problem 62#

Let \(p\) be a large prime, and let \(A\) be the set of all primes less than \(p\). Is every \(x \in \{1, \ldots, p-1\}\) congruent to some product \(a_1 a_2\) where \(a_1, a_2 \in A\)?

This is a problem of Erdős, Odlyzko, and Sárközy [105] from 1987.

Reference: Ben Green's Open Problem 62

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

Green62.green_62

Open: stated without proof.

Let \(p\) be a large prime, and let \(A\) be the set of all primes less than \(p\). Is every \(x \in \{1, \ldots, p-1\}\) congruent to some product \(a_1 a_2\) where \(a_1, a_2 \in A\)?

theorem green_62 :
    ∀ᶠ p in atTop, p.Prime →
      let A := (Finset.range p).filter Nat.Prime
      ∀ x : ℕ, 1 ≤ x ∧ x < p →
        ∃ a₁ ∈ A, ∃ a₂ ∈ A, (x : ZMod p) = (a₁ * a₂ : ZMod p)

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

Sources
LeanGreen62.green_62

TheoremGreen's Open Problem 64#

Reference: Ben Green's Open Problems

Do there exist infinitely many primes \(p\) for which \(p - 2\) has an odd number of prime factors, counted with multiplicity?

Quoted from FormalConjectures/GreensOpenProblems/64.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 3 test statements, counted here but not shown.

Green64.green_64

Open: stated without proof.

Do there exist infinitely many primes \(p\) for which \(p - 2\) has an odd number of prime factors, counted with multiplicity (i.e. \(\Omega(p - 2)\) is odd)?

theorem green_64 :
    {p : ℕ | p.Prime ∧ Odd (Ω (p - 2))}.Infinite

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

Green64.green_64.variants.p_sub_one

Open: stated without proof.

The same question as green_64 but with \(p - 1\) instead of \(p - 2\). Green notes this is "probably more natural".

theorem green_64.variants.p_sub_one :
    {p : ℕ | p.Prime ∧ Odd (Ω (p - 1))}.Infinite

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

Sources
LeanGreen64.green_64 · Green64.green_64.variants.p_sub_one

TheoremBen Green's Open Problem 65#

References: - [Gr26] Ben Green's Open Problem 65 - [Gr22] Green, Ben. "On Sárközy's theorem for shifted primes."

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

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

Green65.green_65

Open: stated without proof.

Is there \(c > 0\) such that every sufficiently large subset \(A \subseteq [N]\) of size at least \(N^{1-c}\) has a difference that is a nonzero square?

theorem green_65 :
    LargeDifferencePattern IsNonzeroSquare

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

Green65.green_65.variants.prime_minus_one

Solved: stated here without proof.

Green asks the analogous question with a nonzero square replaced by \(p - 1\) for a prime \(p\). Green [Gr22, Theorem 1.1] solved this positively.

theorem green_65.variants.prime_minus_one :
    LargeDifferencePattern IsPrimeMinusOne

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

Sources
LeanGreen65.green_65 · Green65.green_65.variants.prime_minus_one

TheoremBen Green's Open Problem 66#

Reference: Ben Green's Open Problem 66

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

Green66.green_66

Open: stated without proof.

Is there always a sum of two squares between \(X - \frac{1}{10}X^{1/4}\) and \(X\)? We formalize this as an eventual statement for sufficiently large real \(X\).

theorem green_66 :
    ∀ᶠ X : ℝ in atTop,
      ∃ n : ℕ, IsSumOfTwoSquares n ∧
        (n : ℝ) ∈ Set.Icc (X - (1 / 10 : ℝ) * X ^ (1 / 4 : ℝ)) X

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

Green66.green_66.variants.trivial_bound

Proved here.

Green notes that a well-known, almost trivial argument gives an \(O(X^{1/4})\) bound on the left.

theorem green_66.variants.trivial_bound :
    ∃ C > (0 : ℝ), ∀ᶠ X : ℝ in atTop,
      ∃ n : ℕ, IsSumOfTwoSquares n ∧
        (n : ℝ) ∈ Set.Icc (X - C * X ^ (1 / 4 : ℝ)) X

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

Sources
LeanGreen66.green_66 · Green66.green_66.variants.trivial_bound

TheoremBen Green's Open Problem 68#

References: - [Gr24] Green, Ben. "100 open problems." (2024). - [Gr14] Green, B., Approximate algebraic structure. Proceedings of the ICM 2014, Vol. I, Kyung Moon Sa, Seoul (2014), 341--367. arXiv:1404.0093 - [Vo90] Voloch, J. F., Arcs in projective planes over prime fields. J. Geom. 38 (1990), 198--200. - [BaLa19] Ball, S. and Lavrauw, M., Arcs in finite projective spaces. EMS Surv. Math. Sci. 6 (2019), 133--172. arXiv:1908.10772

Quoted from FormalConjectures/GreensOpenProblems/68.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 2 API statements, counted here but not shown.

Green68.green_68

Open: stated without proof.

Suppose that \(A \subset \mathbb{F}_p^2\) is a set meeting every line in at most 2 points. Is it true that all except \(o(p)\) points of \(A\) lie on a cubic curve?

Such sets are called arcs. We read "cubic curve" as the zero set of a nonzero polynomial of total degree at most \(3\) in two variables over \(\mathbb{F}_p\). This includes conics and lines, and unions of these. The \(o(p)\) is uniform in \(A\): for every \(\varepsilon > 0\) and every large prime \(p\), every arc \(A\) has all but at most \(\varepsilon p\) of its points on one such curve. Green asked a projective form of this question in [Gr14, Section 4.4]. [Gr24] notes that the question is more natural in projective space, and that the analogue over \(\mathbb{F}_q\) with \(q = p^2\) is false, because of Hermitian quadrics.

theorem green_68 :
    ∀ ε : ℝ, 0 < ε → ∃ p₀ : ℕ, ∀ (p : ℕ) [Fact p.Prime], p₀ ≤ p →
      ∀ A : Finset (Fin 2 → ZMod p), MeetsLinesInAtMost 2 A →
        ∃ F : MvPolynomial (Fin 2) (ZMod p), F ≠ 0 ∧ F.totalDegree ≤ 3 ∧
          (numOffCurve F A : ℝ) ≤ ε * p

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 51 Geometry. Declared in FormalConjectures/GreensOpenProblems/68.lean, line 89.

Green68.green_68.variants.voloch

Solved: stated here without proof.

Voloch's theorem. If \(p\) is an odd prime and \(A \subset \mathbb{F}_p^2\) is a set meeting every line in at most 2 points, with \(|A| > \frac{44}{45} p + \frac{8}{9}\), then \(A\) lies on a conic [BaLa19, Theorem 52], due to Voloch [Vo90]. This is the affine form of the theorem for planar arcs in \(\mathrm{PG}(2, p)\): a set of affine points is an arc in \(\mathrm{PG}(2, p)\) if and only if it meets every affine line in at most 2 points, and the affine equation \(Q(x, y, 1) = 0\) of a conic \(Q = 0\) through \(A\) is a nonzero polynomial of degree at most \(2\) vanishing on \(A\). We assume \(p\) odd, as in [BaLa19, Section 15.3].

theorem green_68.variants.voloch :
    ∀ (p : ℕ) [Fact p.Prime], p ≠ 2 →
      ∀ A : Finset (Fin 2 → ZMod p), MeetsLinesInAtMost 2 A →
        (44 : ℝ) / 45 * p + 8 / 9 < A.card →
          ∃ F : MvPolynomial (Fin 2) (ZMod p),
            F ≠ 0 ∧ F.totalDegree ≤ 2 ∧ ∀ a ∈ A, MvPolynomial.eval a F = 0

Category research solved; AMS 05 Combinatorics, 14 Algebraic geometry, 51 Geometry. Declared in FormalConjectures/GreensOpenProblems/68.lean, line 106.

Green68.green_68.variants.bounded_intersection

Open: stated without proof.

More generally than in green_68, one may conjecture that if \(A \subset \mathbb{F}_p^2\) meets every line in \(O(1)\) points, then all but \(o(p)\) points of \(A\) lie on a curve of degree \(O(1)\) [Gr24]. We read this as: for every \(k\) there is a degree bound \(d\) such that, for every \(\varepsilon > 0\) and every large prime \(p\), every set meeting each line in at most \(k\) points has all but at most \(\varepsilon p\) points on the zero set of a nonzero polynomial of total degree at most \(d\). The degree \(d\) depends on \(k\), not on \(p\) or \(\varepsilon\).

theorem green_68.variants.bounded_intersection :
    ∀ k : ℕ, ∃ d : ℕ, ∀ ε : ℝ, 0 < ε → ∃ p₀ : ℕ, ∀ (p : ℕ) [Fact p.Prime], p₀ ≤ p →
      ∀ A : Finset (Fin 2 → ZMod p), MeetsLinesInAtMost k A →
        ∃ F : MvPolynomial (Fin 2) (ZMod p), F ≠ 0 ∧ F.totalDegree ≤ d ∧
          (numOffCurve F A : ℝ) ≤ ε * p

Category research open; AMS 05 Combinatorics, 14 Algebraic geometry, 51 Geometry. Declared in FormalConjectures/GreensOpenProblems/68.lean, line 123.

Green68.green_68.variants.f_four_little_o

Open: stated without proof.

Denote by \(f_d(p)\) the size of the largest no-three-in-a-line set in \(\mathbb{F}_p^d\). Is \(f_4(p) = o(p^3)\)?

[Gr24] reports that \(f_2(p) \sim p\) and \(f_3(p) \sim p^2\), and that the best known upper bound is \(f_4(p) \le (1 - c)p^3\) for a constant \(c > 0\), due to Nagy and Szőnyi, a slight improvement of the trivial bound.

theorem green_68.variants.f_four_little_o :
    ∀ ε : ℝ, 0 < ε → ∃ p₀ : ℕ, ∀ (p : ℕ) [Fact p.Prime], p₀ ≤ p →
      (maxNoThreeCollinear 4 p : ℝ) ≤ ε * (p : ℝ) ^ 3

Category research open; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/GreensOpenProblems/68.lean, line 139.

Green68.green_68.variants.f_four_polynomial

Open: stated without proof.

Is \(f_4(p) = O(p^{2+o(1)})\), where \(f_d(p)\) is the size of the largest no-three-in-a-line set in \(\mathbb{F}_p^d\)? We read \(O(p^{2+o(1)})\) as: for every \(\varepsilon > 0\) there is \(C\) with \(f_4(p) \le C p^{2+\varepsilon}\) for all primes \(p\). This is stronger than green_68.variants.f_four_little_o.

theorem green_68.variants.f_four_polynomial :
    ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, ∀ (p : ℕ) [Fact p.Prime],
      (maxNoThreeCollinear 4 p : ℝ) ≤ C * (p : ℝ) ^ (2 + ε)

Category research open; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/GreensOpenProblems/68.lean, line 151.

Green68.green_68.variants.blocking_set

Open: stated without proof.

Let \(\mathrm{PG}(2, q)\) be the projective plane over \(\mathbb{F}_q\). Is there a set \(B \subset \mathrm{PG}(2, q)\) (a "blocking set") meeting every line in at least 1, but at most 1000, points?

A question of this kind goes back to Erdős (see [Gr24]). For \(q\) not prime such sets exist in many cases [Gr24]. As \(q\) ranges over sufficiently large primes, it is speculated that no such set exists [Gr24]. We state this speculation. Points of \(\mathrm{PG}(2, p)\) are the one-dimensional subspaces of \(\mathbb{F}_p^3\) (Projectivization), and lines are the two-dimensional subspaces.

theorem green_68.variants.blocking_set :
    ∃ p₀ : ℕ, ∀ (p : ℕ) [Fact p.Prime], p₀ ≤ p →
      ¬ ∃ B : Set (Projectivization (ZMod p) (Fin 3 → ZMod p)),
        ∀ W : Submodule (ZMod p) (Fin 3 → ZMod p), Module.finrank (ZMod p) W = 2 →
          1 ≤ Set.ncard {x ∈ B | x.submodule ≤ W} ∧ Set.ncard {x ∈ B | x.submodule ≤ W} ≤ 1000

Category research open; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/GreensOpenProblems/68.lean, line 166.

Sources
LeanGreen68.green_68 · Green68.green_68.variants.voloch · Green68.green_68.variants.bounded_intersection · Green68.green_68.variants.f_four_little_o · Green68.green_68.variants.f_four_polynomial · Green68.green_68.variants.blocking_set

TheoremBen Green's Open Problem 70#

References: - [Gr24] Green, Ben. "100 open problems." (2024). - [ABBCDHKLPW11] Abel, Z., Ballinger, B., Bose, P., Collette, S., Dujmović, V., Hurtado, F., Kominers, S. D., Langerman, S., Pór, A. and Wood, D. R., Every large point set contains many collinear points or an empty pentagon. Graphs Combin. 27 (2011), 47-60. arXiv:0904.0262 - [KPW05] Kára, J., Pór, A. and Wood, D. R., On the chromatic number of the visibility graph of a set of points in the plane. Discrete Comput. Geom. 34 (2005), 497-506. doi:10.1007/s00454-005-1177-z - [PoWo10] Pór, A. and Wood, D. R., On visibility and blockers. J. Comput. Geom. 1 (2010), 29-40. arXiv:0912.1150

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

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

Green70.green_70

Open: stated without proof.

Fix integers \(k, \ell\). Is it true that, given a set of \(n \geq n_0(k, \ell)\) points in \(\mathbb{R}^2\), either some \(k\) of them lie on a line, or some \(\ell\) of them are 'mutually visible', that is to say that line segment joining them contains no other point from the set?

This question was first raised by Kára, Pór and Wood [KPW05]. It is called the big-line-big-clique conjecture [PoWo10, Conjecture 1]. We read "mutually visible" as "pairwise visible". The cases \(k \leq 3\) are trivial: a set with no three collinear points has all pairs visible. For the cases \(\ell \leq 5\), see green_70.variants.five_visible.

theorem green_70 :
    ∀ k ℓ : ℕ, ∃ n₀ : ℕ, ∀ P : Finset (ℝ × ℝ),
      n₀ ≤ #P → HasCollinear k P ∨ HasMutuallyVisible ℓ P

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/70.lean, line 81.

Green70.green_70.variants.five_visible

Solved: stated here without proof.

The answer to green_70 is yes for \(\ell \leq 5\) [Gr24]: for every \(k\), every sufficiently large planar set contains \(k\) collinear points or \(5\) mutually visible points. The case \(\ell = 5\) is [ABBCDHKLPW11, Theorem 5], and it implies the cases \(\ell \leq 4\) (see HasMutuallyVisible.mono). According to [ABBCDHKLPW11, Section 1.4], the case \(\ell = 4\) was proved in [KPW05]. In [ABBCDHKLPW11] and [PoWo10] the letters \(k\) and \(\ell\) are interchanged.

theorem green_70.variants.five_visible :
    ∀ k : ℕ, ∃ n₀ : ℕ, ∀ P : Finset (ℝ × ℝ),
      n₀ ≤ #P → HasCollinear k P ∨ HasMutuallyVisible 5 P

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/70.lean, line 94.

Green70.green_70.variants.empty_pentagon

Solved: stated here without proof.

Generalised empty pentagon theorem [ABBCDHKLPW11, Theorem 3]: for every integer \(k \geq 2\), every sufficiently large finite set of points in the plane contains \(k\) collinear points or an empty pentagon. By HasEmptyPentagon.hasMutuallyVisible, this implies green_70.variants.five_visible, which is [ABBCDHKLPW11, Theorem 5].

theorem green_70.variants.empty_pentagon :
    ∀ k : ℕ, 2 ≤ k → ∃ n₀ : ℕ, ∀ P : Finset (ℝ × ℝ),
      n₀ ≤ #P → HasCollinear k P ∨ HasEmptyPentagon P

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/70.lean, line 106.

Sources
LeanGreen70.green_70 · Green70.green_70.variants.five_visible · Green70.green_70.variants.empty_pentagon

TheoremBen Green's Open Problem 72#

More commonly known as the no-three-in-line problem.

What is the largest subset of the grid \([N]^2\) with no three points in a line? In particular, for \(N\) sufficiently large, is it impossible to have a set of size \(2N\) with this property?

The upper bound \(2N\) is the easy half and is allowedSetSize_le below, by pigeonhole on the columns. The open content is whether \(2N\) is attained. Green records that it is for \(N\) up to around 50, that \((3/2 + o(1))N\) points are achievable for arbitrary \(N\), and that his "personal suspicion is that this is optimal". The Wikipedia reference points the same way: Guy and Kelly conjectured \(c = \sqrt[3]{2\pi^2/3} \approx 1.874\), and after an error in the heuristic was found Guy corrected it to \(c = \pi/\sqrt3 \approx 1.814\). Both are below \(2\), so the expected answer to the question above is yes.

References: - Ben Green's Open Problem 72 - Wikipedia - [GK2025] Grebennikov, A. Kwan, M. No \((k + 1)\)-in-line problem for large constant \(k\). https://arxiv.org/abs/2510.17743

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

Green72.allowedSetSize_le

Textbook result, proved here.

By the pigeon hole principle, the size of a subset of an \(N \times N\) grid such that no \(k\) points lie on a line is bounded by \(\leq (k - 1) * N\).

theorem allowedSetSize_le {k : ℕ} {N : ℕ} :
    AllowedSetSize k N ≤ (k - 1) * N

Category textbook; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/72.lean, line 61.

Green72.NoKInLine

Open: stated without proof.

The no-k-in-line problem: For which \(k > 2\) does every \(N \times N\) grid with \(N \geq k\) contain a set of \((k - 1) N\) points with no \(k\) on a line, so that AllowedSetSize k N is the pigeonhole bound \((k - 1) N\)?

[GK2025] proves that every \(k > 10^{37}\) has this property, which is no_k_in_line_big below, and does not optimise this constant. At \(k = 3\) it is the property that Green expects to fail for large \(N\), see green_72.

theorem NoKInLine : NoKInLine.answer = {k | 2 < k ∧ ∀ N, k ≤ N → NoKInLineFor k N}

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/72.lean, line 98.

Green72.green_72

Open: stated without proof.

Green's Open Problem 72 / No-three-in-line problem: For \(N\) sufficiently large, is it impossible to have \(2N\) points in \([N]^2\) with no three in a line? Green suspects the answer is yes, and that \((3/2 + o(1))N\) is optimal.

theorem green_72 : ∀ᶠ N in Filter.atTop, ¬ NoKInLineFor 3 N

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/72.lean, line 105.

Green72.green_72.variants.eventually

Open: stated without proof.

Is \(2N\) attained for all sufficiently large \(N\)?

This is not the negation of green_72. Negating that one gives \(\exists^f N\) where this asks \(\forall^f N\), so both can be answered False if the behaviour oscillates. Green asks his question in the green_72 form.

theorem green_72.variants.eventually : ∀ᶠ N in Filter.atTop, NoKInLineFor 3 N

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/72.lean, line 116.

Green72.no_three_in_line_le

Solved: stated here without proof.

For \(N \leq 60\), this has been verified with computers.

theorem no_three_in_line_le {N : ℕ} (hN : 3 ≤ N) (hN' : N ≤ 60) :
    NoKInLineFor 3 N

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/72.lean, line 121.

Green72.no_k_in_line_big

Solved: stated here without proof.

In [GK2025] Grebennikov and Kwan prove that the pigeonhole bound \((k - 1) N\) is attained for \(k > 10 ^ {37}\) and \(N \geq k\).

theorem no_k_in_line_big {k : ℕ} (N : ℕ) (h : 10 ^ 37 < k) (hN : k ≤ N) :
    NoKInLineFor k N

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/72.lean, line 128.

Sources
LeanGreen72.allowedSetSize_le · Green72.NoKInLine · Green72.green_72 · Green72.green_72.variants.eventually · Green72.no_three_in_line_le · Green72.no_k_in_line_big

TheoremBen Green's Open Problem 75#

References: - [Gr24] Green, Ben. "100 open problems." (2024). - [CL25] Conlon, D. and Lim, J., Everywhere unbalanced configurations. Adv. Math. 480 (2025), Paper No. 110445. arXiv:2308.02466 - [Pi03] Pinchasi, R., Lines with many points on both sides. Discrete Comput. Geom. 30 (2003), 415-435. doi:10.1007/s00454-003-2826-8

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

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

Green75.green_75

Open: stated without proof.

Let \(X \subset \mathbb{R}^2\) be a set of \(n\) points. Does there exist a line \(\ell\) through at least two points of \(X\) such that the numbers of points on either side of \(\ell\) differ by at most \(100\)?

This is a form of the Kupitz-Perles conjecture [Gr24]. We take \(n \geq 2\), since a line through two points of \(X\) needs two points. If all points of \(X\) are collinear, the line through them has no points on either side.

theorem green_75 :
    ∀ X : Finset (ℝ × ℝ), 2 ≤ #X → ∃ p ∈ X, ∃ q ∈ X, p ≠ q ∧ imbalance X p q ≤ 100

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

Green75.green_75.variants.exists_constant

Open: stated without proof.

Is there a constant \(C\) such that every finite set \(X \subset \mathbb{R}^2\) with at least two points has a line through two points of \(X\) whose sides differ by at most \(C\)? This is the question of Kupitz in the form of [CL25, Section 1], where the constant is not specified.

green_75 implies it with \(C = 100\).

theorem green_75.variants.exists_constant :
    ∃ C : ℕ, ∀ X : Finset (ℝ × ℝ), 2 ≤ #X →
      ∃ p ∈ X, ∃ q ∈ X, p ≠ q ∧ imbalance X p q ≤ C

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/75.lean, line 83.

Green75.green_75.variants.pinchasi

Solved: stated here without proof.

Pinchasi [Pi03] proved that the answer to green_75 is yes if \(100\) is replaced by \(C \log \log n\) for an absolute constant \(C\), where \(n = |X|\) [Gr24]. This is the best known bound. [CL25, Theorem 1.1] states Pinchasi's theorem for generalised configurations (points with pseudolines); sets of points with lines are a special case. The hypothesis \(n \geq 3\) ensures that \(\log \log n > 0\).

theorem green_75.variants.pinchasi :
    ∃ C : ℝ, ∀ X : Finset (ℝ × ℝ), 3 ≤ #X → ∃ p ∈ X, ∃ q ∈ X, p ≠ q ∧
      (imbalance X p q : ℝ) ≤ C * Real.log (Real.log #X)

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/75.lean, line 96.

Green75.green_75.variants.alon

Solved: stated here without proof.

Kupitz conjectured that one can take the difference to be at most \(1\) [CL25, Section 1]. Alon showed that this is false: there are finite point sets for which, for every line through two of its points, the numbers of points on the two sides differ by at least \(2\) [CL25, Section 1]. [Gr24] phrases this as: the answer to green_75 is no if \(100\) is replaced by \(2\). Since the sets in [CL25] have differences of at least \(2\), they show that \(100\) cannot be replaced by \(1\). We state the form given in [CL25].

theorem green_75.variants.alon :
    ∃ X : Finset (ℝ × ℝ), 2 ≤ #X ∧ ∀ p ∈ X, ∀ q ∈ X, p ≠ q → 2 ≤ imbalance X p q

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/75.lean, line 110.

Sources
LeanGreen75.green_75 · Green75.green_75.variants.exists_constant · Green75.green_75.variants.pinchasi · Green75.green_75.variants.alon

TheoremBen Green's Open Problem 76#

References: - [Gr24] Green, Ben. "100 open problems." (2024). - [AES10] Aronov, Boris, Esther Ezra, and Micha Sharir. "Small-size \(\varepsilon\)-nets for axis-parallel rectangles and boxes." SIAM Journal on Computing 39.7 (2010): 3248-3282. doi:10.1137/090762968 - [PT11] Pach, János. "Boxes and the art of \(\varepsilon\)-net maintenance." Invited problems, 2nd Emléktábla Workshop (2011), Problem 5 (Pach and Tardos). PDF - [PT13] Pach, János, and Gábor Tardos. "Tight lower bounds for the size of epsilon-nets." Journal of the American Mathematical Society 26.3 (2013): 645-658. doi:10.1090/S0894-0347-2012-00759-0, arXiv:1012.1240

Quoted from FormalConjectures/GreensOpenProblems/76.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. It also has 1 test statement and 3 API statements, counted here but not shown.

Green76.green_76

Open: stated without proof.

Let \(A\) be a set of \(n\) points in the plane. Can one select a set \(A'\) of \(n/2\) points, with the property that any axis-parallel rectangle containing \(1000\) points of \(A\) contains at least one point of \(A'\)?

We read "a set of \(n/2\) points" as at most \(\lfloor n/2 \rfloor\) points, and "containing \(1000\) points" as containing at least \(1000\) points. The points of \(A'\) need not lie in \(A\). If \(A' \subseteq A\) is required, then the answer is no; see green_76.variants.subset.

theorem green_76 :
    ∀ A : Finset (ℝ × ℝ), ∃ A', #A' ≤ #A / 2 ∧ HitsRichRectangles 1000 A A'

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/76.lean, line 64.

Green76.green_76.variants.exists_constant

Open: stated without proof.

Is there a constant \(k\) such that the answer to green_76 is yes with \(1000\) replaced by \(k\)? [PT11, Problem 5] asks this in an equivalent form, with \(k = C + 1\): is there a constant \(C\) such that every set of \(n\) points in the plane has a set \(Y\) of \(n/2\) points such that every axis-parallel rectangle disjoint from \(Y\) contains at most \(C\) of the \(n\) points?

Each of green_76 and green_76.variants.weak_net implies this.

theorem green_76.variants.exists_constant :
    ∃ k : ℕ, ∀ A : Finset (ℝ × ℝ), ∃ A', #A' ≤ #A / 2 ∧ HitsRichRectangles k A A'

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/76.lean, line 77.

Green76.green_76.variants.weak_net

Open: stated without proof.

Do weak \(\varepsilon\)-nets of size \(O(1/\varepsilon)\) exist for axis-parallel rectangles in the plane? [Gr24] believes that green_76 is an instance of this question, which he states for axis-parallel boxes. With \(k = \varepsilon n\): is there a constant \(C\) such that, for every \(k \ge 1\), every set \(A\) of \(n\) points in the plane has a set \(A'\) of at most \(Cn/k\) points that meets every axis-parallel rectangle containing at least \(k\) points of \(A\)?

A positive answer implies green_76.variants.exists_constant, and it implies green_76 if the constant \(C\) is at most \(500\). [AES10, Theorem 2.2] gives such sets of size \(O(\varepsilon^{-1} \log \log \varepsilon^{-1})\), even with \(A' \subseteq A\). When \(A' \subseteq A\) is required, this size is optimal [PT13, Theorem 4].

theorem green_76.variants.weak_net :
    ∃ C : ℝ, ∀ k : ℕ, 0 < k → ∀ A : Finset (ℝ × ℝ),
      ∃ A', #A' ≤ C * #A / k ∧ HitsRichRectangles k A A'

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/76.lean, line 94.

Green76.green_76.variants.subset

Solved: stated here without proof.

If \(A'\) is required to be a subset of \(A\), then the answer to green_76 is no, even with \(1000\) replaced by any constant. [Gr24] attributes this remark to Alon. It follows from [PT13, Lemma 4.1], which [Gr24] cites as Lemma 3.1, its number in the arXiv version.

theorem green_76.variants.subset :
    ¬ ∃ k : ℕ, ∀ A : Finset (ℝ × ℝ), ∃ A' ⊆ A, #A' ≤ #A / 2 ∧ HitsRichRectangles k A A'

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/76.lean, line 105.

Green76.green_76.variants.subset_log_log

Solved: stated here without proof.

The answer to green_76 is yes if \(1000\) is replaced by \(C \log \log n\) [Gr24]. This follows from [AES10, Theorem 2.2], which gives \(\varepsilon\)-nets of size \(O(\varepsilon^{-1} \log \log \varepsilon^{-1})\) for axis-parallel rectangles. These nets are subsets of \(A\). The hypothesis \(n \ge 3\) ensures that \(\log \log n > 0\).

theorem green_76.variants.subset_log_log :
    ∃ C : ℝ, ∀ A : Finset (ℝ × ℝ), 3 ≤ #A → ∃ A' ⊆ A,
      #A' ≤ #A / 2 ∧ HitsRichRectangles ⌈C * Real.log (Real.log #A)⌉₊ A A'

Category research solved; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/76.lean, line 116.

Sources
LeanGreen76.green_76 · Green76.green_76.variants.exists_constant · Green76.green_76.variants.weak_net · Green76.green_76.variants.subset · Green76.green_76.variants.subset_log_log

TheoremBen Green's Open Problem 77#

Reference: - Ben Green's Open Problem 77

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

Green77.green_77

Open: stated without proof.

Given \(n\) points in the unit disc, must there be a triangle of area at most \(n^{-2+o(1)}\) determined by them?

theorem green_77 :
    ∃ (o : ℕ → ℝ), Tendsto o atTop (𝓝 0) ∧
      α ≪ fun n ↦ n ^ (-2 + o n)

Category research open; AMS 05 Combinatorics, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/77.lean, line 39.

Sources
LeanGreen77.green_77

TheoremBen Green's Open Problem 82#

References: - Ben Green's Open Problem 82 - An improved lower bound for a problem of Littlewood on the zeros of cosine polynomials (Bedert, 2025) - Cosine polynomials with few zeros (Juškevičius & Sahasrabudhe, 2020)

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

Green82.green_82

Open: stated without proof.

Let \(A \subset \mathbb{Z}\) be a set of size \(n\). For how many \(\theta \in \mathbb{R}/\mathbb{Z}\) must we have \(\sum_{a \in A} \cos(2\pi a\theta) = 0\)? The answer is the function minZeros.

theorem green_82 : green_82.answer = minZeros

Category research open; AMS 11 Number theory, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/GreensOpenProblems/82.lean, line 47.

Green82.green_82_lower_bound

Solved: stated here without proof.

Lower bound: every set has at least \((\log \log n)^{1-o(1)}\) zeros.

theorem green_82_lower_bound :
    ∃ o : ℕ → ℝ, o =o[atTop] (fun _ ↦ (1 : ℝ)) ∧
      ∀ᶠ n in atTop, ∀ A : Finset ℤ, A.card = n →
        (⌊(Real.log (Real.log n)) ^ (1 - |o n|)⌋₊ : ℕ∞) ≤
        ({θ : ℝ | θ ∈ Ico 0 1 ∧ ∑ a ∈ A, cos (2 * π * a * θ) = 0} : Set ℝ).ncard

Category research solved; AMS 11 Number theory, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/GreensOpenProblems/82.lean, line 52.

Green82.green_82_upper_bound

Solved: stated here without proof.

Upper bound: there exists \(A\) with at most \(C(n \log n)^{2/3}\) zeros.

theorem green_82_upper_bound :
    ∃ C > 0, ∀ n ≥ 1, ∃ A : Finset ℤ, A.card = n ∧
      ({θ : ℝ | θ ∈ Ico 0 1 ∧ ∑ a ∈ A, cos (2 * π * a * θ) = 0} : Set ℝ).ncard ≤
      (⌊C * (n * Real.log n) ^ (2 / 3 : ℝ)⌋₊ : ℕ∞)

Category research solved; AMS 11 Number theory, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/GreensOpenProblems/82.lean, line 61.

Sources
LeanGreen82.green_82 · Green82.green_82_lower_bound · Green82.green_82_upper_bound

TheoremGreen's Open Problem 85#

Carbery’s rectangle problem

References: - [Gr24] Green, Ben. "100 open problems." (2024). - [CCW99] Carbery, Anthony, Michael Christ, and James Wright. "Multidimensional van der Corput and sublevel set estimates." Journal of the American Mathematical Society 12.4 (1999): 981-1015 Section 6. - [Ke00] Keleti, Tamás. "Density and covering properties of intervals of ℝn." Mathematika 47.1-2 (2000): 229-242. - [KKM02] Katz, Nets Hawk, Elliot Krop, and Mauro Maggioni. "Remarks on the box problem." Mathematical Research Letters 9.4 (2002): 515-520. - [Mu02] Mubayi, Dhruv. "Some exact results and new asymptotics for hypergraph Turán numbers." Combinatorics, Probability and Computing 11.3 (2002): 299-309 Conjecture 1.4. - [CPZ20] Conlon, David, Cosmin Pohoata, and Dmitriy Zakharov. "Random multilinear maps and the Erd\H {o} s box problem." arXiv preprint arXiv:2011.09024 (2020).

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

Green85.green_85

Open: stated without proof.

Suppose that \(A\) is an open subset of \([0, 1]^2\) with measure \(\alpha\). Are there four points in \(A\) determining an axis-parallel rectangle with area \(\gt c \alpha^2\)?

theorem green_85 :
  ∃ c > 0, ∀ A : Set (ℝ × ℝ),
    IsOpen A →
    A ⊆ Icc 0 1 ×ˢ Icc 0 1 →
    A.Nonempty →
    let α := (volume A).toReal
    ∃ x₁ x₂ y₁ y₂,
      {(x₁, y₁), (x₂, y₁), (x₂, y₂), (x₁, y₂)} ⊆ A ∧
      c * α ^ 2 ≤ |x₁ - x₂| * |y₁ - y₂|

Category research open; AMS 28 Measure and integration, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/85.lean, line 45.

Green85.green_85_loose

Solved: stated here without proof.

From [Gr24] "It is quite easy to show using Cauchy-Schwarz that there must be such a rectangle with area \(\gg \alpha^2 (\log 1/\alpha)^{-1}\)."

theorem green_85_loose :
    ∃ c > 0, ∀ᶠ α in 𝓝[>] 0,
    ∀ A : Set (ℝ × ℝ),
    IsOpen A →
    A ⊆ Icc 0 1 ×ˢ Icc 0 1 →
    A.Nonempty →
    α = (volume A).toReal →
    ∃ x₁ x₂ y₁ y₂,
      {(x₁, y₁), (x₂, y₁), (x₂, y₂), (x₁, y₂)} ⊆ A ∧
      c * α ^ 2 * (Real.log (1/α))⁻¹ ≤ |x₁ - x₂| * |y₁ - y₂|

Category research solved; AMS 28 Measure and integration, 52 Convex and discrete geometry. Declared in FormalConjectures/GreensOpenProblems/85.lean, line 61.

Sources
LeanGreen85.green_85 · Green85.green_85_loose

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.