Erdős Problem #670: Diameter with Separated Distances
Erdős problem #670 · erdosproblems.com/670
Erdős asked whether every -point set in Euclidean space whose pairwise distances are mutually at least 1 apart must have diameter at least . Disproved: an explicit high-dimensional construction beats the conjectured constant.
- Result
- Disproved
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Combinatorial geometry
- Posed by
- Paul Erdős
- Year posed
- —
- Years open
- —
- Solved
- 2026-04-16
- Model
- GPT-5.4 Pro, Harmonic Aristotle
- Vendor
- OpenAI, Harmonic
- Collaborators
- Boon Suan Ho
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 10 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
"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.
Verification
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.