---

Claim. The note Unit distances between disjoint convex translates, dated 27 April 2026, proves in its Theorem 1 that there is an absolute constant $c_0>0$ with $h(n)\geq c_0n^{4/3}$ for all sufficiently large $n$, in the notation of Problem 956. The construction takes a centrally symmetric convex body $D_W$, the convex hull of the points $\pm(\gamma(t)-\nu(t))$ for $0\le t\le W$, where $\gamma$ is a flat parabolic arc and $\nu(t)$ its unit normal, sets $C=D_W/2$ so that $C-C=D_W$, and places translates of $C$ at a parabolic grid: no nonzero difference of grid points lies in $D_W$, so the translates are disjoint, while many differences lie at Euclidean distance exactly $1$ from $D_W$. Combined with the Erdős–Pach bound $h(n)=O(n^{4/3})$, Corollary 1 gives $h(n)=\Theta(n^{4/3})$, so $h(n)>n^{1+c}$ for all large $n$ for every fixed $c<1/3$. Remark 1 of the note credits the counting mechanism to Valtr's parabolic-grid construction of strictly convex norms with many unit distances, and states that the new point is to make the body small enough for the translates to be disjoint.

Submission note. Posted to the site's forum by Przemek Chojecki on 27 April 2026:

GPT-5.5 Pro got

$$h(n)=\Theta(n^{4/3}).$$

using Erdős-Pach for an upper bound

and for a lower bound a construction found in a paper by Pavel Valtr "Strictly convex norms allowing many unit distances and related touching questions" with a slight modification.

Here's the note and here's the full formalization in Lean done by Aristotle.

Claimant. Chojecki posted the note on the site's discussion thread on 27 April 2026, writing that GPT-5.5 Pro had obtained the result; the note itself prints no author line. The post also links a Lean file completed by Aristotle, which formalizes the counting core of the construction (core_lower_bound, a polynomial inequality between the grid size and the number of unit pairs) and not the geometry; Nat Sothanaphan judged it highly incomplete on the thread the same day. Linmiao Xu's Lean development, registered in the Palomar registry on 4 October 2026, presents itself as adapting the parabolic construction announced by Valtr and detailed in this note, extends it to a four-layer signed grid, and proves lower bounds only: $h(n)>n^{4/3}/26$ for $n\geq80$, $h(n)>\frac25n^{4/3}$ for all large $n$, and $h(n)>n^{5/4}$ for all large $n$. The registry replays the proof against a challenge statement; its review is not peer review.

Depends on. Erdős and Pach's upper bound, which supplies the upper half of $h(n)=\Theta(n^{4/3})$.

Standing. Claimed. The result is not refereed, the site labels the problem OPEN, and no independent review was found. Neither Lean development has been built or audited by this corpus. Valtr announced the same order in 2005 without a published proof; that announcement is on its own claim page.