Ben Green's Open Problem 1 to Green's Open Problem 27
TheoremBen Green's Open Problem 1#
References: - Ben Green's Open Problem 1 - [Be25] Bedert, Benjamin, Large sum-free subsets of sets of integers via \(L^1\)-estimates for trigonometric series. arXiv:2502.08624 (2025).
Quoted from FormalConjectures/GreensOpenProblems/1.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved.
Green1.green_1
Solved: stated here without proof.
Let \(A\) be a set of \(n\) positive integers. Does \(A\) contain a sum-free set of size at least \(\frac n 3 + Ω(n)\), where \(Ω(n) → ∞\) as \(n → ∞\)?
Bedert [Be25] proved that every set of \(n\) integers contains a sum-free subset of size at least \(\frac n 3 + c \log\log n\) for some absolute constant \(c > 0\), so the answer is yes.
theorem green_1 : ∃ Ω : ℕ → ℝ, atTop.Tendsto Ω atTop ∧
∀ n, ∀ (A : Finset ℕ), (∀ a ∈ A, 0 < a) → A.card = n →
∃ (S : Finset ℕ), S ⊆ A ∧ IsSumFree (S : Set ℕ) ∧ ((n : ℝ) / 3) + Ω n ≤ S.card
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/1.lean, line 43.
Sources
TheoremBen Green's Open Problem 2#
References: - [Gr24] Green, Ben. "100 open problems." (2024). - [Er65] P. Erdős. Extremal problems in number theory, In Proc. Sympos. Pure Math., Vol. VIII, pages 181–189. Amer. Math. Soc., Providence, R.I., 1965. - [Sa21] Sanders, Tom. "The Erdős–Moser Sum-free Set Problem." Canadian Journal of Mathematics 73.1 (2021): 63-107. - [Ru05] I. Z. Ruzsa, Sum-avoiding subsets. Ramanujan J., 9 (2005) (1-2):77–82. - [Ch71] S. L. G. Choi. On a combinatorial problem in number theory. Proc. London Math. Soc. (3), 23:629–642, 1971. doi:10.1112/plms/s3-23.4.629. - [BSS00] A. Baltz, T. Schoen, and A. Srivastav. Probabilistic construction of small strongly sum-free sets via large Sidon sets. Colloq. Math., 86(2):171–176, 2000. doi:10.4064/cm-86-2-171-176.
Quoted from FormalConjectures/GreensOpenProblems/2.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.
Green2.green_2
Open: stated without proof.
Let \(A \subset \mathbf{Z}\) be a set of \(n\) integers. Is there a set \(S \subset A\) of size \((\log n)^{100}\) such that the restricted sumset\(S \hat{+} S\) is disjoint from \(A\)?
theorem green_2 :
∀ᶠ n : ℕ in atTop, ∀ A : Finset ℤ, A.card = n →
(maxRestrictedSumAvoidingSubsetSize A : ℝ) ≥ (Real.log n) ^ 100
Category research open; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/2.lean, line 58.
Green2.green_2_lower_bound_sanders
Solved: stated here without proof.
From [Sa21] it is known that there is always such an S with \(|S| \gt (\log |A|)^{1+c}\).
theorem green_2_lower_bound_sanders :
∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, ∀ A : Finset ℤ, A.card = n →
maxRestrictedSumAvoidingSubsetSize A ≥ Real.log n ^ (1 + c)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/2.lean, line 67.
Green2.green_2_upper_bound_erdos
Solved: stated here without proof.
From [Er65] it is known that \(M(A) \le \frac{1}{3}|A| + O(1)\).
theorem green_2_upper_bound_erdos :
∃ C : ℝ, ∀ᶠ n in atTop, ∃ A : Finset ℤ, A.card = n ∧
(maxRestrictedSumAvoidingSubsetSize A : ℝ) ≤ A.card / 3 + C
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/2.lean, line 76.
Green2.green_2_upper_bound_choi
Solved: stated here without proof.
From [Ch71] it is known that \(M(A) \le |A|^{2/5 + o(1)}\).
theorem green_2_upper_bound_choi :
∃ (o : ℕ → ℝ) (_ : Tendsto o atTop (𝓝 0)), ∀ᶠ n in atTop, ∃ A : Finset ℤ, A.card = n ∧
(maxRestrictedSumAvoidingSubsetSize A : ℝ) ≤ A.card ^ (2 / 5 + o A.card)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/2.lean, line 90.
Green2.green_2_upper_bound_ruzsa
Solved: stated here without proof.
From [Ru05] the best-known upper bound is \(|S| \lt e^{C \sqrt{\log |A|}}\).
theorem green_2_upper_bound_ruzsa :
∃ C > (0 : ℝ), ∀ᶠ n in atTop, ∃ A : Finset ℤ, A.card = n ∧
(maxRestrictedSumAvoidingSubsetSize A : ℝ) < Real.exp (C * Real.sqrt (Real.log A.card))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/2.lean, line 99.
Sources
TheoremBen Green's Open Problem 3#
References: - Ben Green's Open Problem 3 - [FGY26] Franchi, Leonardo and Gowers, W. T. and Yip, Fredy, Product-free subsets of \((0,1)\), arXiv:2607.06073, Theorem 1.1.
Quoted from FormalConjectures/GreensOpenProblems/3.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 1 research or textbook statement: 1 solved.
Green3.green_3
Solved: stated here without proof.
Suppose that \(A \subset [0,1]\) is open and has measure greater than \(\frac{1}{3}\). Is there a solution to \(xy = z\) with \(x, y, z \in A\)?
The answer is yes. [FGY26] prove that an open product-free subset of \((0,1)\) has measure strictly less than \(\frac{1}{3}\).
theorem green_3 :
∀ A : Set ℝ,
IsOpen A → A ⊆ Icc 0 1 → volume A > 1/3 →
∃ x y z, x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ x * y = z
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/3.lean, line 41.
Sources
TheoremBen Green's Open Problem 4#
Reference: Ben Green's Open Problem 4
Quoted from FormalConjectures/GreensOpenProblems/4.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.
Green4.green_4
Open: stated without proof.
What is the largest product-free set in the alternating group \(A_n\)?
theorem green_4 (n : ℕ) :
MaximalFor (ProdFree (M := alternatingGroup <| Fin n)) Set.ncard (green_4.answer n)
Category research open; AMS 20 Group theory and generalizations. Declared in FormalConjectures/GreensOpenProblems/4.lean, line 38.
Green4.large_green_4
Solved: stated here without proof.
In the case of large n, the problem was solved in On the largest product-free subsets of the alternating groups. Specifically, this theorem formalizes the statement of theorem 1.1 in the mentioned paper
theorem large_green_4 : ∀ᶠ n in .atTop,
∀ S, MaximalFor (ProdFree (M := alternatingGroup <| Fin n)) Set.ncard S →
∃ x I, S = extremalFamily x I ∨ S = (extremalFamily x I).image (·⁻¹)
Category research solved; AMS 20 Group theory and generalizations. Declared in FormalConjectures/GreensOpenProblems/4.lean, line 55.
Sources
TheoremBen Green's Open Problem 5#
References: - [Gr24] Green, Ben. "100 open problems." (2024). - [BaSo85] Babai L, Sós VT. Sidon sets in groups and induced subgraphs of Cayley graphs. European Journal of Combinatorics. 1985 Jun 1;6(2):101-14. - [Ke97] Kedlaya, K. S., Large product-free subsets of finite groups, J. Combin. Theory Ser. A 77 (1997), no. 2, 339–343. - [Ke09] Kedlaya, K. S., Product-free subsets of groups, then and now, Contemp. Math., 479, American Mathematical Society, Providence, RI, 2009, 169–177. - [Go08] Gowers, W. T., Quasirandom groups, Combin. Probab. Comput. 17 (2008), no. 3, 363–387.
Quoted from FormalConjectures/GreensOpenProblems/5.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.
Green5.green_5
Open: stated without proof.
Which finite groups have the smallest biggest product-free sets?
We formalise this as: determine the supremum of exponents \(\alpha\) such that every nontrivial finite group of order \(n\) contains a product-free set of size \(\geq c n^{\alpha}\) for some absolute constant \(c > 0\). (The trivial group is excluded since its only product-free subset is empty.) Kedlaya [Ke97] showed that \(\alpha = 11/14\) is admissible, and Green suggests this exponent may well be sharp; the candidate extremal family is the Ree groups \({}^2G_2(q)\), \(q = 3^{2m+1}\).
theorem green_5 :
IsLUB {α : ℝ | ∃ c > (0 : ℝ), ∀ (G : Type) [Group G] [Fintype G], Nontrivial G →
∃ S : Finset G, IsProductFree (S : Set G) ∧
c * (Fintype.card G : ℝ) ^ α ≤ (S.card : ℝ)}
green_5.answer
Category research open; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/GreensOpenProblems/5.lean, line 56.
Green5.green_5.variants.kedlaya
Solved: stated here without proof.
Kedlaya [Ke97] observed, refining some work of Babai and Sós [BaSo85], that it follows from the classification of finite simple groups that every finite group \(G\) of order \(n\) has a product-free subset of size \(\gg n^{11/14}\).
theorem green_5.variants.kedlaya :
∃ c > (0 : ℝ), ∀ (G : Type) [Group G] [Fintype G], Nontrivial G →
∃ S : Finset G, IsProductFree (S : Set G) ∧
c * (Fintype.card G : ℝ) ^ ((11 : ℝ) / 14) ≤ (S.card : ℝ)
Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/GreensOpenProblems/5.lean, line 69.
Green5.green_5.variants.sl_two
Open: stated without proof.
A good model problem would be to determine the largest product-free subsets of \(\mathrm{SL}_2(\mathbb{F}_p)\).
theorem green_5.variants.sl_two (p : ℕ) [Fact p.Prime] :
let S : Finset (SL₂ p) := (green_5.variants.sl_two.answer p)
MaximalFor (IsProductFree (M := SL₂ p)) Set.ncard (S : Set (SL₂ p))
Category research open; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/GreensOpenProblems/5.lean, line 84.
Green5.green_5.variants.gowers_sl_two
Solved: stated here without proof.
For the largest product-free subsets of \(\mathrm{SL}_2(\mathbb{F}_p)\) of order \(n\), the best-known upper bound is \(O(n^{8/9})\), due to Gowers [Go08].
theorem green_5.variants.gowers_sl_two :
∃ C > (0 : ℝ), ∀ (p : ℕ) [Fact p.Prime], ∀ S : Finset (SL₂ p),
IsProductFree (S : Set (SL₂ p)) →
(S.card : ℝ) ≤ C * (Fintype.card (SL₂ p) : ℝ) ^ ((8 : ℝ) / 9)
Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/GreensOpenProblems/5.lean, line 94.
Sources
TheoremBen Green's Open Problem 7#
Does Ulam's sequence have positive density? Can one explain the curious Fourier properties of Ulam's sequence?
References: - Ben Green's Open Problem 7 - erdosproblems.com/342
Quoted from FormalConjectures/GreensOpenProblems/7.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.
Green7.green_7.variants.positive_density
Open: stated without proof.
Does Ulam's sequence have positive density?
theorem green_7.variants.positive_density :
∀ a : ℕ → ℕ, Erdos342.IsUlamSequence a →
Set.upperDensity (Set.range a) > 0
Category research open; AMS 11 Number theory, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/GreensOpenProblems/7.lean, line 43.
Sources
TheoremGreen's Open Problem 9#
References: - [Gr24] Green, Ben. "100 open problems." (2024). - [BlSi20] Bloom, Thomas F., and Olof Sisask. "Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions." arXiv preprint arXiv:2007.03528 (2020).
Quoted from FormalConjectures/GreensOpenProblems/9.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 3 research or textbook statements: 2 open and 1 solved.
Green9.green_9_i
Solved: stated here without proof.
Problem 9 (i): is \(r_3(N) \ll N(\log N)^{-10}\)?
Solved in [BlSi20].
theorem green_9_i :
(fun (N : ℕ) ↦ (r 3 N : ℝ)) ≪ fun (N : ℕ) ↦ (N : ℝ) * (Real.log N) ^ (-10 : ℝ)
Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/GreensOpenProblems/9.lean, line 47.
Green9.green_9_ii
Open: stated without proof.
Problem 9 (ii): is \(r_5(N) \ll N(\log N)^{-c}\)?
theorem green_9_ii :
∃ c > (0 : ℝ), (fun (N : ℕ) ↦ (r 5 N : ℝ))
≪ fun (N : ℕ) ↦ (N : ℝ) * (Real.log N) ^ (-c)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/GreensOpenProblems/9.lean, line 55.
Green9.green_9_iii
Open: stated without proof.
Problem 9 (iii): is \(r_4(\mathbf{F}_5^n) \ll N^{1-c}\), where \(N=5^n\)?
theorem green_9_iii :
∃ c > (0 : ℝ), (fun (n : ℕ) ↦ ((Finset.univ : Finset (𝔽₅ n)).maxAPFreeCard 4 : ℝ))
≪ fun (n : ℕ) ↦ ((5 : ℝ) ^ n) ^ (1 - c)
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/GreensOpenProblems/9.lean, line 64.
Sources
TheoremGreen's Open Problem 12#
References: - [Gr24] Green, Ben. "100 open problems." (2024).
Quoted from FormalConjectures/GreensOpenProblems/12.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.
Green12.green_12
Open: stated without proof.
Let \(G\) be an abelian group of size \(N\), and suppose that \(A \subset G\) has density \(\alpha\). Are there at least \(\alpha^{15} N^{10}\) tuples \((x_1, \dots, x_5, y_1, \dots, y_5) \in G^{10}\) such that \(x_i + y_j \in A\) whenever \(j \in \{i, i+1, i+2\}\)?
Note: We interpret indices modulo 5.
theorem green_12 :
∀ {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G],
∀ (A : Finset G),
let N := Fintype.card G
let α := (A.card : ℝ) / N
let valid_tuples : Finset ((Fin 5 → G) × (Fin 5 → G)) := Finset.univ.filter (fun t =>
∀ i : Fin 5, ∀ j ∈ ({i, i + 1, i + 2} : Finset (Fin 5)), t.1 i + t.2 j ∈ A)
(valid_tuples.card : ℝ) ≥ α ^ 15 * (N : ℝ) ^ 10
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/12.lean, line 41.
Sources
TheoremBen Green's Open Problem 14#
References: - [Gr24] Green, Ben. "100 open problems." (2024). - [AKS14] Ahmed, Tanbir, Oliver Kullmann, and Hunter Snevily. "On the van der Waerden numbers w (2; 3, t)." Discrete Applied Mathematics 174 (2014): 27-51. - [KeMe23] Kelley, Zander, and Raghu Meka. "Strong bounds for 3-progressions." 2023 IEEE 64th Annual Symposium on Foundations of Computer Science (FOCS). IEEE, 2023. - [Hu22] Hunter, Zach. "Improved lower bounds for van der Waerden numbers." Combinatorica 42. Suppl 2 (2022): 1231-1252. - [Gr21] Green, Ben. "New lower bounds for van der Waerden numbers." Forum of Mathematics, Pi. Vol. 10. Cambridge University Press, 2022. - [Sc20] Schoen, Tomasz. "A subexponential upper bound for van der Waerden numbers W (3, k)." arXiv preprint arXiv:2006.02877 (2020). - [BLR08] Brown, Tom, Bruce M. Landman, and Aaron Robertson. "Bounds on some van der Waerden numbers." Journal of Combinatorial Theory, Series A 115.7 (2008): 1304-1309. - [LiSh10] Li, Yusheng, and Jinlong Shu. "A lower bound for off-diagonal van der Waerden numbers." Advances in Applied Mathematics 44.3 (2010): 243-247. - [Ko15] Kouril, Michal. "Leveraging FPGA clusters for SAT computations." Parallel Computing: On the Road to Exascale (2015): 525-532. - [CCH23] Chowdhury, Md Solimul, Cayden R. Codel, and Marijn J. H. Heule. "A linear weight transfer rule for local search." NASA Formal Methods (NFM 2023), Springer (2023).
Quoted from FormalConjectures/GreensOpenProblems/14.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 58 research or textbook statements: 9 open and 49 solved.
Green14.green_14_polynomial
Solved: stated here without proof.
Is \(W(k, r)\) a polynomial in \(r\), for fixed \(k\)?
We formulate this as asking if \(W(k, r)\) has polynomial growth in \(r\). The answer is no, already for \(k = 4\). Every red \(k\)-term progression with \(k \ge 3\) contains a red \(3\)-term progression, so
mixedMonoAPGuaranteeSet k r ⊆ mixedMonoAPGuaranteeSet 3 r, and both sets are nonempty by van der Waerden's theorem, so \(W(3, r) \le W(k, r)\). Polynomial growth for one \(k \ge 4\) would therefore force polynomial growth for \(k = 3\), contradictinggreen_14_polynomial_k_eq_3[Gr21, p.3].
theorem green_14_polynomial :
¬ ∀ k ≥ 4, ∃ d : ℕ, (fun r => (W k r : ℝ)) =O[atTop] fun r => (r : ℝ) ^ d
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 78.
Green14.green_14_polynomial_k_eq_3
Solved: stated here without proof.
We know \(W(3, r)\) does not have polynomial growth in \(r\) [Gr21, p.3].
theorem green_14_polynomial_k_eq_3 :
¬ ∃ d : ℕ, (fun r => (W 3 r : ℝ)) =O[atTop] fun r => (r : ℝ) ^ d
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 84.
Green14.green_14_quadratic
Solved: stated here without proof.
Is \(W(3, r) \ll r^2\)?
[Gr21] proves a superpolynomial lower bound \(W(3, r) \gg \exp(c(\log r)^{4/3-o(1)})\).
theorem green_14_quadratic :
¬ (fun r => (W 3 r : ℝ)) =O[atTop] fun r => (r : ℝ) ^ 2
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 94.
Green14.green_14_lower_bound_green
Solved: stated here without proof.
[Gr21] proved a lower bound of shape \(W(3, r) \gg \exp(c(\log r)^{4/3-o(1)})\).
theorem green_14_lower_bound_green :
∃ c : ℝ, 0 < c ∧ ∃ (o : ℕ → ℝ) (_ : Tendsto o atTop (𝓝 0)),
(fun (r : ℕ) => Real.exp (c * (Real.log r)^(4/3 - o r))) =O[atTop] fun r => (W 3 r : ℝ)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 100.
Green14.green_14_lower_bound_hunter
Solved: stated here without proof.
[Hu22] improved this to \(W(3, r) \gg \exp(c(\log r)^{2-o(1)})\).
theorem green_14_lower_bound_hunter :
∃ c : ℝ, 0 < c ∧ ∃ (o : ℕ → ℝ) (_ : Tendsto o atTop (𝓝 0)),
(fun (r : ℕ) => Real.exp (c * (Real.log r)^(2 - o r))) =O[atTop] (fun r => (W 3 r : ℝ))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 107.
Green14.green_14_lower_bound_brown_landman_robertson
Solved: stated here without proof.
[BLR08] proved \(W(3, r) \gg r^{2 - 1/\log \log r}\).
theorem green_14_lower_bound_brown_landman_robertson :
(fun (r : ℕ) => (r : ℝ)^(2 - 1 / Real.log (Real.log r))) =O[atTop] (fun r => (W 3 r : ℝ))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 114.
Green14.green_14_lower_bound_li_shu
Solved: stated here without proof.
[LiSh10] proved \(W(3, r) \gg (r / \log r)^2\).
theorem green_14_lower_bound_li_shu :
(fun (r : ℕ) => ((r : ℝ) / Real.log r)^2) =O[atTop] (fun r => (W 3 r : ℝ))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 120.
Green14.green_14_upper_bound_schoen
Solved: stated here without proof.
[Sc20] proves the upper bound \(W(3, r) < \exp(r^{1-c})\) for some \(c > 0\).
theorem green_14_upper_bound_schoen :
∃ c : ℝ, 0 < c ∧
(fun (r : ℕ) => ((W 3 r) : ℝ)) =O[atTop] (fun r => Real.exp ((r : ℝ) ^ (1 - c)))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 126.
Green14.green_14_upper_bound_kelley_meka
Solved: stated here without proof.
[KeMe23] gives a corresponding upper bound \(W(3, r) \ll \exp(C(\log r)^C)\).
theorem green_14_upper_bound_kelley_meka :
∃ C : ℝ,
(fun (r : ℕ) => ((W 3 r) : ℝ)) =O[atTop] (fun r => Real.exp (C * (Real.log r)^C))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 133.
Green14.green_14_variant_2r2
Open: stated without proof.
It remains an interesting open problem to actually write down a colouring showing (say) \(W(3, r) \ge 2r^2\) for some \(r\). [Gr24]
theorem green_14_variant_2r2 :
-- Provide a pair (r, associated coloring) that avoids the monochromatic APs
-- To show $W(3, r) > 2r^2 - 1$, we need a coloring of $\{1, \ldots, 2r^2 - 1\}$
-- that avoids monochromatic APs of length 3 and $r$.
let ans : Σ r : ℕ, Icc 1 (2 * r^2 - 1) → Fin 2 := green_14_variant_2r2.answer
let r := ans.1
let c := ans.2
3 ≤ r ∧
¬ ((∃ s : Finset (Icc 1 (2 * r^2 - 1)), ({(s' : ℕ) | s' ∈ s}).IsAPOfLength 3 ∧ ∀ x ∈ s, c x = 0) ∨
(∃ s : Finset (Icc 1 (2 * r^2 - 1)), ({(s' : ℕ) | s' ∈ s}).IsAPOfLength r ∧ ∀ x ∈ s, c x = 1))
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 145.
Green14.W_3_3
Solved: stated here; a Lean proof is at https://github.com/Konamiu/formal-conjectures/blob/d6a68af97f6ca7856d892569d88ab1ecc8e927bf/FormalConjectures/GreensOpenProblems/14.lean#L289.
\(W(3, 3) = 9\) from [AKS14].
theorem W_3_3 : W 3 3 = 9
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 162.
Green14.W_3_4
Solved: stated here; a Lean proof is at https://github.com/Konamiu/formal-conjectures/blob/d6a68af97f6ca7856d892569d88ab1ecc8e927bf/FormalConjectures/GreensOpenProblems/14.lean#L301.
\(W(3, 4) = 18\) from [AKS14].
theorem W_3_4 : W 3 4 = 18
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 168.
Green14.W_3_5
Solved: stated here; a Lean proof is at https://github.com/Konamiu/formal-conjectures/blob/d6a68af97f6ca7856d892569d88ab1ecc8e927bf/FormalConjectures/GreensOpenProblems/14.lean#L313.
\(W(3, 5) = 22\) from [AKS14].
theorem W_3_5 : W 3 5 = 22
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 174.
Green14.W_3_6
Solved: stated here without proof.
\(W(3, 6) = 32\) from [AKS14].
theorem W_3_6 : W 3 6 = 32
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 178.
Green14.W_3_7
Solved: stated here without proof.
\(W(3, 7) = 46\) from [AKS14].
theorem W_3_7 : W 3 7 = 46
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 182.
Green14.W_3_8
Solved: stated here without proof.
\(W(3, 8) = 58\) from [AKS14].
theorem W_3_8 : W 3 8 = 58
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 186.
Green14.W_3_9
Solved: stated here without proof.
\(W(3, 9) = 77\) from [AKS14].
theorem W_3_9 : W 3 9 = 77
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 190.
Green14.W_3_10
Solved: stated here without proof.
\(W(3, 10) = 97\) from [AKS14].
theorem W_3_10 : W 3 10 = 97
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 194.
Green14.W_3_11
Solved: stated here without proof.
\(W(3, 11) = 114\) from [AKS14].
theorem W_3_11 : W 3 11 = 114
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 198.
Green14.W_3_12
Solved: stated here without proof.
\(W(3, 12) = 135\) from [AKS14].
theorem W_3_12 : W 3 12 = 135
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 202.
Green14.W_3_13
Solved: stated here without proof.
\(W(3, 13) = 160\) from [AKS14].
theorem W_3_13 : W 3 13 = 160
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 206.
Green14.W_3_14
Solved: stated here without proof.
\(W(3, 14) = 186\) from [AKS14].
theorem W_3_14 : W 3 14 = 186
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 210.
Green14.W_3_15
Solved: stated here without proof.
\(W(3, 15) = 218\) from [AKS14].
theorem W_3_15 : W 3 15 = 218
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 214.
Green14.W_3_16
Solved: stated here without proof.
\(W(3, 16) = 238\) from [AKS14].
theorem W_3_16 : W 3 16 = 238
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 218.
Green14.W_3_17
Solved: stated here without proof.
\(W(3, 17) = 279\) from [AKS14].
theorem W_3_17 : W 3 17 = 279
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 222.
Green14.W_3_18
Solved: stated here without proof.
\(W(3, 18) = 312\) from [AKS14].
theorem W_3_18 : W 3 18 = 312
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 226.
Green14.W_3_19
Solved: stated here without proof.
\(W(3, 19) = 349\) from [AKS14].
theorem W_3_19 : W 3 19 = 349
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 230.
Green14.W_3_20_lower
Solved: stated here; a Lean proof is at https://github.com/DomTheDeveloper/formal-conjectures/blob/013a0f04de0057d2bd1034c7cc4caf10ac8dc2cf/FormalConjectures/GreensOpenProblems/Green14FastKernel20.lean.
\(W(3, 20) \ge 389\) from [AKS14, Table 2], proved by an explicit good partition. A kernel-checked Lean proof from the certificate was given by Dominic Dabish.
theorem W_3_20_lower : W 3 20 ≥ 389
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 239.
Green14.W_3_20
Solved: stated here without proof.
\(W(3, 20) = 389\), conjectured in [AKS14, Table 2] and established by Kouril [Ko15] using FPGA-based SAT solving.
theorem W_3_20 : W 3 20 = 389
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 244.
Green14.W_3_21_lower
Solved: stated here without proof.
\(W(3, 21) \ge 416\) from [AKS14, Table 2], proved by an explicit good partition.
theorem W_3_21_lower : W 3 21 ≥ 416
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 248.
Green14.W_3_21_eq
Open: stated without proof.
[AKS14, Table 2] conjectures that \(W(3, 21) = 416\).
theorem W_3_21_eq : W 3 21 = 416
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 252.
Green14.W_3_22_lower
Solved: stated here without proof.
\(W(3, 22) \ge 464\) from [AKS14, Table 2], proved by an explicit good partition.
theorem W_3_22_lower : W 3 22 ≥ 464
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 256.
Green14.W_3_22_eq
Open: stated without proof.
[AKS14, Table 2] conjectures that \(W(3, 22) = 464\).
theorem W_3_22_eq : W 3 22 = 464
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 260.
Green14.W_3_23_lower
Solved: stated here without proof.
\(W(3, 23) \ge 516\) from [AKS14, Table 2], proved by an explicit good partition.
theorem W_3_23_lower : W 3 23 ≥ 516
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 264.
Green14.W_3_23_eq
Open: stated without proof.
[AKS14, Table 2] conjectures that \(W(3, 23) = 516\).
theorem W_3_23_eq : W 3 23 = 516
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 268.
Green14.W_3_24_lower
Solved: stated here without proof.
\(W(3, 24) \ge 593\) from [AKS14, Table 2], proved by an explicit good partition.
theorem W_3_24_lower : W 3 24 ≥ 593
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 272.
Green14.W_3_24_eq
Open: stated without proof.
[AKS14, Table 2] conjectures that \(W(3, 24) = 593\).
theorem W_3_24_eq : W 3 24 = 593
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 276.
Green14.W_3_25_lower
Solved: stated here without proof.
\(W(3, 25) \ge 656\) from [AKS14, Table 2], proved by an explicit good partition.
theorem W_3_25_lower : W 3 25 ≥ 656
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 280.
Green14.W_3_25_eq
Open: stated without proof.
[AKS14, Table 2] conjectures that \(W(3, 25) = 656\).
theorem W_3_25_eq : W 3 25 = 656
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 284.
Green14.W_3_26_lower
Solved: stated here without proof.
\(W(3, 26) \ge 727\) from [AKS14, Table 2], proved by an explicit good partition.
theorem W_3_26_lower : W 3 26 ≥ 727
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 288.
Green14.W_3_26_eq
Open: stated without proof.
[AKS14, Table 2] conjectures that \(W(3, 26) = 727\).
theorem W_3_26_eq : W 3 26 = 727
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 292.
Green14.W_3_27_lower
Solved: stated here without proof.
\(W(3, 27) \ge 770\) from [AKS14, Table 2], proved by an explicit good partition.
theorem W_3_27_lower : W 3 27 ≥ 770
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 296.
Green14.W_3_27_eq
Open: stated without proof.
[AKS14, Table 2] conjectures that \(W(3, 27) = 770\).
theorem W_3_27_eq : W 3 27 = 770
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 300.
Green14.W_3_28_lower
Solved: stated here without proof.
\(W(3, 28) \ge 827\) from [AKS14, Table 2], proved by an explicit good partition.
theorem W_3_28_lower : W 3 28 ≥ 827
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 304.
Green14.W_3_28_eq
Open: stated without proof.
[AKS14, Table 2] conjectures that \(W(3, 28) = 827\).
theorem W_3_28_eq : W 3 28 = 827
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 308.
Green14.W_3_29_lower
Solved: stated here without proof.
\(W(3, 29) \ge 868\) from [AKS14, Table 2], proved by an explicit good partition.
theorem W_3_29_lower : W 3 29 ≥ 868
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 312.
Green14.W_3_29_eq
Solved: stated here without proof.
[AKS14, Table 2] conjectures that \(W(3, 29) = 868\). This is false: Chowdhury, Codel, and Heule [CCH23, Section 6.3] found a good partition of \(\{1, \ldots, 868\}\), so \(W(3, 29) \geq 869\).
theorem W_3_29_eq : ¬ W 3 29 = 868
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 317.
Green14.W_3_30_lower
Solved: stated here without proof.
\(W(3, 30) \ge 903\) from [AKS14, Table 2], proved by an explicit good partition.
theorem W_3_30_lower : W 3 30 ≥ 903
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 321.
Green14.W_3_30_eq
Solved: stated here without proof.
[AKS14, Table 2] conjectures that \(W(3, 30) = 903\). This is false: Chowdhury, Codel, and Heule [CCH23, Section 6.3] found a good partition of \(\{1, \ldots, 903\}\), so \(W(3, 30) \geq 904\).
theorem W_3_30_eq : ¬ W 3 30 = 903
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 326.
Green14.W_3_31_lower
Solved: stated here without proof.
\(W(3, 31) > 930\) from [AKS14, Table 3], proved by an explicit good partition.
theorem W_3_31_lower : W 3 31 > 930
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 332.
Green14.W_3_32_lower
Solved: stated here without proof.
\(W(3, 32) > 1006\) from [AKS14, Table 3], proved by an explicit good partition.
theorem W_3_32_lower : W 3 32 > 1006
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 336.
Green14.W_3_33_lower
Solved: stated here without proof.
\(W(3, 33) > 1063\) from [AKS14, Table 3], proved by an explicit good partition.
theorem W_3_33_lower : W 3 33 > 1063
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 340.
Green14.W_3_34_lower
Solved: stated here without proof.
\(W(3, 34) > 1143\) from [AKS14, Table 3], proved by an explicit good partition.
theorem W_3_34_lower : W 3 34 > 1143
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 344.
Green14.W_3_35_lower
Solved: stated here without proof.
\(W(3, 35) > 1204\) from [AKS14, Table 3], proved by an explicit good partition.
theorem W_3_35_lower : W 3 35 > 1204
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 348.
Green14.W_3_36_lower
Solved: stated here without proof.
\(W(3, 36) > 1257\) from [AKS14, Table 3], proved by an explicit good partition.
theorem W_3_36_lower : W 3 36 > 1257
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 352.
Green14.W_3_37_lower
Solved: stated here without proof.
\(W(3, 37) > 1338\) from [AKS14, Table 3], proved by an explicit good partition.
theorem W_3_37_lower : W 3 37 > 1338
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 356.
Green14.W_3_38_lower
Solved: stated here without proof.
\(W(3, 38) > 1378\) from [AKS14, Table 3], proved by an explicit good partition.
theorem W_3_38_lower : W 3 38 > 1378
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 360.
Green14.W_3_39_lower
Solved: stated here without proof.
\(W(3, 39) > 1418\) from [AKS14, Table 3], proved by an explicit good partition.
theorem W_3_39_lower : W 3 39 > 1418
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/14.lean, line 364.
Sources
TheoremGreen's Open Problem 15#
References: - [Gr24] Green, Ben. "100 open problems." (2024). - [BJP14] T. Brown, V. Jungić and A. Poelstra, "On double 3-term arithmetic progressions", Integers 14 (2014), Paper No. A43. - [CCS14] J. Cassaigne, J. D. Currie, L. Schaeffer and J. Shallit, "Avoidance of additive cubes and related results", Adv. in Appl. Math. 56 (2014), 25–66.
Quoted from FormalConjectures/GreensOpenProblems/15.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.
Green15.green_15
Open: stated without proof.
Does there exist a Lipschitz function \(f : \mathbb{N} \to \mathbb{Z}\) whose graph \(\Gamma = \{(n, f(n)) : n \in \mathbb{N}\} \subseteq \mathbb{Z}^2\) is free of 3-term progressions?
theorem green_15 :
∃ K : ℝ≥0, ∃ f : ℕ → ℤ, LipschitzWith K f ∧
IsAPOfLengthFree {((n, f n) : ℤ × ℤ) | (n : ℕ)} 3
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/15.lean, line 43.
Green15.green_15_ap4
Solved: stated here without proof.
The answer is YES for 4-term progressions [BJP14].
theorem green_15_ap4 :
∃ K : ℝ≥0, ∃ f : ℕ → ℤ, LipschitzWith K f ∧
IsAPOfLengthFree {((n, f n) : ℤ × ℤ) | (n : ℕ)} 4
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/15.lean, line 52.
Sources
TheoremBen Green's Open Problem 16#
References: * Ben Green's Open Problem 16 * [Ruzsa](I. Z. Ruzsa, Solving a linear equation in a set of integers. I. Acta Arith. 65 (1993), no. 3, 259–282.) * [Schoen and Sisask](T. Schoen and O. Sisask, Roth’s theorem for four variables and additive structures in sums of sparse sets Forum of Mathematics, Sigma (2016), Vol. 4, e5, 28 pages.) * [Yufei Zhao](Via Personal Communication with Ben Green)
Quoted from FormalConjectures/GreensOpenProblems/16.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.
Green16.green_16
Open: stated without proof.
What is the largest subset of \([N]\) with no solution to \(x + 3y = 2z + 2w\) in distinct integers \(x, y, z, w\)?
theorem green_16 (N : ℕ) :
∃ A : Finset ℕ, A ⊆ Icc 1 N ∧ SolutionFree A ∧
A.card = green_16.answer N ∧
MaximalFor (fun B => B ⊆ Icc 1 N ∧ SolutionFree B) Finset.card A
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/16.lean, line 50.
Green16.green_16_lower_bound
Solved: stated here without proof.
From [Ruzsa] \(f(N) \gg N^{1/2}\).
theorem green_16_lower_bound :
(fun N ↦ (N : ℝ) ^ (1 / 2 : ℝ)) ≪ fun N ↦ (f N : ℝ)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/16.lean, line 58.
Green16.green_16_upper_bound
Solved: stated here without proof.
From [Schoen and Sisask] \(f(N) \ll N \cdot e^{-c(\log N)^{1/7}}\).
theorem green_16_upper_bound :
∃ c > (0 : ℝ), (fun N ↦ (f N : ℝ)) ≪ fun N ↦ (N : ℝ) * exp (-c * (log N) ^ (1 / 7 : ℝ))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/16.lean, line 64.
Green16.zhao_question
Open: stated without proof.
From [Yufei Zhao]: Is there a subset of \(\{1, \ldots, N\}\) of size \(N^{1/3 - o(1)}\) with no nontrivial solutions to \(x + 2y + 3z = x' + 2y' + 3z'\)?
theorem zhao_question :
∃ h : ℕ → ℝ, Tendsto h atTop (𝓝 0) ∧
∀ᶠ N in atTop, (g N : ℝ) ≥ (N : ℝ) ^ (1 / 3 - h N)
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/16.lean, line 86.
Sources
TheoremBen Green's Open Problem 18#
Reference: - [Gr26] Ben Green's Open Problem 18 - [Au16] Austin, Tim. "Ajtai–Szemerédi theorems over quasirandom groups." Recent trends in combinatorics. Cham: Springer International Publishing, 2016. 453-484. - [So13] Solymosi, Jozsef. "Roth-type theorems in finite groups." European Journal of Combinatorics 34.8 (2013): 1454-1458. - [Go01] Gowers, William T. "A new proof of Szemerédi's theorem." Geometric & Functional Analysis GAFA 11.3 (2001): 465-588.
Quoted from FormalConjectures/GreensOpenProblems/18.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.
Green18.green_18
Open: stated without proof.
Suppose that \(G\) is a finite group, and let \(A \subset G \times G\) be a subset of density \(\alpha\). Is it true that there are \(\gg_\alpha |G|^3\) triples \(x, y, g\) such that \((x, y), (gx, y), (x, gy)\) all lie in \(A\)?
Note: A is taken as \(\alpha\)-dense, i.e. \(|A| \ge \alpha |G|^2\) [Au16, Question 2]
theorem green_18 :
∀ α > 0, ∃ c > 0, ∃ m₀ : ℕ,
∀ (G : Type*) [Group G] [Fintype G] [DecidableEq G] (A : Finset (G × G)),
Fintype.card G ≥ m₀ →
(A.card : ℝ) ≥ α * (Fintype.card G) ^ 2 →
(numNaiveCorners A : ℝ) ≥ c * (Fintype.card G) ^ 3
Category research open; AMS 05 Combinatorics, 11 Number theory, 20 Group theory and generalizations. Declared in FormalConjectures/GreensOpenProblems/18.lean, line 60.
Green18.green_18.bmz_corners
Solved: stated here without proof.
[So13] proved this is true for "BMZ corners". Follows from the proof of Theorem 2.1, p.1456-1457.
theorem green_18.bmz_corners : ∀ α > 0, ∃ c > 0, ∃ m₀ : ℕ,
∀ (G : Type*) [Group G] [Fintype G] [DecidableEq G] (A : Finset (G × G)),
Fintype.card G ≥ m₀ →
(A.card : ℝ) ≥ α * (Fintype.card G) ^ 2 →
(numBmzCorners A : ℝ) ≥ c * (Fintype.card G) ^ 3
Category research solved; AMS 05 Combinatorics, 11 Number theory, 20 Group theory and generalizations. Declared in FormalConjectures/GreensOpenProblems/18.lean, line 82.
Sources
TheoremBen Green's Open Problem 19#
References: - [Gr26] Ben Green's Open Problems - [FSS20] Fox, Jacob, et al. "Triforce and corners." Mathematical Proceedings of the Cambridge Philosophical Society. Vol. 169. No. 1. Cambridge University Press, 2020. - [Ma21] Mandache, Matei. "A variant of the Corners theorem." Mathematical Proceedings of the Cambridge Philosophical Society. Vol. 171. No. 3. Cambridge University Press, 2021. - [Ch11] Chu, Qing. "Multiple recurrence for two commuting transformations." Ergodic Theory and Dynamical Systems 31.3 (2011): 771-792.
Quoted from FormalConjectures/GreensOpenProblems/19.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.
Green19.green_19
Solved: stated here without proof.
What is \(C\), the infimum of all exponents \(c\) for which the following is true, uniformly for \(0 < \alpha < 1\)? Suppose that \(A \subset \mathbb{F}_2^n \times \mathbb{F}_2^n\) is a set of density \(\alpha\). Write \(N := 2^n\). Then there is some \(d \neq 0\) such that \(A\) contains \(\gg \alpha^c N^2\) corners \((x,y), (x,y+d), (x+d,y)\).
This question has been resolved by [FSS20], showing that \(C = 4\).
theorem green_19 : C = 4
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/19.lean, line 83.
Green19.green_19.lower
Proved here.
[Ma21] showed that \(3.13 \leq C\). This also follows from
green_19.
theorem green_19.lower : C >= 3.13
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/19.lean, line 88.
Green19.green_19.upper
Proved here.
[Ma21] showed that \(C \leq 4\). This also follows from
green_19.
theorem green_19.upper : C <= 4
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/19.lean, line 94.
Sources
TheoremBen Green's Open Problem 21#
References: - [Gr24] Green, Ben. "100 open problems." (2024). - [Ra33] Rado, Richard, Studien zur Kombinatorik. Math. Zeit. 36 (1933), 424-480. - [FoKl06] Fox, Jacob and Kleitman, Daniel, On Rado's boundedness conjecture. J. Combin. Theory Ser. A 113 (2006), no. 1, 84-100. - [ElJo23] Ellis, David and Johnson, Robert (editors), A collection of open problems in celebration of Imre Leader's 60th birthday. arXiv preprint arXiv:2310.18163 (2023).
Quoted from FormalConjectures/GreensOpenProblems/21.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: 4 open and 1 solved. It also has 4 test statements, counted here but not shown.
Green21.green_21
Open: stated without proof.
Suppose that \(a_1, \dots, a_k\) are integers which do not satisfy Rado's condition: thus if \(\sum_{i \in I} a_i = 0\) then \(I = \emptyset\). It then follows from Rado's theorem that the equation \(a_1x_1 + \cdots + a_kx_k = 0\) is not partition regular. Write \(c(a_1, \dots, a_k)\) for the least number of colours required in order to colour \(\mathbb{N}\) so that there is no monochromatic solution to \(a_1x_1 + \cdots + a_kx_k = 0\). Is \(c(a_1, \dots, a_k)\) bounded in terms of \(k\) only?
This problem, which is known as Rado's boundedness conjecture, dates back to 1933 [Ra33]. It is open for all \(k \geq 4\).
theorem green_21 : ∃ B : ℕ → ℕ, ∀ (k : ℕ) (a : Fin k → ℤ),
¬ RadoCondition a → minColours a ≤ B k
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/21.lean, line 78.
Green21.green_21.variants.fox_kleitman
Solved: stated here without proof.
The answer was shown to be affirmative for \(k = 3\) by Fox and Kleitman [FoKl06], who showed that \(c(a_1, a_2, a_3) \leq 24\).
theorem green_21.variants.fox_kleitman (a : Fin 3 → ℤ) (ha : ¬ RadoCondition a) :
minColours a ≤ 24
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/21.lean, line 87.
Green21.green_21.variants.fox_kleitman_sharp
Open: stated without proof.
Green [Gr24] is not sure that the constant \(24\) of [FoKl06] is sharp, and remarks that it might be interesting to determine the sharp constant.
The largest value of \(c(a_1, a_2, a_3)\) is attained, since by
green_21.variants.fox_kleitmanthe values form a non-empty set of naturals bounded above by \(24\).
theorem green_21.variants.fox_kleitman_sharp :
IsGreatest {c | ∃ a : Fin 3 → ℤ, ¬ RadoCondition a ∧ minColours a = c}
green_21.variants.fox_kleitman_sharp.answer
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/21.lean, line 101.
Green21.green_21.variants.fox_kleitman_modular
Open: stated without proof.
A question [FoKl06, Conjecture 5] of Fox and Kleitman, which they call a 'modular analogue' of Rado's Boundedness Conjecture. Let \(k > 0\), let \(p\) be a prime, and suppose that \(a_1, \dots, a_k\) are integers with \(\sum_{i \in I} a_i \equiv 0 \pmod p\) only when \(I = \emptyset\). Does there exist an \(f(k)\)-colouring of \((\mathbb{Z}/p\mathbb{Z})^*\) with no monochromatic solution to \(a_1x_1 + \cdots + a_kx_k = 0\)? This seems to be open even when \(k = 3\); Green [Gr24] suspects the answer may be negative.
The point of the question is that the number of colours \(f(k)\) must not depend on \(p\).
The arity \(k\) is required to be positive, as in [FoKl06]: for \(k = 0\) the empty tuple is a monochromatic solution with sum \(0\) for every colouring, so no \(f(0)\) could work.
theorem green_21.variants.fox_kleitman_modular : ∃ f : ℕ → ℕ,
∀ (k p : ℕ), 0 < k → p.Prime → ∀ a : Fin k → ℤ,
(∀ I : Finset (Fin k), (p : ℤ) ∣ ∑ i ∈ I, a i → I = ∅) →
∃ col : (ZMod p)ˣ → Fin (f k), ∀ x : Fin k → (ZMod p)ˣ,
(∀ i j, col (x i) = col (x j)) → ∑ i, (a i : ZMod p) * (x i : ZMod p) ≠ 0
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/21.lean, line 121.
Green21.green_21.variants.milicevic
Open: stated without proof.
Milićević [ElJo23, Conjecture 11.1] conjectures the following 2-adic variant. For any \(k \in \mathbb{N}\), there exists \(K = K(k)\) such that the following is true. Let \(r\) be a positive integer, and let \(a_1, \dots, a_k \in \mathbb{Z}/2^r\mathbb{Z}\). Let \(d\) be the largest integer such that \(\sum_{i \in I} a_i \equiv 0 \pmod{2^d}\) for some non-empty subset \(I \subset [k]\). Then there is a \(K\)-colouring of \(\mathbb{Z}/2^r\mathbb{Z}\) such that all monochromatic solutions \(x = (x_1, \dots, x_k)\) to the equation \(a_1x_1 + \cdots + a_kx_k = 0\) satisfy \(x_i \equiv 0 \pmod{2^{r-d}}\) for all \(i = 1, \dots, k\).
Milićević remarks that, if true, this would imply the Rado boundedness conjecture by a compactness argument.
theorem green_21.variants.milicevic : ∀ k : ℕ, ∃ K : ℕ, ∀ r : ℕ, 0 < r →
∀ a : Fin k → ZMod (2 ^ r), ∃ col : ZMod (2 ^ r) → Fin K,
∀ x : Fin k → ZMod (2 ^ r), (∀ i j, col (x i) = col (x j)) →
∑ i, a i * x i = 0 → ∀ i, 2 ^ (r - maxDepth a) ∣ (x i).val
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/21.lean, line 151.
Sources
TheoremGreen's Open Problem 22#
References: - [Gr26] Ben Green's Open Problems - [Mo17] Moreira, Joel. "Monochromatic sums and products in N." Annals of Mathematics 185.3 (2017): 1069-1090. - [GrSa25] Green, Ben, and Mehtaab Sawhney. "Bounds for monochromatic solutions to ${x+ y, xy} $." arXiv preprint arXiv:2511.09365 (2025). - [Ri25] Richter, Florian K. "Sums and products in sets of positive density." arXiv preprint arXiv:2507.00515 (2025). - [BoSa24] Bowen, Matt, and Marcin Sabok. "Monochromatic products and sums in the rationals." Forum of Mathematics, Pi. Vol. 12. Cambridge University Press, 2024. - [Bo25] Bowen, Matt. "Monochromatic products and sums in 2-colorings of N." Advances in Mathematics 462 (2025): 110095. - [Al23] Alweiss, Ryan. "Monochromatic Sums and Products over $\mathbb {Q} $." arXiv preprint arXiv:2307.08901 (2023).
Quoted from FormalConjectures/GreensOpenProblems/22.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 4 research or textbook statements: 1 open and 3 solved.
Green22.green_22
Open: stated without proof.
If \(\{1, \ldots, N\}\) is \(r\)-coloured then, for \(N \geqslant N_0(r)\), there are integers \(x, y \geqslant 3\) such that \(x + y, xy\) have the same colour.
Find reasonable bounds for \(N_0(r)\). The goal is to improve upon the Green-Sawhney bound.
theorem green_22 :
∀ᶠ r in atTop, N₀ r ≤ green_22.answer r ∧
green_22.answer =o[atTop] GreenSawhneyBound
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/22.lean, line 76.
Green22.green_22.variants.green_sawhney_bound
Solved: stated here without proof.
[GrSa25, Theorem 1.1] found a permissible upper bound.
theorem green_22.variants.green_sawhney_bound :
∀ᶠ r in atTop, N₀ r ≤ GreenSawhneyBound r
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/22.lean, line 85.
Green22.green_22.variants.moreira_infinite
Solved: stated here without proof.
[Mo17, Corollary 1.5] For any finite coloring of \(\mathbb{N}\) there exist (infinitely many) \(x, y \in \mathbb{N}\) such that \(\{xy, x + y\}\) is monochromatic.
This guarantees that \(N_0(r)\) is well-defined.
Note: [Mo17] also establishes that \(x\) is of the same colour.
theorem green_22.variants.moreira_infinite :
∀ (r : ℕ) (coloring : ℕ → Fin r),
Set.Infinite { p : ℕ × ℕ |
0 < p.1 ∧ 0 < p.2 ∧
coloring p.1 = coloring (p.1 * p.2) ∧
coloring p.1 = coloring (p.1 + p.2) }
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/22.lean, line 98.
Green22.green_22.variants.lower_nine
Solved: stated here without proof.
Since \(x, y \geq 3\), we must have \(xy \geq 9\), so every \(N\) such that all \(r\)-colourings of \(\{1, \ldots, N\}\) have the monochromatic sum-product property is at least \(9\). In particular \(N_0(r) \geq 9\) once \(N_0(r)\) is well-defined, which follows from [Mo17].
The bound is stated for every such \(N\) and not as
9 ≤ N₀ r: sincesInf ∅ = 0inℕ, the latter is equivalent to the existence of such an \(N\).
theorem green_22.variants.lower_nine : ∀ r : ℕ, r ≠ 0 →
∀ N : ℕ, (∀ c : Icc 1 N → Fin r, HasMonochromaticSumProduct N r c) → 9 ≤ N
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/22.lean, line 115.
Sources
TheoremGreen's Open Problem 23#
References: - Green, Ben. "100 open problems." (2024). - [FrKlMo25] Frantzikinakis, N., O. Klurman, and J. Moreira. "Partition regularity of Pythagorean pairs." Forum of Mathematics, Pi 13. Cambridge University Press (2025).
Quoted from FormalConjectures/GreensOpenProblems/23.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.
Green23.green_23
Solved: stated here without proof.
Suppose that \(\mathbb{N}\) is finitely coloured. Are there \(x,y\) of the same colour such that \(x^2 + y^2\) is a square?
Solved in [FrKlMo25].
theorem green_23 :
-- For every finite colouring of the natural numbers
∀ (k : ℕ) (c : ℕ → Fin k),
-- there exist two numbers of the same colour whose squares sum to a square
∃ x y : ℕ,
0 < x ∧ 0 < y ∧ -- Exclude trivial x^2 + 0^2 = x^2 solution
c x = c y ∧ -- Same colour
IsSquare (x^2 + y^2)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/23.lean, line 39.
Sources
TheoremGreen's Open Problem 24#
References: - Green, Ben. "100 open problems." (2024). - [Aa19] Aaronson, James. "Maximising the number of solutions to a linear equation in a set of integers." Bulletin of the London Mathematical Society 51.4 (2019): 577-594. - [HaL28] Hardy, G. H., and J. E. Littlewood. "Notes on the theory of series (VIII): an inequality." Journal of the London Mathematical Society 1.2 (1928): 105-110.
Quoted from FormalConjectures/GreensOpenProblems/24.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.
Green24.green_24
Open: stated without proof.
If \(A\) is a set of \(n\) integers, what is the maximum number of affine translates of the set \(\lbrace 0,1,3 \rbrace\) that \(A\) can contain?
Conjectured in [Aa19] p.579: \(\left(\frac{1}{3} + o(1)\right) n^2\).
theorem green_24 : ∀ n, max013AffineTranslates n = green_24.answer n
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/24.lean, line 58.
Green24.variants.upper_trivial
Proved here.
From [Aa19] p.577: the trivial upper bound is \(n^2\) (non asymptotic).
theorem upper_trivial {n : ℕ} : max013AffineTranslates n ≤ n ^ 2
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/24.lean, line 68.
Green24.variants.upper_HL
Solved: stated here without proof.
Asymptotic upper bound (1.2) in [Aa19]. Named after Hardy and Littlewood [HaL28].
theorem upper_HL : gamma ≤ 3/4
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/24.lean, line 82.
Green24.variants.lower_HL
Solved: stated here without proof.
Asymptotic lower bound (1.2) in [Aa19]. Named after Hardy and Littlewood [HaL28].
theorem lower_HL : gamma ≥ 1/12
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/24.lean, line 87.
Green24.variants.conjecture
Open: stated without proof.
Conjecture p.579 in [Aa19]: \(\left(\frac{1}{3} + o(1)\right) n^2\).
theorem conjecture : gamma = 1/3
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/24.lean, line 92.
Sources
TheoremGreen's Open Problem 25#
References: - [Gr24] Green, Ben. "100 open problems." (2024). - [ESS89] Erdős, Pál, András Sárközy, and V. T. Sós. "On a conjecture of Roth and some related problems I." Irregularities of partitions. Berlin, Heidelberg: Springer Berlin Heidelberg, 1989. 47-59. - [Ru04] Ruzsa, Imre Z. "A problem on restricted sumsets." CONTEMPORARY MATHEMATICS 342 (2004): 245-248.
Quoted from FormalConjectures/GreensOpenProblems/25.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 and 3 solved.
Green25.green_25
Open: stated without proof.
For which values of \(k\) is the following true: whenever we partition \([N] = A_1 \cup \dots \cup A_k\), \(\left|\bigcup^k_{i=1} (A_i \hat{+} A_i)\right| \geq \frac{1}{10} N\)?
theorem green_25 : {k : ℕ → ℕ | ∀ᶠ N in atTop, Property25 (k N) N} = green_25.answer
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/25.lean, line 60.
Green25.green_25.upper
Open: stated without proof.
We conjecture that the best-known upper bound can be lowered.
theorem green_25.upper :
-- Ensure k is a valid partition size
(∀ᶠ N in atTop, 1 ≤ green_25.upper.answer N ∧ green_25.upper.answer N ≤ N) ∧
(fun N => (green_25.upper.answer N : ℝ)) =o[atTop] bestUpper ∧
¬ ∀ᶠ N in atTop, Property25 (green_25.upper.answer N) N
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/25.lean, line 67.
Green25.green_25.lower
Open: stated without proof.
We conjecture that the best-known lower bound can be raised.
theorem green_25.lower :
(bestLower =o[atTop] green_25.lower.answer) ∧
(∀ᶠ N in atTop, 1 ≤ green_25.lower.answer N ∧ green_25.lower.answer N ≤ N) ∧
∀ k : ℕ → ℕ,
(∀ᶠ N in atTop, 1 ≤ k N ∧ k N ≤ N) ∧
((fun N => (k N : ℝ)) ≪ green_25.lower.answer) →
∀ᶠ N in atTop, Property25 (k N) N
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/25.lean, line 78.
Green25.green_25.variants.lower_ess89
Solved: stated here without proof.
For \(k \ll \log \log N\), this is true [Gr24].
NOTE: [ESS89] derive a precise constant for which this is true, but \(\ll\) would imply that it works for any constant. We thus prefer a little-o statement.
theorem green_25.variants.lower_ess89 :
∀ k : ℕ → ℕ,
(∀ᶠ N in atTop, 1 ≤ k N ∧ k N ≤ N) ∧ -- Ensure Property25 is not False due to non-existent partitions
(fun N => (k N : ℝ)) =o[atTop] bestLower →
∀ᶠ N in atTop, Property25 (k N) N
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/25.lean, line 94.
Green25.green_25.variants.upper_ess89
Solved: stated here without proof.
For \(k \gg N / \log N\), it need not be true [Gr24].
We formalize by enforcing a \(N / \log N\) growth rate on \(k(N)\). This avoids cases like \(k(N) = N\) or \(N-1\), which produce trivial counter examples with singletons and thus empty restricted sumsets.
theorem green_25.variants.upper_ess89 :
∃ k : ℕ → ℕ,
(∀ᶠ N in atTop, 1 ≤ k N ∧ k N ≤ N) ∧
(fun N => (k N : ℝ)) =Θ[atTop] bestUpper ∧
¬ ∀ᶠ N in atTop, Property25 (k N) N
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/25.lean, line 108.
Green25.green_25.variants.upper_pow_23_40
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/green-25-upper-bound/blob/3a54a688dfc4d7b9c8990bbaeb1a124c075454e4/lean/Green25UpperFC.lean#L3043-L3051.
For \(k(N) = \lceil N^{23/40} \rceil\), it need not be true: for all sufficiently large \(N\) there is a partition of \([N]\) into \(\lceil N^{23/40} \rceil\) parts with \(\left|\bigcup^k_{i=1} (A_i \hat{+} A_i)\right| < \frac{1}{10} N\). In particular, the best-known upper bound \(N / \log N\) can be lowered.
theorem green_25.variants.upper_pow_23_40 :
let k : ℕ → ℕ := fun N => Nat.ceil ((N : ℝ) ^ (23 / 40 : ℝ))
(∀ᶠ N in atTop, 1 ≤ k N ∧ k N ≤ N) ∧
(fun N => (k N : ℝ)) =o[atTop] bestUpper ∧
∀ᶠ N in atTop, ¬ Property25 (k N) N
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/25.lean, line 125.
Sources
TheoremGreen's Open Problem 26#
References: - [Gr24] Green, Ben. "100 open problems." (2024). - [JLP92] Jaeger, François, et al. "Group connectivity of graphs—a nonhomogeneous analogue of nowhere-zero flow properties." Journal of Combinatorial Theory, Series B 56.2 (1992): 165-182. - [ALM91] Alon, Noga, Nathan Linial, and Roy Meshulam. "Additive bases of vector spaces over prime fields." Journal of Combinatorial Theory, Series A 57.2 (1991): 203-210. - [Yu25] Yu, Yang. "Note on the Additive Basis Conjecture." arXiv preprint arXiv:2510.01300 (2025).
Quoted from FormalConjectures/GreensOpenProblems/26.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.
The file states 4 research or textbook statements: 1 open and 3 solved.
Green26.green_26
Solved: stated here without proof.
Let \(A_1, \dots, A_{100}\) be "cubes" in \(\mathbb{F}^n_3\). Is it true that \(A_1 + \dots + A_{100} = \mathbb{F}^n_3\)?
theorem green_26 :
∀ n : ℕ,
∀ A : Fin 100 → Set (𝔽₃ n), (∀ i, IsCube (A i)) →
∑ i, A i = univ
Category research solved; AMS 05 Combinatorics, 11 Number theory, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/GreensOpenProblems/26.lean, line 53.
Green26.green_26.variants.yu25
Solved: stated here without proof.
[Yu25] has solved the original problem (with 100 replaced by 4)
theorem green_26.variants.yu25 :
∀ n : ℕ,
∀ A : Fin 4 → Set (𝔽₃ n), (∀ i, IsCube (A i)) →
∑ i, A i = univ
Category research solved; AMS 05 Combinatorics, 11 Number theory, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/GreensOpenProblems/26.lean, line 61.
Green26.green_26.variants.alm91
Solved: stated here without proof.
[ALM91] showed that if 100 is replaced by \(\leq c(p) \log n\) then the result is true for \(\mathbb{F}^n_p\).
theorem green_26.variants.alm91 :
∀ (p : ℕ) [Fact p.Prime],
∃ (k : ℕ → ℕ),
((fun n ↦ (k n : ℝ)) =O[atTop] fun n ↦ Real.log n) ∧
∀ᶠ n in atTop,
∀ A : Fin (k n) → Set (𝔽 p n), (∀ i, IsCube (A i)) →
∑ i, A i = univ
Category research solved; AMS 05 Combinatorics, 11 Number theory, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/GreensOpenProblems/26.lean, line 74.
Green26.green_26.variants.open
Open: stated without proof.
The analogous problem in \(\mathbb{F}^n_p\) remains open. [Gr24]
theorem green_26.variants.open :
∀ (p : ℕ) [Fact p.Prime],
(∃ C, ∀ n, ∀ A : Fin C → Set (𝔽 p n), (∀ i, IsCube (A i)) →
∑ i, A i = univ)
Category research open; AMS 05 Combinatorics, 11 Number theory, 15 Linear and multilinear algebra; matrix theory. Declared in FormalConjectures/GreensOpenProblems/26.lean, line 85.
Sources
TheoremGreen's Open Problem 27#
References: - [Gr24] Green, Ben. "100 open problems." (2024). - [Be23] Bedert, Benjamin. "On unique sums in Abelian groups." Combinatorica 44.2 (2024): 269-298. - [CY26] Cao, Jiao-Long, and Ye Yuan. "A Second-Logarithm Lower Bound for Sets with No Unique Sums." arXiv preprint arXiv:2608.06728 (2026). - [St76] Straus, E. G. "Differences of residues (mod p)." Journal of Number Theory 8.1 (1976): 40-42.
Quoted from FormalConjectures/GreensOpenProblems/27.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 and 6 solved.
Green27.green_27.equivalent
Open: stated without proof.
What is the size of the smallest set \(A \subset \mathbb{Z} / p\mathbb{Z}\) (with at least two elements) for which no element in the sumset \(A + A\) has a unique representation?
theorem green_27.equivalent :
green_27.equivalent.answer ~[primesAtTop] m
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/27.lean, line 63.
Green27.green_27.lower
Solved: stated here without proof.
Propose a better lower bound along primes.
Cao and Yuan [CY26, Theorem 1.1] prove \(m(p) \gg \log p \log \log p\). This beats
lowerBest, since \(\sqrt{\log \log \log p} / \log \log \log \log p = o(\log \log p)\). The exact order of \(m(p)\) remains open.
theorem green_27.lower :
(lowerBest =o[primesAtTop] green_27.lower.answer) ∧ (green_27.lower.answer =O[primesAtTop] m)
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/27.lean, line 75.
Green27.green_27.upper
Open: stated without proof.
Propose a better upper bound along primes.
theorem green_27.upper :
(green_27.upper.answer =o[primesAtTop] upperBest) ∧ (m =O[primesAtTop] green_27.upper.answer)
Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/27.lean, line 84.
Green27.green_27.variants.lower_be23
Solved: stated here without proof.
We have \(m(p) \geq \omega(p) \log p\) for some function \(\omega(p)\) tending to infinity [Be23, Theorem 3].
theorem green_27.variants.lower_be23 :
∃ ω : ℕ → ℝ, Tendsto ω primesAtTop atTop ∧
∀ᶠ p in primesAtTop,
ω p * Real.log (p : ℝ) ≤ m p
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/27.lean, line 93.
Green27.green_27.variants.lower_cy26
Solved: stated here without proof.
Lower bound: \(\log p \log \log p \ll m(p)\) [CY26, Theorem 1.1].
theorem green_27.variants.lower_cy26 :
(fun p ↦ Real.log (p : ℝ) * Real.log (Real.log (p : ℝ))) =O[primesAtTop] m
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/27.lean, line 101.
Green27.green_27.variants.upper_be23
Solved: stated here; a Lean proof is at https://github.com/mkwatson/unique-sums-notes/blob/d4383f93a52e3a916ccce78d5fb7739c3bf3dabc/Green27Upper/Theorem.lean#L26.
Upper bound: \(m(p) \ll (\log p)^2\) [Be23, Theorem 5].
theorem green_27.variants.upper_be23 :
m =O[primesAtTop] upperBest
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/27.lean, line 110.
Green27.green_27.variants.previous_lower
Solved: stated here without proof.
Previous best-known lower bound \(\log p \ll m(p)\) from [St76].
theorem green_27.variants.previous_lower :
(fun p ↦ Real.log (p : ℝ)) =O[primesAtTop] m
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/27.lean, line 116.
Green27.green_27.variants.previous_upper
Solved: stated here without proof.
Previous best-known upper bound \(m(p) \ll \sqrt{p}\) from [Be23].
theorem green_27.variants.previous_upper :
m =O[primesAtTop] (fun p ↦ Real.sqrt (p : ℝ))
Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/GreensOpenProblems/27.lean, line 122.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.