AI Proved What?

Episode 120, October 2026

Almost-linear matching?

A claimed randomized algorithm that finds a maximum matching in any graph in almost-linear time

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

5:23. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Matchings and odd cycles
  2. 1:23The claim
  3. 2:35How the algorithm works
  4. 4:49Where it stands

The claim, in plain words

A matching pairs up vertices along edges, using each vertex at most once; the classic problem is to find a largest one. In bipartite graphs, alternating paths settle it. In general graphs, odd cycles get in the way: on a triangle, giving each edge 1/2 satisfies every vertex constraint, yet only one edge can be matched. Edmonds overcame this in 1965 by shrinking odd cycles, called blossoms, and his matching polytope adds constraints for odd sets.

For decades the best bound for sparse general graphs was that of Micali and Vazirani, O(m√n). Algebraic methods of Mucha, Sankowski and Harvey run in matrix-multiplication time, best on dense graphs. For bipartite graphs, the almost-linear exact flow algorithms of Chen, Kyng, Liu, Peng, Probst Gutenberg and Sachdeva, and of van den Brand and coauthors, gave almost-linear exact matching. Sparse general graphs, with their odd blocks, stayed at the square-root bound.

Result 120 is one OpenAI preprint (86 pages, September 24, 2026). It claims one uniform randomized algorithm that finds a maximum-cardinality matching in any simple graph with n vertices and m edges in time (n + m)1+o(1), on every computation path in a logarithmic-word model, outputting an explicit maximum matching with probability at least 2/3. No perfect matching is assumed; on the densest graphs the bound is n2+o(1). The same guarantees hold for finding a spanning subgraph with prescribed vertex degrees (an f-factor) or deciding that none exists, via Tutte’s reduction with rearrangeable networks.

What it doesn’t claim

The algorithm is randomized: it may fail, with probability at most 1/3, though its running time is bounded on every computation path. The o(1) in the exponent is not a fixed constant, so this is an asymptotic guarantee rather than a practical running time. The result is about cardinality; weighted matching is not claimed.

Where it stands

Posted as a preprint
OpenAI, 86 pages, dated September 24, 2026
Peer reviewed
Not yet
Checked in Lean
No Lean proof of the theorem; uncatalogued Lean files check one ingredient, the degree-reduction lemma (we have not run them)

Last checked October 19, 2026. The preprint has not been revised. OpenAI published no Lean proof of the theorem, so the 86 pages are the only proof of the algorithm and its running time. OpenAI’s files do contain five uncatalogued (not linked from the collection’s catalog) Lean files, 645 lines excluding Mathlib, with no unproved steps by our search, that check one ingredient: the paper’s degree-reduction lemma. Replacing each vertex by a path gives a graph of maximum degree three, with 4m − n vertices, that has a perfect matching exactly when the original graph does (for graphs without isolated vertices). The lemma’s running time is not formalized, and we have not run these files. It is not among those OSVerify reviewed, and we have seen no expert review. A claim of this size would need careful independent checking.

How the algorithm works

  1. Bins, rows and ledgers. The core subproblem is a perfect matching in a graph of maximum degree 3. The current matching is stored through a partition: odd blocks called bins, matched internally apart from one exposed vertex; single vertices called rows, assigned along edges to distinct bins; and matched pairs. Ledgers split a fixed amount from each row among its neighbouring bins. At a settled state the lowest ledger certifies a strict Hall surplus, and the highest carries a logarithmic objective that can always improve when a perfect matching exists and no structural step is available.
  2. Debt pays for repairs. Repairs are exact flow problems on row–bin incidences, initially explored only where debt is large relative to bin size. An unexplored bin accepts flow optimistically; if enough arrives, it is explored and locks in an amount proportional to its size, so the explored region stays proportional to the starting debt. When a margin cannot be met, bins are removed instead, which also reduces debt.
  3. Priced steps. The matching objective and the local flow tests use one interface: find a circulation direction with enough improvement relative to its weighted length, and take a small exact step. Directions live in a changing forest; the data structure behind it, built in full, uses a routing sparsifier, frozen forest decompositions into local correction cycles, and prebuilt copies of paths, adapting the minimum-ratio-cycle machinery of the almost-linear flow algorithms.
  4. One program. A threshold search turns the cardinality question into perfect-matching questions on degree-3 graphs, keeping explicit witnesses. Capping every random retry and running all branches side by side with an exact fallback makes the bound hold on every computation path, while the error budgets keep the chance of success at least 2/3.

