The maximal triangular Hilbert transform at the symmetric point

Lean formalization in OpenAI math repository (Result 082)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'The maximal triangular Hilbert transform at the symmetric point'. For arbitrary complex inputs in L^3(\mathbb R^2), we prove the pointwise maximal L^3\times L^3\to L^{3/2} estimate for the triangular Hilbert transform, with the supremum over both hard truncation endpoints. The estimate yields joint almost-everywhere and L3/2 convergence as the lower endpoint tends to zero and the upper endpoint tends to infinity. This also proves the conjectured scalar estimate at the symmetric point.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 082). The Lean development was not rebuilt locally.

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository