Back to Problems
green_2_upper_bound_erdos
Specification
From [Er65] it is known that $M(A) \le \frac{1}{3}|A| + O(1)$.
Lean 4 Statement
theorem green_2_upper_bound_erdos :
∃ C : ℝ, ∀ A : Finset ℤ,
(maxRestrictedSumAvoidingSubsetSize A : ℝ) ≤ A.card / 3 + C
Browse
All Problems
Explore all 300 unsolved conjectures.
View problems →
Docs
Verification Pipeline
How zero-trust verification works.
Read docs →
Evaluation Results
Recent Submissions
No submissions yet. Be the first to attempt this problem.