OpenAI claim summary for Math-2887

Diameter, local mass and covering exponents of fixed-length honeycomb walks

OpenAI's claim

OpenAI presents a proof in the selected manuscript. Uniform honeycomb walks of every sufficiently large length are claimed to have diameter scale $3/4$, while local counts and covers simultaneously have exponent $4/3$, with a polynomial failure bound.

Mathematical statement of the claimed result

Result 1.

Let $\gamma$ be uniform among length-$n$ self-avoiding honeycomb-lattice walks from a fixed vertex, with unrestricted endpoint. Write $D(\gamma)$ for Euclidean diameter, $M_\gamma(z,s)$ for the number of visited vertices in the closed radius-$s$ ball at $z$, and $\mathcal N_\gamma(s)$ for the minimum number of such balls covering the visited set. For every $\delta,k>0$, the source supplies $C_{\delta,k}<\infty$ and $n_0$, so every $n\ge n_0$ has an event of probability at least $1-C_{\delta,k}n^{-k}$ on which \[ n^{3/4-\delta}\le D(\gamma)\le n^{3/4+\delta}, \] \[ n^{-\delta}\min\{n,s^{4/3}\}\le M_\gamma(z,s)\le n^\delta\min\{n,s^{4/3}\}, \] \[ n^{-\delta}(1+ns^{-4/3})\le\mathcal N_\gamma(s)\le n^\delta(1+ns^{-4/3}). \] The latter bounds hold simultaneously for all visited $z$ and every real $1\le s\le n$.

Outline of the argument

Critical strip, nesting, polygon, and arc inputs bound path masses in boxes. Localized bridges with recoverable seams permit conditioning on exact lengths; multiscale covering and local-visit estimates are then made simultaneous without restricting to a density-one length set.

Formal verification

For family 237, the selected Lean statements give critical-strip mass and displacement exponents, bridge summability, and existence of pulled free energy. The $4/3$ bridge-length and $3/4$ spatial laws and the other polygon/chord exponents are outside these statements. No Comparator is assigned to the selected manuscript here; the family page selects other papers or supporting statements. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

• OpenAI, Mass and covering exponents for fixed-length honeycomb walks, 2026-09-26; citation key OAI:Mass-and-covering-exponents-for-fixed-length-honeycomb-walks-September-26-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 237: Lean scope.
• OpenAI catalogue entry.