Let $A \subset R^{2}$ 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?

Worked, still open.

geometry · solved · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

alphaproof · AlphaProof Nexus (DeepMind) · machine-verified (Lean)

Machine-verified Lean proof (kernel-checkable, sorry-free).

Lean proof ↗

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

As far as I can find in the literature, this is **open**. It appears as an Erdős–Nešetřil–Rödl “Pisier-type” decomposition problem (Erdős Problem #846), and the current recorded status is **OPEN** (no proof or counterexample known). ([Erdős Problems][1])

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · solved (literature)

theorem erdos_846 : answer(False) ↔ ∀ᵉ (A : Set ℝ²) (ε > 0), A.Infinite → NonTrilinearFor A ε →
    WeaklyNonTrilinear A

formal-conjectures/846.lean ↗

Kernel-checked proof; human-attested statement.

faithful — reviewer:will-blair erdos_846.lean

status

solved

evidence

formal

status

Search Vela