Back to Problems

green_2_upper_bound_choi

Specification

From [Ch71] it is known that $M(A) \le |A|^{2/5 + o(1)}$.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement 
theorem green_2_upper_bound_choi :
    ∃ (o : ℕ → ℝ) (_ : Tendsto o atTop (𝓝 0)), ∀ A : Finset ℤ,
      (maxRestrictedSumAvoidingSubsetSize A : ℝ) ≤ A.card ^ (2 / 5 + o A.card)
ID: GreensOpenProblems__2__green_2_upper_bound_choi
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.