Skip to content

Erdős problem 846

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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/846.lean

Formal Conjectures

FormalConjectures/ErdosProblems/846.leanErdos846.erdos_8463 linesExact file
False ↔  ∀ (A : Set (EuclideanSpace ℝ (Fin 2))),    ∀ ε > 0, A.Infinite → Erdos846.NonTrilinearFor A ε → Erdos846.WeaklyNonTrilinear A
SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:846
  • PLBY Lean proofsErdosProblems.Erdos846

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • AI alongside literature

    Erdős AI contributions wiki · 21-25 Feb, 2026

    Machine
    DeepMind prover agent, OpenAI internal model (independently)
    Open the source record

  • construction

    VibeMathed

    Machine
    DeepMind prover agent; OpenAI internal model (independently)
    Reported outcome
    resolved
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page