An exact Hausdorff gauge for SLE
An exact Hausdorff gauge for SLE is the subject of two manuscripts dated 25 and 26 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). Schramm asked whether the trace of chordal Schramm–Loewner evolution (SLEκ) admits a Hausdorff gauge function, a refinement of the power rd, under which pieces of the curve have positive finite Hausdorff measure. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original results
- Claim. For each fixed 0 < κ < 8, put d = 1 + κ/8. The gauge h(r) = rd(log log(1/r))(2−d)/2 at sufficiently small radii almost surely gives positive finite Hausdorff measure to every nontrivial compact positive-time segment of chordal SLEκ, and the entire trace has finite expected measure in every bounded disk. The abstract states that this gives an explicit solution to Schramm's Hausdorff-measure problem in this parameter range and that the exponent-one iterated-logarithm gauge suggested by Schramm is not σ-finite on any such segment. Source: An explicit exact Hausdorff gauge for SLE (26 September 2026).
- Existence of a gauge. An earlier manuscript constructs, for each 0 < κ < 8, a deterministic gauge with the same properties, without the explicit formula. Source: An exact Hausdorff gauge for SLE (25 September 2026).
- Formalization, as described by the repository. The scope note lean/docs/230.md states that the Lean formalization proves that every continuous nondecreasing gauge agreeing with h at sufficiently small radii almost surely assigns positive measure to every nontrivial compact positive-time segment of chordal SLEκ.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 14 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math at commit adc7f12, tables at repository commit cd0063d, 13 October 2026) |
Review (fidelity of the formal statements) | Rates this family "partial": only the positivity half is stated in Lean, while the finiteness of the measure on segments and the finite expected measure of the trace in bounded disks have no Lean statement. It also notes that SLE is not a Mathlib object, so the formalization defines it by hand through a Loewner-chain characterization. Its per-challenge table records a sandboxed Comparator pass for the challenge SLELowerPositivity (8 October 2026). |
The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet. |
| 2026-10-10 | D. Zhan, An Exact Hausdorff Measure as Natural Length for SLE (arXiv:2610.15066, v1) | Extension | The Hausdorff measure with OpenAI's gauge hκ is a deterministic positive constant multiple of the occupation measure (natural length) constructed by Lawler and Rezaei. | arXiv v1 (7 pages). |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.