Erdős problem 755
Erdős asked whether every -point set in spans at most unit equilateral triangles.
Sources
FormalConjectures/ErdosProblems/
755.lean
Retained formal statement
Erdos755.unitEquilateralTriangleCount 1 ∅ = 0TestStatement only, no proof