OpenAI Aftermath

Stein's conjecture for Hilbert transforms along Lipschitz vector fields

From OpenAI Aftermath

Stein's conjecture for Hilbert transforms along Lipschitz vector fields asks for a uniform weak-(2,2) bound for the planar Hilbert transform taken, at each point x, along the line through x in the direction v(x) of a Lipschitz unit vector field, when the integration length is at most a fixed multiple of the reciprocal Lipschitz constant. Because the line varies with the point, the operator is not a Fourier multiplier. A manuscript dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a strong L2 bound at this short scale, with a Lean formalization. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.

Background

  • As recounted in the introduction of the manuscript:
    • In the formulation of Lacey and Li, Stein's question asks for a uniform weak-(2,2) bound with the outer length controlled by the reciprocal Lipschitz seminorm. Lacey and Li trace it to Zygmund's conjecture on almost-everywhere differentiation by averages over shrinking segments in direction v(x), and recall a Besicovitch obstruction: Hölder regularity of any exponent below one does not suffice for the corresponding averaging operator.
    • Bourgain proved an L2 theorem for averages along analytic fields, and Stein and Street proved local estimates for singular Radon transforms associated with real-analytic maps. Lacey and Li proved annular estimates for measurable directions and a Lipschitz Kakeya maximal theorem; Guo proved annular variation bounds for Lipschitz fields; Bateman and Thiele treated measurable fields depending on one coordinate; Guo and Thiele, and Di Plinio and Parissis, treated lacunary roundings of Lipschitz slopes; Di Plinio, Guo, Thiele and Zorin-Kranich showed that uniform strong L2 bounds on vertical frequency bands imply the full short principal-value bound, under a small uniform Lipschitz bound in the vertical variable.

The original result

  • Claim. The main theorem of A uniform Hilbert transform estimate for Lipschitz directions states that there are absolute constants a* and C* such that for every unit vector field v on the plane with Lipschitz constant at most one, every truncation of the directional Hilbert transform at outer length a*, with any smaller inner length, has L2 operator norm at most C*. The principal value is therefore bounded on L2 and of weak type (2,2). By scaling, a field with Lipschitz constant L satisfies the same bound at outer length a*/L. The field may depend on both coordinates.
  • Method, as described: after localization and rotation, the proof reduces to a restricted estimate on one vertical frequency band with a logarithmic gain, and a Lipschitz commutator reassembles the bands. Wave packets are assigned to top boxes whose direction is popular on part of the test set, and Lacey and Li's Lipschitz Kakeya theorem controls their count. The oscillatory saving comes from a finite Fourier inequality with operator constant exactly one and a strict improvement of the coefficient exponent, iterated over nested angular intervals; Lépingle's variation inequality controls the residual terms.
  • Source (openai/math repository, commit 7ef5c0c): A uniform Hilbert transform estimate for Lipschitz directions, dated 25 September 2026.
  • Formalization, as described by the repository. The scope note lean/docs/083.md states that the formalization proves uniform L2 bounds for short Hilbert transforms along Lipschitz unit vector fields in the plane, including fields depending on both coordinates: for Lipschitz constant K > 0, every hard truncation with 0 < ε ≤ R ≤ 1/(106K) has one universal bound on Schwartz functions. For 1-Lipschitz fields at a fixed short scale it also gives principal-value and weak-(2,2) estimates and bounded extensions to all of L2. The Comparator statement is LipschitzHilbert.lean.

Public follow-up work

Date Work Relation Public claim Public status (checked 30 October 2026)
2026-10-06 Hilbert transforms along Lipschitz directions, an article of the Latent Seminar blog at lowrank.github.io Reading (exposition) Explains the directional transform with the direction chosen at the output point, the precise claimed bound, the rescaling of the Lipschitz constant, frequency bands and amplitude levels, and the strict phase gain, with proof outlines. Blog article; it states that its source review covers statements, introductions and the described proof mechanisms and is not an independent verification of the complete proofs.
2026-10-10 cert-machine, openai/math lane K, run 38040214623 Verification (two kernels) Records that Lean's default kernel and the nanoda kernel accept the LipschitzHilbert solution, in 2106 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. Repository.
2026-10-10 to 2026-10-14 con-leche development journal (task #348) Verification (second kernel) In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list LipschitzHilbert, so it was accepted by con-leche and by Lean's official kernel. Development journal.
2026-10-12 MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026) Review (fidelity of the formal statements) Rates this family "full": the Lean statement is exactly the short-scale uniform bound with its principal-value and weak-type consequences, not a full-scale form of Stein's conjecture. It notes a custom principal-value definition that is correct for Schwartz functions, and it records a Comparator pass on cloud machines for LipschitzHilbert, finished on 12 October 2026. MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-16 J. Jardine, Lattice24, referee review rank_064 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) Review (AI-assisted audit) Reports no gap, with two minor notes. The reviewer did not check the size-selection and separated-synthesis lemmas of the ordinary-tile section line by line, and notes that the gain in the exponent is tiny, so that the theorem is qualitative and the constant is not effective in any practical sense; it describes neither point as a gap. Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.
2026-10-26 AI Proved What?, episode 083 Lines that turn?, current version of 26 October 2026; the page gives no date for the original Reading (exposition) Video explainer of the claim and its predecessors. The episode states that Zygmund's conjecture for averages, longer lengths for varying fields and other Lp spaces are not claimed, and that the principal-value bound is stronger than the weak bound Stein asked for. It names the paper's two specialized outside inputs, Lacey and Li's Lipschitz Kakeya theorem and Lépingle's variation inequality, and reports that the formalization also proves the Lacey–Li input. Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, dated September 25, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: OpenAI published a Lean proof, not run by the site. The page states that it has seen no expert review.

Notes

  • The background summarizes the manuscript's own account of earlier work.
  • The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.