ProbXiv
sign in
Problem archiveProblem record

Erdős Problem #670: Diameter with Separated Distances

Combinatorics · posed by Paul Erdős · disproved

2 comments

Statement

Erdős asked whether every nn-point set in Euclidean space whose pairwise distances are mutually at least 1 apart must have diameter at least (1+o(1))n2(1+o(1))n^2. Disproved: an explicit high-dimensional construction beats the conjectured constant.

Record

Source
Added
Links

Comments

No person has examined this. Everything below was judged by machines. say whether it holds →

  1. construction · #1

    GPT-5.4 Pro, Harmonic Aristotle, with Boon Suan Ho

    The record says a model found this and names the people who worked on it. No ProbXiv account is credited for it, and nobody has answered for it here.

    AI involvement
    ai discovered
    — the result was found by a model.

    "GPT-5.4 Pro was used to discover the construction of this paper, and Harmonic Aristotle was used to formalize the proof in Lean 4, with some assistance from GPT-5.4 Pro." All arguments independently verified by the author.

  2. Machine-checked by Lean on #1 · not a person

    lean: partially checkedLean

    scope Lean formalization of the core argument; statement correspondence not independently audited

    The proof is formalized in Lean 4 by Harmonic Aristotle; the formalization is public. Tier: the formalization is by Harmonic Aristotle with author verification only - and as of August 2026, erdosproblems.com still lists #670 as OPEN, so the canonical tracker has not yet accepted the disproof.

    Lean checked the formalisation, not that it says the same thing as the statement above.

Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.

Sign in

Solve with an agent

Open the statement in a chat, with the problem and the ground rules already written into the prompt.

open in Claude →open in ChatGPT →

This opens a third-party site. Nothing is posted back to ProbXiv and nothing you write there is recorded here — what a model gives you is an attempt, which a person still has to check.