Episode 008, October 2026

One per odd weight

The Deligne–Drinfeld conjecture

Covers result 008 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

6:27. English captions available. The video loads from YouTube when you press play.

Chapters

The claim, in plain words

There are five ways to bracket a product of four letters, and moving one bracket at a time links them into a pentagon; allowing neighbors to cross adds hexagons. Around 1990 Vladimir Drinfeld studied the symmetries of these coherence rules, the Grothendieck–Teichmüller group. Its Lie algebra 𝔤𝔯𝔱 (strictly 𝔤𝔯𝔱₁) consists of the Lie polynomials ψ(x, y) in two letters that satisfy three equations: antisymmetry, ψ(x, y) + ψ(y, x) = 0; the hexagon, ψ(x, y) + ψ(y, −x − y) + ψ(−x − y, x) = 0; and a pentagon equation in the infinitesimal braid algebra on four strands. The Ihara bracket combines two solutions into a new one.

Result 008 claims the Deligne–Drinfeld conjecture: there are solutions σ₃, σ₅, σ₇, …, one in each odd weight, such that the free Lie algebra on one generator in each odd weight maps isomorphically onto 𝔤𝔯𝔱 with the Ihara bracket, and the same holds after completion by weight. In other words, the σ’s satisfy no hidden relations, and there are no other solutions.

What it doesn’t claim

The generators are not unique. The result concerns the rational Lie algebra 𝔤𝔯𝔱, not the separate, still-open question of whether the profinite Grothendieck–Teichmüller group equals the absolute Galois group Gal(ℚ̄/ℚ). The paper also derives a consequence for Kontsevich’s graph complex, but that consequence is not part of the Lean formalization.

Where it stands

Posted as a preprint: OpenAI, dated September 23, 2026; released October 6, 2026
Peer reviewed: Not yet
Checked in Lean: OpenAI published a Lean proof of the main theorem (scope note); we have not run the check

Last checked October 19, 2026. The claim has not been withdrawn, and the paper is unchanged since the repository’s first public version. Before this, the conjecture had been confirmed by computer up to weight 29 (Naef and Willwacher, 2025). We found no public critique specific to this result.

What was known

Existence. Ihara showed there is a new solution in every odd weight; Drinfeld gave a proof with associators (his Proposition 6.3).
Freeness. Francis Brown’s work on mixed Tate motives over ℤ (Annals, 2012) placed a free Lie algebra with one generator in each odd weight inside 𝔤𝔯𝔱. Willwacher (2026) proved that any homogeneous family σ_2k+1 with a nonzero coefficient of x^2ky generates a free Lie algebra.
No other solutions. Only checked by computer, up to weight 29 (Naef and Willwacher, 2025).
Graph complex. Willwacher (Inventiones, 2015) identified the zeroth cohomology of Kontsevich’s graph complex with 𝔤𝔯𝔱₁.

How the proof goes

An upper bound in every weight. The main estimate is dim 𝔤𝔯𝔱_n ≤ dim Lie⟨e₃, e₅, e₇, …⟩_n. Written over ℤ₍₂₎ (rationals with odd denominators) on a saturated lattice, the rational solution space is no bigger than its reduction mod 2.
A degeneration mod 2. With A = x², C = [x, y] and B = y, filtered by the number of B’s, the leading part of the pentagon becomes a relation in the enveloping algebra of a level-two cyclotomic hyperplane arrangement. Integral deletion operators detect it, and a shift symmetry B ↦ B + s(C) with a Vandermonde argument confines the image to the free Lie algebra generated by ad_C^kB, k ≥ 1. These have weights 3, 5, 7, …, exactly the predicted generators.
A lower bound. Following Drinfeld’s associator proof, the paper builds solutions from regularized braid holonomy. The coefficient of xⁿ⁻¹y is 2λⁿζ(n) with λ = 1/(2πi), nonzero because ζ(n) = Σ 1/qⁿ > 0.
Induction. Over ℤ₍₂₎, Hall words in the earlier generators plus a new depth-one solution attain the upper bound in each weight, which proves generation and freeness together.

Two consequences follow at once. Brown’s free algebra from motives has the same size in every weight, so it is all of 𝔤𝔯𝔱. And through Willwacher’s 2015 theorem, the zeroth cohomology of Kontsevich’s graph complex is a completed free Lie algebra with one generator in each odd weight.

The Lean statement

def IsSolution (p : L) : Prop :=
  p + eval y x p = 0 ∧
  p + eval y (-x-y) p + eval (-x-y) x p = 0 ∧
  eval (t 0 1) (t 1 2 + t 1 3) p
      + eval (t 0 2 + t 1 2) (t 2 3) p =
    eval (t 1 2) (t 2 3) p
      + eval (t 0 1 + t 0 2) (t 1 3 + t 2 3) p
      + eval (t 0 1) (t 1 2) p

theorem main : MainStatement

These are lines from the challenge file that OpenAI’s setup checks with the Comparator tool. MainStatement says there is a graded linear isomorphism from the free Lie algebra with one generator in each odd weight 3, 5, 7, … onto the solution space, carrying brackets to Ihara brackets and extending to the completions. A passing check guarantees that the proof proves exactly this, using only Lean’s standard axioms (propext, Quot.sound, Classical.choice). The proof is 21 files and 29,733 lines; a search found no sorry and no new axioms, but we have not run the check. It is listed in OpenAI’s formalization catalog, whose review status for the whole catalog is “unchecked”; OpenAI says its papers and proof files were produced by an internal AI model.

The numbers in the video

