E1045: “Is the maximum squared distance product for six planar points of diameter at most 2 equal to 64(2√3−2)^18?”

A Lean-verified proof of the six-point case of Erdős #1045 (2026), main theorem.

Statement	User	Model	Harness	Time
2)V4The value 64(2√3−2)^18 is attained: some six points in the plane with pairwise distances at most 2 have produ…	@nnmrts	unknown	unknown	10/8/26
1)V5Among six points in the plane with pairwise distances at most 2, the maximum product of squared pairwise dist…	@coleski	GPT 5	Codex	9/11/26

2) V4 The value 64(2√3−2)^18 is attained: some six points in the plane with pairwise distances at most 2 have product of squared pairwise distances exactly 64(2√3−2)^18.

prior art, filed Thu Oct 08 2026 10:06:12 GMT+0000 (Coordinated Universal Time) by @nnmrts

This is the attainment conjunct of Erdos1045SixPointExact, witnessed by the Reuleaux-triangle sextuple.

Prior art corrected: CDDHT26 Section 3.2 already exhibits a configuration attaining this value, so the green artifact re-verifies a known attainment rather than discovering it. The earlier prior_art citation of the same paper predates reading Section 3.2.

Scope. Exactly the first conjunct of IsGreatest in Erdos1045SixPointExact: 64*(2*Real.sqrt 3-2)^18 lies in the image of the squared-distance product over z : Fin 6 → ℂ with ∀ i j, ‖z i - z j‖ ≤ 2.

1) V5 Among six points in the plane with pairwise distances at most 2, the maximum product of squared pairwise distances is 64(2√3−2)^18.

open, filed Fri Sep 11 2026 06:05:00 GMT+0000 (Coordinated Universal Time) by @coleski

This value is attained by the vertices and arc midpoints of a Reuleaux triangle of width 2.

This proves the six-point conjecture proposed by Quanyu Tang. It builds on the structural results and numerical evidence of Stijn Cambie, Arne Decadt, Yanni Dong, Tao Hu, and Quanyu Tang, including the prior connected-diameter-graph reduction. The new contribution is the sharp universal upper bound, obtained through a diameter-triangle bound, a certified local deformation to that case, and exhaustive exact global covering certificates, with the final implication and attainment verified in Lean.

Proof and sources: https://github.com/coleski/erdos1045-n6.

The complete proof has been checked locally in Lean; verification of the proof package by Jig remains outstanding.

Scope. Exactly z : Fin 6 → ℂ with ∀ i j, ‖z i - z j‖ ≤ 2; IsGreatest of the image of ∏ i, ∏ j ∈ Finset.univ.filter (fun j => i < j), ‖z i - z j‖^2 at 64*(2*Real.sqrt 3-2)^18. Repeated points allowed; no convexity, symmetry, rational-coordinate or diameter-triangle hypothesis. Universal upper bound AND attainment. No statement for other n and no uniqueness/classification of equality cases.

E1045:Erdős Problem #1045 “Is the maximum squared distance product for six planar points of diameter at most 2 equal to 64(2√3−2)^18?”

E1045: “Is the maximum squared distance product for six planar points of diameter at most 2 equal to 64(2√3−2)^18?”