Problem detail · source-aware
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Erdős asked whether every $n$-point set in Euclidean space whose pairwise distances are mutually at least 1 apart must have diameter at least $(1+o(1))n^2$. Disproved: an explicit high-dimensional construction beats the conjectured constant.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement fidelity, correctness, priority, or novelty.
"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.
Provider: OpenAI, Harmonic · Prompt public: unknown · Independence: unknown
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.
Correctness: supported · statement fidelity: unaudited · peer review: none
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Source-reported tools: construction.
Independent: unknown · difference confidence: 0
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.