Back to Problems

erdos_188.nonempty

Specification

Old and new problems and results in combinatorial number theory by Erdős & Graham (Page 14, 15): It has been shown that there is a large $M$ so that it is possible to partition $\mathbb{E}^2$ into two sets $A$ and $B$ so that $A$ contains no pair of points with distance 1 and $B$ contains no A.P. of length $M$.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement
theorem erdos_188.nonempty : s.Nonempty
ID: ErdosProblems__188__erdos_188.nonempty
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.