Back to Problems

erdos_188.estimate

Specification

Old and new problems and results in combinatorial number theory by Erdős & Graham (Page 15): How small can $M$ be made? The only estimate currently known is that $M \le 10000000$ (more or less). In the other direction, it has just been shown by R. Juhász [Ju (79)] that we must have $M \ge 5$.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement
theorem erdos_188.estimate : (∀ k, k ∈ s → 5 ≤ k) ∧ (∃ k ∈ s, k ≤ 10000000)
ID: ErdosProblems__188__erdos_188.estimate
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.