The numbers in the video

  • The Tutte–Berge formula, which counts odd components, matched the blossom algorithm’s maximum on 60 random graphs.
  • The best fractional matching with only vertex constraints exceeded the true maximum on 43 of 296 random graphs.
  • Tutte’s gadget for prescribed degrees agreed with brute force on 143 small instances.

Read the source

The paper

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

Transcript

Read the full script

0:00Matchings and odd cycles

A matching pairs up vertices along edges, using each vertex at most once, and the classic problem is to find a largest one. In bipartite graphs, alternating paths settle it. In general graphs, odd cycles get in the way: on a triangle, giving each edge 1/2 satisfies every vertex constraint, yet only one edge can be matched. Edmonds overcame this in 1965 by shrinking odd cycles, called blossoms, and his matching polytope adds constraints for odd sets. In our check, the Tutte–Berge formula, which counts odd components, matched the maximum on 60 random graphs, while the best fractional matching, with only vertex constraints, exceeded the true maximum on 43 of 296. For decades the best bound for sparse general graphs was that of Micali and Vazirani, m√n. Algebraic methods of Mucha, Sankowski and Harvey run in matrix-multiplication time, best on dense graphs. For bipartite graphs, a series of advances in flow algorithms, culminating in the almost-linear exact flow algorithms of Chen, Kyng, Liu, Peng, Probst Gutenberg and Sachdeva, and of van den Brand and coauthors, gave almost-linear exact matching. Sparse general graphs, with their odd blocks, stayed at the square-root bound.

1:23The claim

Result 120 is one OpenAI preprint, 86 pages, dated September 24. It claims one uniform randomized algorithm that finds a maximum-cardinality matching in any simple graph with n vertices and m edges in time (n + m)^(1+o(1)). The time bound holds on every computation path in a logarithmic-word model, and with probability at least 2/3 the output is an explicit maximum matching. No perfect matching is assumed, and on the densest graphs the bound is n^(2+o(1)). The same guarantees hold for finding a spanning subgraph with prescribed vertex degrees, called an f-factor, or deciding that none exists. This follows Tutte’s reduction to perfect matching, with rearrangeable networks so that high-degree vertices do not blow up the instance. In our check, Tutte’s gadget agreed with brute force on 143 small instances. There is no Lean proof of the theorem; a few files that OpenAI’s catalog does not link check one ingredient, the degree-reduction lemma.

2:35How the algorithm works

The core subproblem is a perfect matching in a graph of maximum degree 3; a reduction handles general inputs while keeping the original edge names. The algorithm stores its current matching through a partition: odd blocks called bins, each matched internally apart from one exposed vertex; single vertices called rows, assigned along edges to distinct bins; and matched pairs. Ledgers split a fixed amount from each row among its neighboring bins. At a settled state the lowest ledger certifies a strict Hall surplus, and the highest carries a logarithmic objective that can always improve when a perfect matching exists and no structural step is available. Repairs are exact flow problems on row-bin incidences, initially explored only where debt is large relative to bin size. An unexplored bin accepts flow optimistically; if enough arrives, the bin is explored and locks in an amount proportional to its size, so the region explored stays proportional to the starting debt. When a margin cannot be met, bins are removed instead, which also reduces debt. Debt pays both for exploration and for structural change. Both the matching objective and these local flow tests use one interface: find a circulation direction with enough improvement relative to its length, and take a small exact step. Directions live in a changing forest, so a long path need not be expanded at every step. The data structure behind it is built in full: a routing sparsifier, frozen forest decompositions into local correction cycles, and prebuilt copies of paths, adapting the minimum-ratio-cycle machinery of the almost-linear flow algorithms. A threshold search turns the maximum-cardinality question into perfect-matching questions on degree-3 graphs, keeping explicit witnesses. A single finite program, with one exponent envelope for every density, then gives the bound in the theorem. Capping every random retry, and running all branches side by side with an exact fallback, makes the bound hold on every computation path, while the error budgets keep the chance of success at least 2/3.

4:49Where it stands

The preprint is not peer reviewed and has not been revised, and there is no Lean proof of the theorem. It is not among those OSVerify reviewed, and we have seen no expert review. A claim of this size would need careful independent checking of all 86 pages. If it holds, maximum matching in general graphs joins bipartite matching and maximum flow in almost-linear time, below the square-root bound that has stood since Micali and Vazirani in 1980.

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.