AI Proved What?

Episode 294, October 2026

The parts fall short?

An AI preprint claims a counterexample to the quasitrace problem, equivalent to Kaplansky’s question

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

4:11. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:30The claim
  3. 2:27How the proof goes
  4. 3:19Where it stands

The claim, in plain words

A trace measures the size of elements in an operator algebra: on matrices it is the normalized trace, and on a projection it gives the relative rank. A quasitrace keeps the trace’s rules on each commutative piece, and the size of x*x equals the size of xx*, but it need not add up across elements that do not commute; a 2-quasitrace must also extend to 2×2 matrices over the algebra. In the early 1950s Kaplansky asked whether every type II₁ AW*-factor is a von Neumann algebra. In 1982 Blackadar and Handelman showed that every stably finite unital C*-algebra has a normalized 2-quasitrace, and whether every 2-quasitrace is a trace, the quasitrace problem, is known to be equivalent to Kaplansky’s question. Haagerup proved, in a 1991 draft published in 2014, that on unital exact C*-algebras every 2-quasitrace is a trace.

Result 294 is one OpenAI paper, 16 pages, dated September 23, 2026, and published October 6. It claims a counterexample: a separable unital C*-algebra with normalized 2-quasitraces, and one fixed pair of positive contractions on which every one of them fails to add up, the parts falling short of the whole by at least 1/144. By the known equivalence, some type II₁ AW*-factor would not be a von Neumann algebra. It also claims two unital simple stably finite C*-algebras, one of them the reduced free group algebra, whose minimal tensor product is properly infinite, answering a question of Milhøj and Rørdam.

What it doesn’t claim

An exact or nuclear counterexample, which Haagerup’s theorem forbids, or an explicit simple factor. The method uses no results from quantum complexity.

Where it stands

Posted as a preprint
OpenAI, 16 pages, dated September 23, 2026
Peer reviewed
Not yet
Formalized in Lean
Both main statements (docs)

Last checked October 19, 2026. The paper has not been revised. In Lean, both main statements are formalized and match the paper: the quasitrace counterexample in about 32,000 lines and the tensor-product consequences in about 38,000 including it, with no unproved steps in our scan (we did not build them). The Lean proof reaches the simple example without AW*-algebras. OSVerify has not reviewed it. One expert has mentioned it as “proposing a counterexample”, and no one has reported an error.

How the proof goes

  1. No trace from the start. The algebra has 24 generators whose relations say outflow 1, inflow at most 2/3, which rules out a trace. The danger is the opposite: over a single point, a simple doubling tower becomes properly infinite at once.
  2. Twisted bundles. The paper twists the levels with line bundles over complex projective spaces. A Chern class then forbids a flat piece big enough to hold two orthogonal isometries, with one test for every matrix size and word length; the smallest lives on ℂP960.
  3. The defect. A convex scaling lemma makes the relations exact, and a telescoping step gives the defect: (1 − 2/3)/48 = 1/144.

The numbers in the video

  • Ours: a functional on 2×2 matrices that adds up on every commuting pair yet misses by 1/4 on two Pauli matrices; the square rule forces it back to the trace.
  • Ours: the smallest Chern-class test, on ℂP960: a bundle of rank 1,280 whose trivial part, 320, is less than the 512 two isometries would need.

Read the source

The paper

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

Transcript

Read the full script

0:00The question

A trace measures the size of elements in an operator algebra: on matrices it is the normalized trace, and on a projection it gives the relative rank. A quasitrace keeps the trace’s rules on each commutative piece, and the size of x*x equals the size of xx*, but need not add up across elements that do not commute; a 2-quasitrace must also extend to 2×2 matrices over the algebra. Our computer builds a functional on 2×2 matrices that adds up on every commuting pair yet misses on two Pauli matrices by 1/4; imposing the square rule forces it back to the trace. In the early 1950s Kaplansky asked whether every type II₁ AW*-factor, an algebraic cousin of a von Neumann algebra, is a von Neumann algebra. In 1982 Blackadar and Handelman showed that every stably finite unital C*-algebra has a normalized 2-quasitrace, and whether every 2-quasitrace is a trace, the quasitrace problem, is known to be equivalent to Kaplansky’s question. Haagerup proved, in a 1991 draft published in 2014, that on unital exact C*-algebras every 2-quasitrace is a trace. A 2025 preprint claiming the same for all algebras was withdrawn within days for a gap, and on October 7, 2026, a six-author paper still called the problem a huge open problem.

1:30The claim

Result 294 is one OpenAI paper, 16 pages, dated September 23 and published October 6, 2026. It claims a counterexample: a separable unital C*-algebra with normalized 2-quasitraces, and one fixed pair of positive contractions on which every one of them fails to add up, by at least 1/144. By the known equivalence, some type II₁ AW*-factor would not be a von Neumann algebra. It also claims two unital simple stably finite C*-algebras whose minimal tensor product is properly infinite, one of them the reduced free group algebra, answering a question of Milhøj and Rørdam. Not claimed: an exact or nuclear counterexample, which Haagerup’s theorem forbids, or an explicit simple factor; and the method uses no results from quantum complexity.

2:27How the proof goes

The algebra is built from 24 generators whose relations say outflow 1, inflow at most 2/3, which rules out a trace from the start. The danger is the opposite: over a single point, a simple doubling tower becomes properly infinite at once, as our computer shows with two orthogonal isometries. So the paper twists the levels with line bundles over complex projective spaces. A Chern class then forbids a flat piece big enough to hold two orthogonal isometries, with one test for every matrix size and word length; our computer checks the paper’s integer bookkeeping for the smallest test, on complex projective space of dimension 960. A convex scaling lemma makes the relations exact, and a telescoping step gives the defect: (1 − 2/3)/48, is 1/144.

3:19Where it stands

The paper is unrefereed and unchanged since release. In Lean, both main statements are formalized and match the paper: the quasitrace counterexample in about 32,000 lines, and the tensor product consequences in about 38,000 including it. Our scan finds no unproved steps, but we did not build them. The Lean proof reaches the simple example without AW*-algebras. OSVerify has not reviewed it; one expert has mentioned it as proposing a counterexample, and no one has reported an error. If it holds, a 2-quasitrace, a size that adds up on everything that commutes, can still fail to add up: on one pair, the parts fall short of the whole by at least one part in 144, every time.

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.