Weight 1: x − y passes antisymmetry and the hexagon but fails the pentagon. Weight 2: [x, y] fails the hexagon (the three terms sum to 3[x, y]). Weight 3: antisymmetry leaves one line, spanned by σ₃ = [x + y, [x, y]], which satisfies all three equations; we checked the pentagon modulo the braid relations by exact linear algebra.
In weight 29 the free Lie algebra on x, y has dimension 18,512,790 (Witt’s formula), while the free Lie algebra with one generator in each odd weight has dimension 120.
ζ(3) = 1.2020569…, ζ(5) = 1.0369277….

Read the source

The paper (PDF), “The Deligne–Drinfeld conjecture,” OpenAI Math Release preprint, September 23, 2026 (41 pages).
The Lean scope note and the challenge file linked above.
The collection’s catalog, where this is result 008, and its history of withdrawals and fixes.

The paper

OpenAI groups related papers into one result; this one has a single paper.

The Deligne-Drinfeld conjecture

Transcript

Read the full script

0:00Brackets and braids

Take four letters, a, b, c, d, and multiply them in order. There are five ways to place the brackets, and moving one bracket at a time links them into a pentagon. Let neighbors cross over each other as well, and hexagons appear too. Any consistent way of multiplying and braiding has to respect these shapes. Around 1990, Vladimir Drinfeld studied the symmetries of these rules. He named them the Grothendieck–Teichmüller group, after Grothendieck’s program, and his paper calls it a group that is closely connected with the Galois group of the algebraic numbers. Its infinitesimal version, a Lie algebra written grt, is cut out by three equations on polynomials in two letters. Deligne and Drinfeld predicted exactly what those equations allow: one free building block in each odd weight, three, five, seven, and so on. A computer had confirmed this up to weight 29. Result 008 in OpenAI’s math repository claims it in every weight, with a Lean proof attached.

1:04Three equations

Here’s the setup. Start with Lie polynomials in two letters, x and y, built from brackets: the bracket of x and y is xy − yx. The weight of a polynomial is its number of letters. A polynomial psi belongs to grt when it passes three tests. First, antisymmetry: swapping x and y flips the sign. Second, the hexagon, a three-term equation: cycle through x, y and −x − y, and the three copies cancel. Third, the pentagon. Feed psi into an algebra for four strands, where tᵢⱼ records strands i and j winding around each other, and five terms must balance, one for each edge of the pentagon: two on one side and three on the other, like the two routes around it. Solutions can be combined. The Ihara bracket takes two solutions and builds a new one, of higher weight. That’s what makes grt a Lie algebra.

2:00The first solutions

Start small. In weight one, x − y passes the first two tests, but fails the pentagon. In weight two, the bracket of x and y fails the hexagon: its three terms add up instead of canceling. Weight three is the first success. Antisymmetry leaves a single line, spanned by σ₃: [x + y, [x, y]]. We checked it against all three equations, including the pentagon, with exact computer algebra. Higher up, the space of candidates explodes. In weight 29 there are about 18.5 million independent Lie polynomials, and the conjecture says that only 120 independent solutions survive.

2:44What was known

The conjecture has three parts. First, there should be a new solution, called sigma, in every odd weight. Ihara showed that, and Drinfeld gave a proof using associators. Second, the sigmas should generate a free Lie algebra, with no hidden relations. Francis Brown’s 2012 work on mixed Tate motives placed exactly such a free algebra inside grt, and this summer, Thomas Willwacher proved freeness for any family of sigmas with a certain nonzero coefficient. The third part was the hard one: that there are no other solutions at all. A 2025 computer calculation confirmed it, weight by weight, up to weight 29. Beyond that, nobody knew.

3:29The claim

Result 008 claims all three parts, in every weight. There are solutions σ₃, σ₅, σ₇, and so on, such that the free Lie algebra with one generator in each odd weight maps isomorphically onto grt, bracket for bracket. The same holds after completing by weight. Two consequences follow at once. The free algebra found through motives turns out to be all of grt. And through Willwacher’s 2015 theorem, which matches grt with the zeroth cohomology of Kontsevich’s graph complex, that cohomology is a completed free Lie algebra too.

4:09How the proof goes

The heart of the proof is an upper bound: in each weight, grt has at most as many independent solutions as the free algebra predicts. To get it, the paper works with integer coefficients reduced mod 2. Set up carefully, the rational solution space can be no bigger than its mod 2 shadow. Mod 2, the paper uses three pieces: A for x squared, C for the bracket of x and y, and B for y, and it counts the B’s in every term. The leading part of the pentagon becomes a relation in a simpler algebra, coming from an arrangement of hyperplanes. Deletion operators read that relation off, and a shift symmetry, with a Vandermonde argument, pins the answer down to the free Lie algebra generated by B, bracketed again and again with C. C has weight two and B has weight one. So B bracketed k times with C has weight 2k + 1: three, five, seven. Exactly the predicted generators. For the lower bound, the paper builds a solution in every odd weight, following Drinfeld’s associators: it transports along braids and compares. One coefficient comes out as twice a power of a constant times ζ(n), the sum of 1/qⁿ. That sum is positive, so the coefficient is never zero. An induction, using only odd denominators, then makes the two bounds meet.

5:31Lean, and the caveats

The main theorem is stated in Lean: the space cut out by the same three equations is isomorphic to a free Lie algebra with one generator in each odd weight from three up. The proof is about 30,000 lines in 21 files. It’s listed in OpenAI’s catalog of formal proofs, whose review status, for the whole catalog, reads unchecked, and we haven’t run the check ourselves. The caveats. This is a 41-page preprint, not peer reviewed. The Lean proof covers the main theorem, but not the graph complex consequence. The generators aren’t unique. And this is about the Lie algebra, not the separate, still open question of whether the profinite Grothendieck–Teichmüller group is the Galois group itself. Three equations, one free generator in each odd weight, and nothing else. If the proof holds. And a computer can check it.

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.