AI Proved What?

Episode 014, October 2026

Ramanujan’s bound, up to E₈

Generic Ramanujan for exceptional groups over function fields, and restricted geometric Langlands in characteristic p

Covers result 014 in OpenAI’s catalog: all 8 papers. See its connections to other results and the work it cites.

Play Episode 014: Ramanujan, up to E₈? Generic forms are tempered, over function fields. A gold circle with points on it, above the Dynkin diagrams of G₂, F₄, E₆, E₇ and E₈.

5:29. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Ramanujan’s bound
  2. 0:55The general prediction
  3. 1:51Function fields
  4. 2:29The claims
  5. 3:37How the proofs go
  6. 4:45The caveats

The claim, in plain words

In 1916 Ramanujan studied the coefficients τ(n) of q∏(1 − qn)24 = q − 24q2 + 252q3 − 1472q4 + ⋯ and conjectured that |τ(p)| ≤ 2p11/2 for every prime p. Deligne proved it in 1974. The Langlands program predicts the same kind of bound for automorphic forms on other groups: for the right forms, the numbers attached to each prime (Hecke eigenvalues, or Satake parameters) are as small as possible, and the form is called tempered. Not every form is: Howe and Piatetski-Shapiro found exceptions in 1979, and Arthur’s conjectures explain them with an extra copy of SL2. Generic cusp forms, those with a nonzero Whittaker coefficient, are among those expected to be tempered.

Result 014 works over function fields, built from curves over finite fields, where far more is known. Its eight papers claim, among other things:

  • Generic Ramanujan for exceptional groups (19 pages). For a split adjoint group of type G2, F4, E6, E7 or E8 over any global function field, every globally generic cuspidal automorphic representation is tempered at every place, with no restriction on the characteristic, the ramification depth or the local type.
  • Ramanujan–Arthur decompositions (64 pages). For a split semisimple group, cuspidal functions at every full finite level split by nilpotent orbits of the dual group, each piece with its Satake classes in the pattern set by that orbit’s SL2, the same at every unramified place. This proves conjectures of Gaitsgory, Lafforgue and Raskin, and gives: for split adjoint simple groups of every type, a cusp form that is generic and unramified at one place is tempered at every unramified place.
  • Restricted geometric Langlands in characteristic p (39 pages). Gaitsgory and Raskin’s full-support conjecture: their restricted geometric Langlands functor is an equivalence onto all of the spectral side, for curves over the algebraic closure of a finite field under four conditions on the characteristic, and over other algebraically closed fields under two more.
  • The rest. Rationality of the canonical unramified Arthur filtration (43 pages), global Arthur enhancements of Vincent Lafforgue’s parameters (69 pages), and three papers constructing tame Hecke eigensheaves (46, 40 and 28 pages).

What it doesn’t claim

Everything here is over function fields. Over the rational numbers, the open cases of the Ramanujan conjecture, such as Maass forms for GL2, are untouched. The temperedness theorem is for globally generic cusp forms on split adjoint exceptional groups; non-generic forms can fail the bound, as Arthur’s conjectures predict. The Arthur-enhancement paper does not classify packets or prove a multiplicity formula.

Where it stands

Posted as preprints
OpenAI, September 24 and October 5, 2026; eight papers
Peer reviewed
Not yet
Checked in Lean
No: OpenAI published no Lean proof of the main theorems; one uncatalogued Lean file checks a linear-algebra step of the rationality paper (we have not run it)

Last checked October 19, 2026. The claims have not been withdrawn, and we found no public critique. The geometric papers assume conditions on the characteristic and rest on Gaitsgory and Raskin’s 2025 preprint and on the proof of geometric Langlands in characteristic zero; the two Ramanujan papers use neither. The exceptional-group paper also relies on a recent preprint of Genestier and Lafforgue. None of the main theorems has a Lean proof. OpenAI’s files do contain one uncatalogued (not linked from the collection’s catalog) Lean file of 431 lines, excluding Mathlib, with no unproved steps by our search; we have not run it. It checks a linear-algebra step of the rationality paper: over an algebraically closed field of characteristic zero, a space of vectors that stays the same when any automorphism of the field acts on the coordinates is spanned by vectors with rational coordinates. The file itself says the Arthur filtration is not formalized there. Correction (October 15, 2026): the video says there is no Lean proof; that is still true of every main theorem, but we missed this file.

What was known

  • Ramanujan’s conjecture for τ was proved by Deligne in 1974, as a consequence of the Weil conjectures.
  • Over function fields, Drinfeld proved the Ramanujan conjecture for GL2 and Laurent Lafforgue for GLn (Fields Medals 1990 and 2002). Vincent Lafforgue attached Galois parameters to automorphic forms for every reductive group.
  • Lomelí proved the generic Ramanujan conjecture over function fields for split classical groups and quasi-split unitary groups. For the exceptional groups there were conditional results (Sawin and Templier; Ciubotaru and Harris).
  • Geometric Langlands in characteristic zero was proved by Gaitsgory, Raskin and collaborators (2024), in about a thousand pages. In 2025 Gaitsgory and Raskin proved a restricted version in characteristic p onto some components of the spectral side, and all of it for GLn.

