Bounded-degree coboundary expanders
From OpenAI Aftermath
Bounded-degree coboundary expanders are simplicial complexes in which every vertex lies in a bounded number of top-dimensional faces and every set of faces with a small coboundary is close to a coboundary, uniformly as the complexes grow; in dimension one they are the bounded-degree expander graphs. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims such complexes over the field with two elements in every dimension d ≥ 3, with a Lean formalization. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Over F2, the coboundary of a set of i-faces is the set of (i + 1)-faces that contain an odd number of them. Coboundary expansion asks that the size of the coboundary control the distance from the space of coboundaries, in weighted norms obtained by sampling a top face and then one of its i-faces. This forces the cohomology to vanish; an inequality measured against cocycles alone, called cosystolic expansion, allows nonzero cohomology.
- Linial and Meshulam, and Meshulam and Wallach, developed the coisoperimetric viewpoint for random complexes. Gromov connected cohomological filling inequalities with topological overlap and asked for arbitrarily large complexes with bounded vertex incidence and uniform filling bounds. Lubotzky and Meshulam in dimension two, and Lubotzky, Luria and Rosenthal in every dimension, constructed random coboundary expanders whose vertex degrees grow with the size.
- For bounded vertex degree, Kaufman, Kazhdan and Lubotzky obtained cosystolic and topological expansion for two-dimensional skeleta of Ramanujan complexes, and Evra and Kaufman obtained bounded-degree cosystolic expanders in every dimension. Chapman and Lubotzky proved the existence of bounded-degree two-dimensional coboundary expanders over F2. Oppenheim and Valentiner-Branth proved a cosystolic expansion theorem for Kac–Moody–Steinberg coset complexes, which the manuscript uses as its quantitative input.
The original result
- Claim. Theorem 1.1 of Bounded-degree coboundary expanders in every dimension states that for every integer d ≥ 3 there are constants D and ε > 0 and finite connected pure d-dimensional simplicial complexes Xm, with the number of vertices tending to infinity, such that every vertex lies in at most D faces of dimension d and every F2-cochain of degree i < d has coboundary norm at least ε times its distance from the coboundaries. Together with expander graphs and the two-dimensional result of Chapman and Lubotzky, the manuscript concludes that bounded-degree F2 coboundary expanders exist in every positive dimension.
- Method, as described: the complexes are the d-skeletons of finite congruence quotients, modulo powers of t, of a coset complex for a group of polynomial matrices in SL2d+1(Fq[t]) over a sufficiently large odd prime q. The infinite complex is identified with the part of an affine twin building opposite one chamber, which gives the needed acyclicity; Morrow's pro Tor-unitality theorem, Iwasa's homology pro-stability theorem and an odd-index transfer argument carry the cohomology vanishing to every congruence level; the Oppenheim–Valentiner-Branth theorem supplies the inequality against cocycles, and a comparison of weights passes it to the d-skeleton.
- Source (openai/math repository, commit
7ef5c0c): Bounded-degree coboundary expanders in every dimension, dated 24 September 2026. - Formalization, as described by the repository. The scope note lean/docs/177.md states that the formalization constructs bounded-degree F2 coboundary expanders in every dimension d ≥ 3, with constants that may depend on d, and that the graph and two-dimensional cases used for the all-dimensions conclusion are separate. The Comparator statement is
CoboundaryExpanders.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 29 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | G. Kalai, Updates: Sharing AI progress on mathematics (amazing!); and my lecture plans, a post on the blog Combinatorics and more | Remark (blog post) | Lists the result twice among connections between the release and earlier posts of the blog: with Ramanujan graphs, as bounded-vertex-degree coboundary expanders in every dimension at least three, and as a construction of arbitrarily large complexes with bounded vertex degrees and uniform coboundary expansion over the field with two elements, in connection with his 2011 introductory post on high-dimensional expanders. | Blog post of 7 October 2026. The post states that the collection includes results at different stages of verification, that their proofs will need to be checked and digested by the mathematical community, and that even Lean verification may have issues. |
| 2026-10-07 | Bounded-degree coboundary expansion, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains coboundary expansion as a higher-dimensional graph cut, the weighted norms, why vanishing cohomology is an additional requirement beyond cosystolic expansion, the construction and its local geometry, the passage from limiting information to each finite level, and the comparison of skeleton weights, with proof outlines. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": the Lean statement is the standard weighted coboundary expansion over the integers modulo 2 for every d ≥ 3, and the graph and two-dimensional cases are not part of the claim, as the collection's summary says. It records a sandboxed Comparator pass for CoboundaryExpanders on 8 October 2026. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38040214623 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the CoboundaryExpanders solution, in 489 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list CoboundaryExpanders, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-12 | Coboundary expanders of bounded degree, a course on Open Mathematics Courses (kokunoyumeto/open-math-courses-public) | Reading (exposition) | Three lessons: coboundary expansion, coset complexes, and the groups of polynomial matrices with their coset complexes, bounded degree and growth. The theorem is derived from two named statements, an expansion inequality relative to the cocycles and the vanishing of cohomology, which the course does not prove. | The course states that it was written and self-checked by Claude Opus 5.5 (Anthropic) and that independent review is not complete. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_547 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap and no minor notes. The reviewer read the whole source and checked the local group identities, also by brute force in small cases, the lattice stabilizers, the codistance filtration, the stabilization and transfer steps, the trivial-action argument and the weight comparison. It did not check the exact statements of the cited theorems of Iwasa, Oppenheim–Valentiner-Branth and Morrow. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
| 2026-10-16 | AI Proved What?, episode 177 Expanders in every dimension?, remade version of 24 October 2026 | Reading (exposition) | Video explainer of the claim and its place between cosystolic expansion and the earlier random constructions. The episode states that the result gives no small or computed constants: the prime is only sufficiently large, and by the site's own arithmetic the explicit conditions in dimension three force a degree bound of at least about 1.7 × 1034 and a first complex with at least about 1.3 × 1076 vertices. It also states that the result gives one growing sequence rather than every size, no algorithm, coefficients modulo 2 only, and no applications. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, 14 pages, dated September 24, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: formalized by OpenAI in the same form and not run by the site. The page states that the Lean proof proves the case of the cosystolic inequality it uses rather than assuming the cited theorems, that it found no unproved steps by search without rebuilding it, and that it has seen no expert review. |
Notes
- The background summarizes the manuscript's own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
