Erdős Problem #755
PROVED LEANdatabase updated 2026-08-23
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
A three-point set whose pairwise distances are all equal to `side`.
A unit equilateral triangle in Euclidean `d`-space.
An equilateral triangle of any positive side length in Euclidean `d`-space.
Erdős asked whether every \(n\)-point set in \(\mathbb{R}^6\) spans at most \((1/27 + o(1)) n^3\) unit equilateral triangles. Clemen, Dumitrescu, and Liu [CDL25b] proved the stronger any-size statement \(T_6(n) = (1/27 + o(1)) n^3\). The unit-triangle upper bound follows as a corollary, since unit equilateral triangles are a subset of equilateral triangles of any positive side length: \(T_\mathrm{unit} \leq T_\mathrm{anysize}\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/755.Prizenone
Topicsgeometry
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/755
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.