Probability and statistical mechanics · Result 230

Exact Hausdorff gauges for SLE

2 papersLean

Resolves Schramm’s Hausdorff-measure question for chordal SLE_κ, \(0\lt \kappa\lt 8\). The explicit gauge \(r^d(\log\log(1/r))^{(2-d)/2}\), \(d=1+\kappa/8\), gives almost surely positive finite measure to every trace segment \(\gamma([s,t])\) with \(0\lt s\lt t\lt \infty\), and finite expected measure to the trace in every bounded disk.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

An exact Hausdorff gauge for SLE

OpenAI · September 25, 2026

For each \(0\lt \kappa\lt 8\), we construct a deterministic Hausdorff gauge that almost surely assigns positive finite measure to every nontrivial compact positive-time segment of chordal Schramm–Loewner evolution. This answers Schramm's Hausdorff-measure existence problem in this parameter range. The entire trace has finite expected gauge measure in each bounded box.

Read PDF Download Source

Cite

@misc{OAI:An-exact-Hausdorff-gauge-for-SLE-September-25-2026,
  author = {{OpenAI}},
  title = {{An exact Hausdorff gauge for SLE: A moment-integral and finite-batch construction}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-exact-Hausdorff-gauge-for-SLE-September-25-2026/An-exact-Hausdorff-gauge-for-SLE-September-25-2026.pdf}{OAI:An-exact-Hausdorff-gauge-for-SLE-September-25-2026}},
  year = {2026}
}

An explicit exact Hausdorff gauge for SLE

OpenAI · September 26, 2026

For each fixed \(0\lt \kappa\lt 8\), let \(d=1+\kappa/8\). The gauge \(h(r)=r^d(\log\log(1/r))^{(2-d)/2}\) at sufficiently small radii almost surely gives positive finite Hausdorff measure to every nontrivial positive-time compact segment of chordal SLE_κ. This gives an explicit solution to Schramm's Hausdorff-measure problem in this parameter range. The entire trace has finite expected measure in every bounded disk. The exponent-one iterated-logarithm gauge suggested by Schramm is not sigma-finite on any such segment.

Read PDF Download Source

Cite

@misc{OAI:An-explicit-exact-Hausdorff-gauge-for-SLE-September-26-2026,
  author = {{OpenAI}},
  title = {{An explicit exact Hausdorff gauge for SLE: A regular formula from quantitative tails and dense visits}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-explicit-exact-Hausdorff-gauge-for-SLE-September-26-2026/An-explicit-exact-Hausdorff-gauge-for-SLE-September-26-2026.pdf}{OAI:An-explicit-exact-Hausdorff-gauge-for-SLE-September-26-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

For \(0<\kappa<8\), put \(d=1+\kappa/8\). The formalization proves that every continuous nondecreasing Hausdorff gauge agreeing with \(h(r)=r^d(\log\log(1/r))^{(2-d)/2}\) at sufficiently small positive radii almost surely assigns positive measure to every nontrivial compact positive-time segment of ordinary chordal \(\mathrm{SLE}_\kappa\).

Comparator links

Result	Comparator statement
Positivity of the explicit gauge on every positive-time segment	SLELowerPositivity.lean

Scope note on GitHub →