AI Proved What?

Episode 291, October 2026

One week, two proofs?

Four AI preprints claim the last direction of the Toms–Winter conjecture, the same week as a two-part human proof

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

Play Episode 291: One week, two proofs? A triangle of arrows whose last side is drawn twice, in gold and pink.

3:59. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:20The claims
  3. 2:32How the proof goes
  4. 3:19Where it stands

The claim, in plain words

In a C*-algebra, traces measure the size of elements, and Cuntz comparison asks whether one positive element fits inside another. In 6×6 matrices, the normalized trace of higher and higher roots of a rank-2 element climbs to 2/6; it fits inside a rank-3 element but not a rank-1 one. Strict comparison means that whatever is smaller under every trace fits inside. The Jiang–Su algebra 𝒵 is infinite-dimensional and has no projections except 0 and 1, yet K-theory and traces see it exactly as they see the complex numbers; an algebra unchanged when tensored with it is Z-stable. Nuclear dimension is one less than the number of colours a cover needs: two for an interval, three for a brick-wall cover of a square.

For simple separable nuclear algebras, matrix algebras aside, Toms and Winter conjectured (first written down in 2009) that finite nuclear dimension, Z-stability and strict comparison coincide. By 2021 every direction was proved except strict comparison implies Z-stability, which a recent problem list called “the final open implication.” Result 291 is four OpenAI preprints, 180 pages, dated September 23 and October 5, 2026, and published October 6. The main paper claims that direction for all separable simple nuclear non-elementary algebras, nonunital ones included. Another offers a second proof of the unital case through uniform property Γ, a third claims Robert and Tikuisis’s conjecture on nuclear dimension, and the fourth claims the unital stably finite case of Szabó’s conjecture for amenable group actions, with no restriction on traces.

The same week, and what it doesn’t claim

On October 5 Hannes Thiel posted a proof that strict comparison gives pureness, and on October 7 Evington, Hua, Schafhauser, Seth, Tikuisis and White posted a proof that pureness gives Z-stability, together completing the conjecture. Both human papers credit AI with early help on a key lemma. The release does not claim anything about the UCT, so classification is not completed, or Z-stability beyond nuclear algebras.

Where it stands

Posted as preprints
OpenAI, four papers, 180 pages, dated September 23 and October 5, 2026
Peer reviewed
Not yet
Formalized in Lean
In part: one uniform Γ theorem registered, the unital comparison theorem unregistered (docs)

Last checked October 19, 2026. The preprints have not been revised. In Lean, the registered check covers one uniform Γ theorem, about 17,000 lines; a larger development built on it, about 69,000 lines but not registered for checking, proves the unital comparison theorem. Our scan finds no unproved steps in either; we built neither. OSVerify has not reviewed them, and we found no expert comment.

How the proof goes

  1. Building blocks. The main paper turns comparison into divisibility, and divisibility into central copies of dimension-drop algebras, the building blocks of 𝒵. With coprime sizes 2 and 3, such a block has only the projections 0 and 1, and K0 = ℤ, K1 = 0.
  2. Splitting every trace at once. The uniform Γ paper uses a central limit theorem: sums of many centered operator coins, cut into equal slices of a bell curve. The equivariant paper does the same along group orbits, with a unitary spread evenly round the circle, cut into arcs.

The numbers in the video

  • Ours: in 6×6 matrices, the normalized trace of a1/k for a rank-2 element reaches 0.3333 at k = 4,096.
  • Ours: with 4,096 coins under a biased trace, centered coins give slices of 0.337, 0.327 and 0.337; uncentered coins give 0, 0 and 1.

Read the source

The 4 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:00The question

In a C*-algebra, traces measure the size of elements, and Cuntz comparison asks whether one positive element fits inside another. Our computer shows the matrix version: taking higher and higher roots of a rank-2 element of 6×6 matrices, its normalized trace climbs to 2/6, its rank out of six, and it fits inside a rank-3 element but not a rank-1. Strict comparison means that whatever is smaller under every trace fits inside. The Jiang–Su algebra is infinite-dimensional and has no projections except 0 and 1, yet K-theory and traces see it exactly as they see the complex numbers. An algebra that absorbs it, unchanged when tensored with it, is called Z-stable. Nuclear dimension is one less than the colours a cover needs: our computer colours a cover of an interval with two colours, and a brick-wall cover of a square with three. For simple separable nuclear algebras, matrix algebras aside, Toms and Winter conjectured, in a form first written down in 2009, that three properties coincide: finite nuclear dimension, Z-stability and strict comparison. By 2021 every direction was proved except one, strict comparison implies Z-stability, which a May 2026 problem list called the final open implication.

1:20The claims

Result 291 is four OpenAI preprints, 180 pages, dated September 23 and October 5, 2026, and published October 6. One claims that missing direction for all separable simple nuclear non-elementary algebras, non-unital ones included. Another offers a second proof of the unital case through uniform property Gamma, a third claims to settle a related conjecture about nuclear dimension, and the fourth claims the unital stably finite case of Szabó’s conjecture for amenable group actions, with no restriction on traces. The same week, people posted proofs of the same direction independently. On October 5 Hannes Thiel posted a proof that strict comparison gives pureness, and on October 7 Evington, Hua, Schafhauser, Seth, Tikuisis and White showed that pureness gives Z-stability, completing the conjecture. Both human papers credit AI with early help on a key lemma. Not claimed by the release: anything about the UCT, so classification is not completed, or Z-stability beyond nuclear algebras.

2:32How the proof goes

The main paper turns comparison into divisibility, and divisibility into central copies of dimension-drop algebras, the building blocks of the Jiang–Su algebra. Our computer checks such a block: with coprime sizes 2 and 3, its only projections are 0 and 1, and its K-theory matches the complex numbers’. The uniform Gamma paper splits every trace evenly at once with a central limit theorem: sums of many centered operator coins, cut into equal slices of a bell curve. Our computer finds thirds of about 0.33 even under a biased trace, while uncentered coins pile everything into one slice. The equivariant paper does the same along group orbits, with a unitary spread evenly round the circle, cut into arcs.

3:19Where it stands

The preprints are unrefereed and unchanged since release. In Lean, the registered check covers one uniform Gamma theorem, about 17,000 lines, and a larger development built on it, about 69,000 lines but not registered for checking, proves the unital comparison theorem. Our scan finds no unproved steps in either, but we built neither. OSVerify has not reviewed them, and we found no expert comment. The last arrow of the Toms–Winter triangle got two proofs in one week: this release, if it holds, and two human papers that together make one, each helped by AI.

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.