---

Claim. Write $M_n$ for the maximum of the product $\Delta$ of Problem 1045 over $n$ points of the plane of diameter at most $2$ (the ordered product of the problem page, which is $\prod_{i<j}|z_i-z_j|^2$). Theorem 1.1 of Boyang Hu's manuscript Eventual maximizers of the planar distance product (revised 22 September 2026) asserts that for every odd $n\ge2^{100\,000\,000}$ and every even $n\ge2^{10^{120}}$ the maximizer is unique up to a Euclidean isometry and a relabeling of the points. For odd $n$ it is the regular polygon of diameter $2$, so that

$$M_n=n^n\sec^{\,n(n-1)}\frac{\pi}{2n}.$$

For even $n=2m$ the diameter graph of the maximizer (the pairs at distance exactly $2$) is a cycle on $n-3$ vertices with three pendant edges, attached so that the three cycle arcs between the attachment points are as equal as possible; the configuration has a reflection symmetry and, when $6\mid n$, a rotation symmetry of order three. Its geometry is given as the unique relevant solution of a rational stationary system in $n+1$ real variables, selected by one rational energy inequality, and the manuscript asserts no closed formula for even $n$. Theorem 1.2 states the perimeter analogue: for every $n\ge2^{100\,000\,000}$ the regular polygon is the unique maximizer of $\Delta$ among configurations whose convex hull has perimeter at most $2\pi$, with $M$ replaced by $n^n(\pi/(n\sin(\pi/n)))^{n(n-1)}$. The corollary on limits gives $M_n/n^n\to e^{\pi^2/8}$ along odd $n$ and $M_n/n^n\to\frac{3^{9/4}}8\exp\frac{\pi^2-2\sqrt3\pi}8$ along even $n$. The manuscript's abstract and outline (section 1.1) describe two passages from an approximate statement to an exact one. In the first, a maximizer is localized: averaging small circular measures around the points turns $\Delta\ge n^n$ into a lower bound on logarithmic capacity, a perimeter-capacity estimate makes the convex hull nearly circular, and one-point extremality on the hull yields angular equilibrium equations from which near-equality of the gaps between consecutive vertices follows; a quadratic form in the normal and tangential increments of the edges then controls the perimeter-normalized objective near the regular polygon, which gives Theorem 1.2 and, through Reinhardt's perimeter-diameter inequality, the odd case. In the second, for even $n$, the displacements of the centers of the opposite pairs are compared with a finite model, the maximum of a quadratic form over sign words that record which of the two crossing edges at each site is saturated: a move changing at most two signs improves every unbalanced word by a gain of order $n^{-2}$, and the move is transferred to exactly feasible configurations with a relative error of order $n^{-5/2}$, smaller than the gain. Strict concavity on the parameter domain of the balanced word gives uniqueness, and a rational stationary system with one rational energy inequality fixes the geometry (section 11). The thresholds are part of the statements; the claim's notes on the site describe the proof as effective.

Submission note. Posted to erdosproblems.com as a proof claim by Rogerhu (account Rogerhu) on 23 September 2026, giving "GPT-6 Pro, Astra" as the AI used:

We determine the optimal configurations for all sufficiently large $n$: regular polygons for odd $n$; for even $n$, the graph joining pairs at distance $2$ is a cycle on $n-3$ vertices with three leaves. We first show that every optimizer is nearly circular, with nearly equally spaced points. Small deformations of a regular polygon lower the product at fixed perimeter, with bounds independent of $n$. A perimeter–diameter bound then settles the odd case. For even $n$, we approximate the gain from moving the centers of nearly opposite pairs. At each site, a sign records which of the two adjacent crossing edges has length $2$. The best pattern has three alternating blocks, as equal in length as possible, over half the sequence. Improvements to competing patterns carry over to the geometry because the error is smaller than the gain. A second-derivative estimate gives uniqueness, and polynomial equations within a specified region determine the optimizer exactly. Notes: The proof is effective, with explicit finite thresholds for $n$. The initial research draft was generated by GPT-6 Pro, and the Lean 4 formalization was subsequently developed by Astra under human direction.

Covers. Every odd $n\ge2^{100\,000\,000}$ and every even $n\ge2^{10^{120}}$: the value of $M_n$ and the maximizer for odd $n$, the exact algebraic description of the maximizer for even $n$, and the regular-polygon question at those orders (yes for odd $n$, no for even $n$). The problem asks for the maximum for every $n$; the orders $6\le n$ below the thresholds are outside this claim (the values through $n=5$ and the failure of the regular polygon for every even $n\ge4$ are recorded on the problem page from the earlier literature).

Standing. The author filed the claim on the site's proof-claims tab on 23 September 2026 under the username Rogerhu, marked as a full claim. The one thread comment (5 October 2026) points out that the problem asks for every $n$ and that the result covers only sufficiently large $n$; this page records the scope the theorem states. The site labels the problem OPEN (page last edited 02 April 2026), no reviewer independent of the author has endorsed the manuscript, and it has no refereed publication. The claim therefore stays claimed.

AI systems. The manuscript's acknowledgment and the repository's source note say that the initial mathematical draft was generated with GPT-6 Pro and that the Lean formalization was developed with OpenAI Codex agents under human direction; the claim's notes on the site name GPT-6 Pro and Astra.

Formalization. The linked repository, pinned at the commit in the link, describes itself as a Lean 4 formalization of the manuscript. Its main theorem Erdos1045.main has five conjuncts: the diameter characterization with the parity thresholds above, the perimeter characterization, the two normalized limits, an algebraic certificate for the even-order system and a positive KKT certificate for the even-order maximizers; comparator.json names the theorem and permits only the axioms propext, Classical.choice and Quot.sound, and Challenge.lean restates the claims with the main theorem left open as a comparator reference. This corpus has not built or kernel-checked the development, so its self-reported build awards nothing here.

Depends on. Nothing beyond the cited manuscript.