{"id":"palomar/PALOMAR-2026-10-20-000001","url":"https://github.com/roos-j/lean-trilinearht/tree/0fac9f4ed4aa3391931897a681ce547981fb5f46","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-20-000001-v1.json","repo":"https://github.com/roos-j/lean-trilinearht","tags":["math.CA","msc:42B20","msc:42B25","msc:11B30","harmonic-analysis","trilinear-hilbert-transform","formalization"],"score":0,"title":"Formalization of L^3 boundedness of the trilinear Hilbert transform","trust":"high","domain":"math.CA","source":"palomar","authors":["Joris Roos"],"reviews":0,"subject":"math.CA","summary":"This is a Lean 4 formalization of the `L³ x L³ x L³ → L¹` boundedness of the trilinear Hilbert transform. The formalization follows a blueprint that was generated by GPT-6 Astra Pro on the basis of a preprint claiming this result made public by OpenAI on Oct 6, 2026, and of a revised, shorter version of its argument generated by GPT-6. The preprint was made public without an accompanying formalization leaving possible doubts about its correctness. This formalization formally verifies its main result. The theorem statement is human-written, while the proof was autoformalized by coding agents.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-20","reactions":{},"formalized":true,"formalizes":[{"title":"An L^3 bound for the trilinear Hilbert transform","identifier":"OpenAI Math Release preprint (2026), https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-L3-bound-for-the-trilinear-Hilbert-transform-October-5-2026/paper.pdf","relationship":"formalizes"},{"title":"An L^3 estimate for the trilinear Hilbert transform: A revised, shorter argument","identifier":"No stable public location: shorter_argument.tex and a 57-page PDF dated October 8, 2026","relationship":"adapts"},{"title":"A forward formalization blueprint for the L^3 trilinear Hilbert transform estimate","identifier":"blueprint/formalization_blueprint.tex in this repository","relationship":"formalizes"}]}