Vela

Is there a set of points in such that every subset of points determines at least distances, yet the total number of distinct distances is

Worked, still open.

geometry · solved · possible · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239
vela reproduce examples/erdos-problems

evidence

unverified AI candidates (1)

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

A concrete example is a **truncated anisotropic lattice** (a “stretched grid”). Take [ P_m={(i,\sqrt2,j):0\le i,j\le m-1}\subset \mathbb Z\times \sqrt2,\mathbb Z, ] so (|P_m|=m^2). ([Erdős Problems][1])

candidate solution ↗

formal

AMS 52 · solved (literature)

theorem erdos_659 : answer(True) ↔ ∃ A : ℕ → Finset ℝ²,
   (∀ n, #(A n) = n ∧ ∀ S ⊆ A n, #S = 4 → 3 ≤ distinctDistances S) ∧
    (fun n ↦ distinctDistances (A n)) ≪ fun n ↦ n / sqrt (log n)
formal-conjectures/659.lean ↗

status

solved

notary

vela reproduce examples/erdos-problems
  • packet.json · sha256 5046fcd284011e8a7ca32b8a7a320ee75fbcc152652546aa43457a50c80a1707

finding.noted · reviewer:will-blair · 1 day

renders the record as of vev_d199cb2e · 1,338 events · hub

Search Vela

Jump to a section, signal, campaign, document, primitive, work path, frontier, record index, atlas, constellation, agent, capability, or full-state search.