OpenAI claim summary for Math-2915

A deterministic exact Hausdorff gauge for ordinary SLE

OpenAI's claim

The linked manuscripts present the following claims by OpenAI: For $0<\kappa<8$, a deterministic gauge is claimed to give positive finite measure to each nontrivial compact positive-time SLE segment; The explicit proposed SLE gauge is $r^d(\log\log(1/r))^{(2-d)/2}$, $d=1+\kappa/8$; the exponent-one alternative is claimed not sigma-finite on nontrivial segments. Together they give a claimed affirmative answer in the matching scope.

Mathematical statement of the claimed result

Result 1.

For $0<\kappa<8$, let $\gamma$ be ordinary chordal $\mathrm{SLE}_\kappa$ from $0$ to $\infty$ in $\mathbb H$, with capacity $2t$. There exists a deterministic continuous nondecreasing gauge $h_\kappa$, vanishing at zero and positive elsewhere, such that almost surely \[ 0<\mathcal H^{h_\kappa}(\gamma([s,t]))<\infty \qquad\text{simultaneously for all real }0<s<t<\infty. \] Here $\mathcal H^h(E)=\lim_{\delta\downarrow0}\inf\{\sum_jh(\operatorname{diam}U_j):E\subset\bigcup_jU_j,\ \operatorname{diam}U_j\le\delta\}$. The gauge depends only on $\kappa$.

Result 2.

Let $\gamma$ be ordinary chordal $\mathrm{SLE}_\kappa$ in $\mathbb H$, from $0$ to $\infty$, parametrized with capacity $2t$, and write $\Gamma=\gamma([0,\infty))$. Fix $0<\kappa<8$, put $d=1+\kappa/8$, $p=2-d$, and define near zero \[ h(r)=r^d\left(\log\log(1/r)\right)^{p/2}. \] Complete this gauge continuously and monotonically at larger radii. Using diameter-based Hausdorff measure, almost surely \[ 0<\mathcal H^h(\gamma([s,t]))<\infty\quad\text{for every real }0<s<t<\infty. \] For each deterministic $R>0$, $\mathbb E\mathcal H^h(\Gamma\cap\overline B(0,R))\le C_{\kappa,R}<\infty$. In particular, the trace has finite $h$-measure in every rectangle $[-m,m]+i[0,m]$, simultaneously for integers $m\ge1$.

Outline of the argument

Finite stopped Green tilts give one-point laws, and regularized product supermartingales control simultaneous radius hits. Integrating collision singularities constructs a canonical trace mass; its moment growth selects a gauge with both lower density and upper covering estimates.

Localized stopped densities and Brownian boundary-occupation estimates give a uniform spatial tail bound. A positive mass with controlled ball density supplies the lower Hausdorff estimate, and carefully chosen spatial covers supply the upper bound; comparison of gauges then excludes the exponent-one choice.

Formal verification

For family 230, the selected statement proves positivity for the explicit iterated-logarithm gauge on every nontrivial compact SLE segment. Finiteness, expected box measure, and failure of the exponent-one gauge are beyond that entry. The listed Comparator files are SLELowerPositivity.lean. The inventory does not supply a named declaration for these Comparator entries. 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, An exact Hausdorff gauge for SLE: A moment-integral and finite-batch construction, 2026-09-25; citation key OAI:An-exact-Hausdorff-gauge-for-SLE-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• OpenAI, An explicit exact Hausdorff gauge for SLE: A regular formula from quantitative tails and dense visits, 2026-09-26; citation key OAI:An-explicit-exact-Hausdorff-gauge-for-SLE-September-26-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 230: Lean scope.
• Comparator SLELowerPositivity.json.
• Comparator SLELowerPositivity.lean.
• OpenAI catalogue entry.