Erdős 的直径猜想在高维空间中的距离分离情形已被推翻

Erdős 询问是否每一个n点集在欧几里得空间中，其$\binom{n}{2}$对偶距离彼此至少相距1，都必须具有直径至少为$(1+o(1))n^2$。我们通过为每个素数q构造集合$\mathcal X_q\subset \mathbb R^{q^2+q}$中n=q+1个点，使得$\mathcal X_q$中所有对偶距离彼此至少相距1，而$\operatorname{diam}(\mathcal X_q)\le\Bigl(1-\frac{1}{\pi^2}+o(1)\Bigr)n^2$来否定此陈述。该证明在Lean 4中完全形式化。