Lean formalization of the L³ bound for the trilinear Hilbert transform
An independent mathematician machine-checked one of the 372 claimed results in OpenAI's October 2026 mathematics release, the boundedness of the trilinear Hilbert transform with slopes 1, 2 and 3, writing the theorem statement by hand and having coding agents generate roughly 194,000 lines of Lean proof from a blueprint another model wrote.
- Lab
- Independent
- Model
- GPT-6 Astra Pro for the blueprint, with GPT-6 Astra Light and Claude Opus 5.5 autoformalizing the proof
- Field
- Mathematics
- Date
- 2026-10-20
- Human collaborators
- Joris Roos
What was found
OpenAI's release carried an bound for the trilinear Hilbert transform with fixed slopes 1, 2 and 3 as family 086, published on 2026-10-05 with no formalization attached. Joris Roos stated the theorem and the operator by hand in Lean 4 against Mathlib, as an a priori estimate on Schwartz functions, then had coding agents prove it from a blueprint that GPT-6 Astra Pro generated from the OpenAI manuscript and from a shorter version of the argument the same model produced. The proof runs to about 194,000 lines over 61 files, built between 8 and 16 October, first by Codex with GPT-6 Astra Light and then by Claude Opus 5.5; machine-generated code is confined to an Auto namespace and directory, and the README is human-written. The author records that Claude at medium reasoning effort stalled without disclosing it, building redundant wrappers and revisiting the same parts of the blueprint, which human monitoring of an agent-maintained status file caught and a large refactor at higher effort repaired. The Comparator challenge file states the theorem with its proof omitted and a solution module supplies it, permitting only propext, Quot.sound and Classical.choice.
Novelty check
Searched arXiv on 2026-10-26: ti:"trilinear Hilbert" returns three papers and all:"trilinear Hilbert transform" five, none of them a positive bound for the straight trilinear Hilbert transform at slopes 1, 2 and 3. The nearest published results point the other way or sit beside it: Demeter proved in 2007 that the operator is unbounded in a range of spaces with near 1 (arXiv 0712.2494), and Hu and Lie bound curved variants under a non-resonance assumption of pairwise distinct exponents (arXiv 2308.10706 and 2511.07373), which excludes the equal-slope straight case at issue. The mathematical claim here is OpenAI's rather than this author's; what is new is a machine-checked proof of it. The registry already carries two Lean formalizations from the same group, 2026-08-27-norm-variation-ergodic-averages-lean and 2026-10-18-two-commuting-ergodic-averages, both registered at Palomar from repositories under roos-j, and no entry covers the trilinear Hilbert transform.
Caveats and known objections
What was proved is what the Lean statement says, an a priori bound on Schwartz functions. That is common practice in the field and it is narrower than a bound on all of , so whether it is what the literature means by the trilinear Hilbert transform conjecture at these slopes stays a separate reading. Graded formal on the Palomar registration, which certifies that the proof typechecks against the recorded statement under the three permitted axioms; a scan of all 61 Lean files at the registered commit found no axiom declarations and no sorry outside the Comparator challenge file, where one is there by construction. Two limits on that evidence: the repository's own Lean build workflow has no run recorded against the registered commit, whose later green builds differ from it only in the README, and its Palomar comparator workflow shows no run at all in the repository's Actions history, so the registration is the record here rather than a rerun a reader can point to. The proof has not been read by a human. The author says so, says the agent-written log of discrepancies between blueprint and formalization has not been human-reviewed, and notes that those logs were written by weaker models than the one credited with the original manuscript. A formalization that follows a blueprint derived from OpenAI's argument is evidence that the argument goes through as written, not an independent route to the result. Autonomy is ai-led: the human posed the problem, wrote the statement and definitions, monitored the run and ordered the refactor, while the proof itself was machine-generated throughout.
Machine-checked elsewhere
PalomarFormalization of L^3 boundedness of the trilinear Hilbert transform
PALOMAR-2026-10-20-000001 · roos-j/lean-trilinearht at 0fac9f4ed4aa · checked 2026-10-20
ProvedTrilinearHT.trilinear_ht_bound
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Permitted axioms are exactly propext, Quot.sound and Classical.choice. Palomar records trust level high and archives a fork of the repository.
No independent check is recorded on this entry yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Lean formalization of the L³ bound for the trilinear Hilbert transform. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-20-trilinear-hilbert-transform-leanBibTeX
@misc{whataifound-independent-2026-lean,
title = {Lean formalization of the L³ bound for the trilinear Hilbert transform},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-10-20-trilinear-hilbert-transform-lean}
}