The triangular Hilbert transform at the symmetric point
The triangular Hilbert transform at the symmetric point is the subject of three manuscripts dated 24 September and 5 October 2026 in OpenAI's public mathematics collection (github.com/openai/math). The triangular Hilbert transform is a bilinear singular integral operator on functions of two variables whose boundedness at the symmetric exponents had been an open problem. 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
- Maximal estimate. For arbitrary complex F, G in L3(R2), the manuscript proves the pointwise maximal L3 × L3 → L3/2 estimate for the triangular Hilbert transform, with the supremum over both hard truncation endpoints, together with almost-everywhere and L3/2 convergence of the truncations; it states that this proves the conjectured scalar estimate at the symmetric point. Source: the manuscript The maximal triangular Hilbert transform at the symmetric point, dated 24 September 2026.
- Annular variation. A second manuscript proves annular r-variation estimates from complex L3 × L3 to L3/2 for every r > 2, with partitions allowed to depend on the output point. Source: the manuscript Annular variation of the triangular Hilbert transform at the symmetric point, dated 5 October 2026.
- Dyadic model. A third manuscript proves a uniform L3 × L3 × L3 estimate for the dyadic triangular Hilbert form with unrestricted real inputs, with constant forty. Source: the manuscript An L3 bound for the dyadic triangular Hilbert form, dated 5 October 2026.
- Formalization, as described by the repository. The scope note lean/docs/082.md states that the Lean formalization proves the symmetric maximal estimate with one absolute constant, together with a common full-measure set on which the truncated integrals are defined and almost-everywhere measurability of the maximal output.
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": the Lean states the maximal L3 × L3 → L3/2 bound, while the annular variation estimates, the convergence statements and the trilinear form at the symmetric point are not stated. Its per-challenge table records a sandboxed Comparator pass for the challenge TriangularHilbert (8 October 2026). |
The review states that its ratings concern whether 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-09 (branch commit e60e7a6, 13 October 2026) |
J. Roos, roos-j/lean-twocommuting (GitHub) | Use (method; formal) | A Lean 4 formalization stating that for a probability space with two commuting measure-preserving transformations T and S, and for f in Lp and g in Lq with p, q ≥ 1 and 1/p + 1/q ≤ 1, the averages N−1 Σn<N f(Tnx)g(Snx) converge for almost every x. The README states that the problem was solved by GPT 6 Astra Pro, instructed to adapt the triangular Hilbert transform result above, that the formalization was generated by Claude Opus 5.5, and that only the README and the theorem statement are human-authored. | The repository's metadata records its review status as self-assessed; a branch prepares a Palomar submission. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.