AI Proved What?

Episode 307, October 2026

Lost in assembly?

Two AI preprints claim counterexamples to the rational coarse Novikov conjecture, one checked in Lean

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

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

Chapters

  1. 0:00The question
  2. 1:35The claims
  3. 2:43How the proof goes
  4. 3:46Where it stands

The claims, in plain words

Coarse geometry looks at a space from far away, ignoring everything at small scales. To such a space one attaches its Roe algebra, made of operators that only move things a bounded distance, together with their limits, and the coarse assembly map sends K-homology classes of the space, measured at larger and larger scales, to the K-theory of that algebra: a higher index. The coarse Baum–Connes conjecture says this map is an isomorphism for spaces of bounded geometry. Its injective half is the coarse Novikov conjecture, and Yu proved it for spaces that coarsely embed into Hilbert space. Surjectivity was known to fail around 2000, by work of Higson and of Higson, Lafforgue and Skandalis, for certain expanders, where the projection onto constant functions is a ghost: norm one, but every matrix entry tiny. Injectivity was known to fail only without bounded geometry, and Willett and Yu wrote that a bounded-geometry counterexample would be very interesting.

Result 307 is two OpenAI papers, 40 pages; the companion is dated September 23 and the main paper October 5, and both were made public October 6, 2026. The main paper claims a coarse disjoint union of finite connected graphs of uniformly bounded degree, with a class of infinite order that the maximal coarse assembly map sends to zero. Since the maximal index carries over to the reduced index, this also breaks the reduced map. The companion builds a different space and claims the reduced failure directly, which would disprove the rational coarse Novikov conjecture for bounded-geometry spaces.

What they don’t claim

Anything about groups: the classical Novikov conjecture is untouched, and a separate result, covered in episode 285, claims a torsion-free group for which reduced Baum–Connes fails to be rationally injective. The class is in odd degree, and there is no conflict with Yu’s theorem, because these graphs contain expanders and do not coarsely embed into Hilbert space.

Where it stands

Posted as preprints
OpenAI, two papers, 40 pages, dated September 23 and October 5, 2026
Peer reviewed
Not yet
Formalized in Lean
In part: the reduced companion, not the maximal result (docs)

Last checked October 19, 2026. Neither paper has been revised. In Lean, the companion’s reduced counterexample is formalized: the challenge statement builds Roe algebras, K-theory and the assembly map from scratch in about 6,600 lines, the proof’s own files total about 45,000 lines, our scan finds no unproved steps, and property (T) is proved there by an explicit certificate; we did not build it. The maximal result, the item’s headline, is not formalized. One tracker worried that the formal assembly map might quietly default to zero; the proof shows that fallback never happens. OSVerify has not reviewed it, and we found no specialist comment.

How the proof goes

  1. Discs with deep fibres. The companion uses hexagonal discs whose vertices carry copies of SL₃(ℤ/2ᵏ), deepening toward the centre, with a twist. The class comes from the boundary circles of the discs. It survives at every scale because short loops carry no winding charge, and its index dies because the circles bound in the plain discs, and property (T) averaging carries that across into the graph’s Roe algebra.
  2. Twisted tori, in the maximal norm. The main paper stacks three-dimensional tori with a Heisenberg twist; the class is the top torus minus the bottom torus. It survives because a Chern class becomes divisible by 2ʲ in the middle, and its index dies through a Kazhdan projection and a sliding stack of copies of an operator, all in the maximal norm.

The numbers in the video

  • Ours: the fibre graph on SL₃(ℤ/2) has 168 vertices, so every entry of the ghost projection is 1/168; twenty averaging steps come within 0.06 of it, while on a 168-cycle the distance is still 0.99.
  • Ours, from the definitions: one component of the companion’s space at the tenth stage has about 8 × 10²³ vertices; the main paper’s first component has about 10¹².

Read the source

The 2 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

Coarse geometry looks at a space from far away, ignoring everything at small scales. To such a space one attaches its Roe algebra, made of operators that only move things a bounded distance, together with their limits, and the coarse assembly map sends K-homology classes of the space, measured at larger and larger scales, to the K-theory of that algebra: a higher index. The coarse Baum–Connes conjecture says this map is an isomorphism for spaces of bounded geometry. Its injective half is the coarse Novikov conjecture, and Yu proved it for spaces that coarsely embed into Hilbert space. Surjectivity was known to fail around 2000, by work of Higson and of Higson, Lafforgue and Skandalis, for certain expanders: graphs of bounded degree with a uniform spectral gap. There the projection onto constant functions is a ghost, with norm one but every matrix entry tiny. Our computer checks the fibre graphs used here: on the special linear group of 3 × 3 matrices mod 2, with 168 vertices, every entry is 1/168, and 20 averaging steps already come within 0.06 of that projection, while on a cycle of the same size the error is still 0.99. Injectivity was known to fail only without bounded geometry, in examples of Yu and of Dranishnikov, Ferry and Weinberger. Willett and Yu wrote that a bounded-geometry counterexample would be very interesting.

1:35The claims

Result 307 is two OpenAI papers, 40 pages; the companion is dated September 23 and the main paper October 5, and both were made public October 6, 2026. The main paper claims a coarse disjoint union of finite connected graphs of uniformly bounded degree, with a class of infinite order that the maximal coarse assembly map sends to zero: maximal assembly is not even rationally injective. Since the maximal index carries over to the reduced index, this also breaks the reduced map. The companion builds a different space and claims the reduced failure directly, which would disprove the rational coarse Novikov conjecture for bounded-geometry spaces. Not claimed: anything about groups. The classical Novikov conjecture is untouched, and a separate result, in episode 285, claims a torsion-free group for which reduced Baum–Connes fails to be rationally injective. The class is in odd degree, and there is no conflict with Yu’s theorem, because these graphs contain expanders and do not coarsely embed into Hilbert space.

2:43How the proof goes

The companion uses hexagonal discs whose vertices carry copies of the special linear group mod 2ᵏ, deepening toward the centre, with a twist. The class comes from the boundary circles of the discs. It survives at every scale because short loops carry no winding charge, and its index dies because the circles bound in the plain discs, and property (T) averaging carries that across into the graph’s Roe algebra. By our count from the definitions, one component at the tenth stage already has about 8 × 10²³ vertices. The main paper stacks three-dimensional tori with a Heisenberg twist; the class is the top torus minus the bottom torus. It survives because a Chern class becomes divisible by 2ʲ in the middle, and its index dies through a Kazhdan projection and a sliding stack of copies of an operator, all in the maximal norm. Our computer checks its commutator identity exactly; its first component already has about 10¹² vertices.

3:46Where it stands

Both papers are unrefereed and unchanged since release. In Lean, the companion’s reduced counterexample is formalized: the challenge statement builds Roe algebras, K-theory and the assembly map from scratch in about 6,600 lines, the proof’s own files total about 45,000 lines, our scan finds no unproved steps, and property (T) is proved there by an explicit certificate; we did not build it. The maximal result, the item’s headline, is not formalized. One tracker worried that the formal assembly map might quietly default to zero; the proof shows that fallback never happens. We found no specialist comment. If they hold, coarse assembly can fail to be injective, even rationally, for spaces of bounded geometry: the coarse Novikov conjecture is false in general, while the cases for groups are untouched, and spaces that coarsely embed into Hilbert space are still covered by Yu’s theorem.

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.