Back to Problems

erdos_846

Specification

**Erdős Problem 846** Let `A ⊂ ℝ²` be an infinite set for which there exists some `ϵ>0` such that in any subset of `A` of size `n` there are always at least `ϵn` with no three on a line. Is it true that `A` is the union of a finite number of sets where no three are on a line? In other words, prove or disprove the following statement: every infinite `ε`-non-trilinear subset of the plane is weakly non-trilinar.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement
theorem erdos_846 : answer(sorry) ↔ ∀ᵉ (A : Set ℝ²) (ε > 0), A.Infinite → NonTrilinearFor A ε →
    WeaklyNonTrilinear A
ID: ErdosProblems__846__erdos_846
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.