AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Almost-everywhere Fourier convergence in L log L

Can the mathematical statement in Almost-everywhere Fourier convergence in L log L be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 075)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Almost-everywhere Fourier convergence in L log L'. We prove that the ordinary symmetric Fourier partial sums of every complex-valued function in L\log L on the circle converge almost everywhere to the function along the full sequence. This establishes the classical L\log L sufficiency conjecture.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 075). The Lean development was not rebuilt locally.