How the proofs go

  1. The decomposition. A new local argument plays two bounds on the same cohomology of moduli of shtukas against each other (Deligne’s weights from below; derived Satake, Wakimoto filtrations and Springer theory from above) to show the Satake classes follow the pattern of an SL2 attached to a nilpotent orbit. Vincent Lafforgue’s parameters and purity from Laurent Lafforgue’s GLn theory show the orbit is the same at every unramified place. A generic place forces the zero orbit (a criterion of Ciubotaru and Harris), and the zero orbit means tempered.
  2. Ramified places. There the parameter carries a nilpotent monodromy operator. The exceptional-group paper compares two such operators over the same parameter: one from the global geometry, made pure by the unramified result and Deligne’s local monodromy theorem, and one from the representation. Both lie in the one open orbit, so they match, and purity passes to the representation, which forces temperedness.
  3. Full support. The geometric paper starts from Gaitsgory and Raskin’s equivalence onto some components. A missing component would give, after lifting the curve to characteristic zero, a nonzero sheaf whose nearby cycles (its specialization back) vanish; Hecke operators, a Levi reduction and finite slices of the support show the nearby cycles cannot vanish.

The numbers in the video

  • τ(1), …, τ(7) = 1, −24, 252, −1472, 4830, −6048, −16744, and |τ(p)| ≤ 2p11/2 for all 168 primes below 1000, with largest ratio 0.959. The exceptional groups G2, F4, E6, E7, E8 have dimensions 14, 52, 78, 133 and 248. Checked with a short Python script.

Read the source

The 8 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00Ramanujan’s bound

In 1916, Srinivasa Ramanujan studied the coefficients of this power series: q ∏ (1 − qⁿ)²⁴. Call them τ(n): 1, −24, 252, −1,472, and so on. He conjectured a bound: at every prime p, τ(p) is at most 2p^(11/2), in size. Divide by that, and every value lands between −1 and 1. Pierre Deligne proved it in 1974, as a consequence of his proof of the Weil conjectures. Ramanujan’s conjecture has a sweeping generalization, to other symmetry groups. Result 014 in OpenAI’s math repository claims a large piece of it over function fields, together with a central conjecture of geometric Langlands theory.

0:55The general prediction

Ramanujan’s series is a modular form, a function with a huge symmetry. The Langlands program generalizes it to automorphic forms for other groups: orthogonal and symplectic groups, and the five exceptional groups, G₂, F₄, E₆, E₇ and E₈. Each such form has numbers attached to each prime, like τ(p), called Hecke eigenvalues. The generalized Ramanujan conjecture says that, for the right kind of form, those numbers are as small as possible: the form is tempered. But not every form qualifies. In 1979, Roger Howe and Ilya Piatetski-Shapiro found forms that break the naive bound. Arthur’s conjectures explain such failures through an extra copy of SL₂, and among the forms expected to be tempered are the generic ones: those with a nonzero Whittaker coefficient, a kind of Fourier coefficient.

1:51Function fields

There is a parallel world where far more is known: function fields, built from curves over finite fields. Primes become points on the curve, and automorphic forms become functions on bundles over it. There, Vladimir Drinfeld proved Ramanujan’s conjecture for GL₂, and Laurent Lafforgue for GLₙ, work recognized with Fields Medals. For other groups, Vincent Lafforgue attached Galois parameters to automorphic forms in general, and Luis Lomelí proved the generic conjecture for the classical groups. For the exceptional groups, it stayed open, apart from conditional results.

2:29The claims

Result 014 has eight papers, about 350 pages. The headline arithmetic claim: over any function field, every globally generic cuspidal automorphic representation of a split adjoint exceptional group, G₂ through E₈, is tempered at every place, with no restriction on the characteristic or the ramification. On the way, a companion paper splits all cuspidal functions by nilpotent orbits of the dual group, at every finite level, proving conjectures of Gaitsgory, Lafforgue and Raskin. For split adjoint simple groups of every type, being generic at one unramified place forces temperedness at every unramified place. On the geometric side, another paper proves Gaitsgory and Raskin’s full-support conjecture: the restricted geometric Langlands equivalence holds for curves over finite fields, under four conditions on the characteristic. The other papers build Hecke eigensheaves, prove a rationality conjecture, and attach Arthur’s extra SL₂ to Vincent Lafforgue’s parameters.

3:37How the proofs go

The decomposition comes first. A new local argument, playing two cohomology bounds against each other, and purity from the GLₙ theory, pin down the sizes of Hecke eigenvalues: they follow the pattern of an SL₂ inside the dual group, given by a nilpotent orbit, and the same orbit at every unramified place. A generic place forces the zero orbit, and the zero orbit means tempered. At a ramified place, the parameter carries extra data: a nilpotent monodromy operator. The paper compares two such operators over the same parameter, one coming from the global geometry, made pure by the unramified result and Deligne’s work, and one coming from the representation. It shows they must match, and that forces temperedness. The geometric paper starts from Gaitsgory and Raskin’s equivalence onto some of the components of the spectral stack. If a component were missing, lifting the curve to characteristic zero would produce a nonzero sheaf that vanishes when specialized back. Hecke operators and slices of the support rule that out, so no component is missing.

4:45The caveats

The caveats. These are eight preprints, about 350 pages, not peer reviewed, and with no Lean proof. The geometric results assume conditions on the characteristic, and rest on Gaitsgory and Raskin’s 2025 preprint and on the thousand-page proof of geometric Langlands in characteristic zero; the Ramanujan theorems need neither. And all of this is about function fields: the open cases over the rational numbers, even for GL₂, are untouched. Ramanujan’s bound, for every generic cusp form of every split adjoint exceptional group, over every function field. If the proofs hold.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.