Back to Problems

ersz_bounds

Specification

Erdős and Szekeres proved the bounds $$ 2^{n-2} + 1 ≤ f(n) ≤ \binom{2n-4}{n-2} + 1 $$ ([ErSz60] and [ErSz35] respectively). [ErSz60] Erdős, P. and Szekeres, G., _On some extremum problems in elementary geometry_. Ann. Univ. Sci. Budapest. Eötvös Sect. Math. (1960/61), 53-62. [ErSz35] Erdős, P. and Szekeres, G., _A combinatorial problem in geometry_. Compos. Math. (1935), 463-470.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement
theorem ersz_bounds :
    ∀ n ≥ 3, 2^(n - 2) + 1 ≤ f n ∧ f n ≤ Nat.choose (2 * n - 4) (n - 2) + 1
ID: ErdosProblems__107__ersz_bounds
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.