Formalization of L^3 boundedness of the trilinear Hilbert transform
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.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-20-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-20-000001/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-20-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'