---

Claim. The repository A Lean-verified proof of the six-point case of Erdős #1045, published on GitHub by the user coleski on 11 September 2026, claims that for six points of the plane with pairwise distances at most $2$ the maximum of the ordered product of Problem 1045 is

$$\max\prod_{0\le i<j\le5}|z_i-z_j|^2=64(2\sqrt3-2)^{18},$$

attained at $(-1,0),(1,0),(0,\sqrt3),(0,\sqrt3-2),(\sqrt3-1,1),(1-\sqrt3,1)$, the configuration Quanyu Tang conjectured optimal. It gives a computer-assisted written proof (a diameter-triangle bound, a certified local deformation to that case and exact interval covering certificates) and a Lean development of the final implication and of attainment. The repository says the proof was developed using Codex. Hu's manuscript on large $n$ (its claim page) cites the repository as its reference [10].

Covers. The maximum for $n=6$. The value exceeds the regular hexagon's $6^6$, which Danzer and Pommerenke had already shown is not optimal.

Depends on. No page of this wiki.

Standing. A self-published repository with no journal publication or outside review recorded; the repository says no submission to the site's forum was made. This corpus has not built the Lean development, so it gives no formalized evidence here. The site labels the problem OPEN.