View source for The L log L Fourier-convergence conjecture

The '''''L'' log ''L'' Fourier-convergence conjecture''' asks whether the Fourier series of every function ''f'' on the circle with |''f''| log(2 + |''f''|) integrable converges almost everywhere. Carleson's theorem gives convergence for square-integrable functions and Kolmogorov's example shows that integrability alone is not enough; the conjecture places the threshold at the Orlicz class ''L'' log ''L''. A manuscript in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), dated 23 September 2026, claims to prove it, with a Lean formalization of the main theorem. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper is not presented here as independent verification.

== Background ==
* As recounted in the introduction of the manuscript:
** Carleson proved almost-everywhere convergence for square-integrable functions and Hunt extended it to ''L''<sup>''p''</sup> for every ''p'' > 1; Kolmogorov's integrable counterexample shows that the conclusion fails throughout ''L''<sup>1</sup>.
** Between these, Sjölin obtained convergence in ''L'' log ''L'' log log ''L'', Soria developed larger convergence spaces through extrapolation, Antonov proved convergence in ''L'' log ''L'' log log log ''L'', and Arias de Reyna introduced a quasi-Banach space containing both Antonov's class and Soria's space, which Carro, Mastyło and Rodríguez-Piazza studied further.
** Lie gave a time-frequency proof of the maximal bound from Arias de Reyna's space and formulated the ''L'' log ''L'' conjecture through a weak-''L''<sup>1</sup> maximal estimate; Di Plinio and Fragkos proved weak-''L''<sup>''p''</sup> bounds of order (''p'' − 1)<sup>−1</sup> as ''p'' tends to 1.

== The original result ==
* '''Claim.''' Theorem 1.1 of ''Almost-everywhere Fourier convergence in L log L'' states that for every complex-valued function ''f'' on the circle with ∫|''f''| log(2 + |''f''|) finite, the ordinary symmetric Fourier partial sums ''S''<sub>''N''</sub>''f'' converge to ''f'' almost everywhere along the full sequence ''N'' = 0, 1, 2, …. The manuscript also derives, through Stein's theorem, a weak-''L''<sup>1</sup> bound for the maximal partial sum in terms of the Luxemburg norm.
* ''Method, as described:'' the central estimate concerns one nonnegative input of mass one and bounded height, and bounds by ''Cd'' the integral over a good set of the supremum, over all integer modulations, of a delayed Haar-type sum along dyadic paths. Translation and scale averaging, following the dyadic representation method of Petermichl and Hytönen, turn these kernels into the Hilbert kernel and so into the ordinary Fourier projections. The combinatorial part identifies frequencies with nearly the same phase from a noisy observation of the input point: a compression lemma produces large sets of frequencies with small phase defects relative to one center, the Griffiths–Ginibre positive-correlation method controls the cost of new observations, and information costs are counted separately from the cost of choosing frequencies.
* '''Source''' (openai/math repository, commit <code>7ef5c0c</code>): [https://github.com/openai/math/tree/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/preprints/Almost-everywhere-Fourier-convergence-in-L-log-L-September-23-2026 Almost-everywhere Fourier convergence in L log L], dated 23 September 2026.
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/lean/docs/075.md lean/docs/075.md] states that the formalization proves almost-everywhere convergence of the full symmetric Fourier partial sums for every measurable complex-valued function on the circle with |''f''| log(2 + |''f''|) integrable, with the Comparator challenge [https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/lean/ComparatorChallenges/FourierLLogL.lean FourierLLogL.lean].

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 30 October 2026)
|-
| 2026-10-06 || [https://lowrank.github.io/latent-seminar/OpenAI-Math/075-fourier-convergence-l-log-l ''Almost-everywhere Fourier convergence in L log L''], an article of the Latent Seminar blog at lowrank.github.io || Reading (exposition) || Explains Fourier sums and the Orlicz space, the endpoint claim, the bounded-density estimate, why frequency selection costs information and the passage from maximal control to convergence, with proof outlines on delayed signs and a predictable martingale estimate, compression, thermal kernels and the transfer back to ordinary Fourier sums. || Blog article; it states that its source review covers statements, introductions and the proof mechanisms it describes and is not an independent verification of the complete proofs.
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>94c6630</code>, 28 October 2026) || Review (fidelity of the formal statements) || Rates this family "full": the Lean theorem is the manuscript's Theorem 1.1, needing only unpacking of the normalized Haar measure on the circle, the Fourier coefficients and the definition of ''L'' log ''L'' as an integrability hypothesis. It records a sandboxed Comparator pass for <code>FourierLLogL</code>. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-10 || cert-machine, openai/math lane K, run 38019899278: [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/FourierLLogL.json FourierLLogL] || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the solution, in 902 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. || Repository.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) does not list this challenge, so it was accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-12 || ''AI Proved What?'', episode 075 [https://aiprovedwhat.com/episodes/075-fourier-convergence-conjecture/ Enough to converge?], remade version of 26 October 2026 || Reading (exposition) || Video explainer of the claim and its history. The episode states that nothing is claimed about the classes between Konyagin's divergent examples and ''L'' log ''L'' or beyond ordinary one-dimensional Fourier series, and lists the outside inputs: Chang's large-spectrum method in Lee's entropy form, the Griffiths–Ginibre inequalities, Ville's maximal inequality, the dyadic averaging of Petermichl and Hytönen, and Stein's theorem. || Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, dated September 23, 2026, released October 6; under expert review: not yet; peer reviewed: not yet; checked in Lean: the main theorem, by OpenAI, which the site states it has not built. The page states that it has seen no expert review.
|}

== Notes ==
* The background summarizes the manuscript's own account of earlier work.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]