Erdős Problem #846
DISPROVED LEANdatabase updated 2026-02-25
The statement as posed is false. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
We say a subset `A` of points in the plane is `ε`-non-trilinear if any subset `B` of `A`, contains a non-trilinear subset `C` of size at least `ε|B|`.
We say a subset `A` of points in the plane is weakly non-trilinear if it is a finite union of non-trilinear sets.
**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.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/846.Prizenone
Topicsgeometry
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/846
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.