The GNRS conjecture for planar and bounded-treewidth graphs
From OpenAI Aftermath
The Gupta–Newman–Rabinovich–Sinclair (GNRS) conjecture predicts that, for every proper minor-closed family of finite graphs, the shortest-path metrics of graphs in the family, with arbitrary positive edge lengths, embed into L1 with uniformly bounded distortion. Equivalently, the undirected multicommodity flow–cut gap is uniformly bounded on such a family. Two manuscripts dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claim the planar case and the bounded-treewidth case. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; this page does not certify them.
Background
- As recounted in the introductions of the manuscripts:
- The worst flow–cut gap on a fixed graph equals the worst L1 distortion of its weighted shortest-path metrics (Gupta, Newman, Rabinovich and Sinclair, Section 3, Theorem 3.2).
- For n-vertex planar metrics the general preceding bound was O(√log n), due to Rao, through Euclidean space. Newman and Rabinovich showed that even series-parallel metrics can require Ω(√log n) distortion into Euclidean space.
- Constant L1 distortion was known for series-parallel graphs (Gupta, Newman, Rabinovich and Sinclair), with the sharp value 2 (upper bound of Chakrabarti, Jaffe, Lee and Vincent; matching lower bound of Lee and Raghavendra), and for planar graphs of bounded outerplanarity (Chekuri, Gupta, Newman, Rabinovich and Sinclair). Further results restrict the pairs to be preserved (terminals on few faces) or the geometry (Sidiropoulos's nonpositively curved planar metrics).
- For bounded treewidth, Lee and Sidiropoulos settled bounded pathwidth through stochastic embeddings into trees, and Abraham, Filtser, Gupta and Neiman obtained O(√p) distortion for pathwidth p. The manuscript notes that dominating trees cannot give a uniform bound for all bounded-treewidth graphs, and names the local-consistency theorem of Chlamtáč, Krauthgamer and Raghavendra as its closest precursor.
The original results
- Planar graphs. Theorem 1.1 of Planar Graph Metrics Embed into L1 with Constant Distortion states that there is a universal constant C such that the shortest-path metric of every finite connected planar graph with positive real edge lengths embeds into a real L1 space with distortion at most C. The constant does not depend on the number of vertices or on the edge lengths. The manuscript also states the corresponding universal bound on the undirected fractional flow–cut gap for planar graphs.
- Bounded treewidth. Theorem 1.1 of L1 Embeddings of Graphs of Bounded Treewidth states that for every bag-size bound k ≥ 2 there is a constant Ck such that every finite connected graph with a tree decomposition whose bags have at most k vertices embeds with distortion at most Ck, for every positive edge-length function. The manuscript gives no explicit estimate for Ck. By the excluded-planar-minor theorem of Robertson and Seymour, it states, the result also gives a uniform bound for graphs excluding any fixed planar graph as a minor.
- Almost-embeddable families. The planar manuscript combines both theorems with a stochastic reduction of Lee and Sidiropoulos to obtain uniform distortion, and flow–cut, bounds for each fixed-parameter almost-embeddable family in their sense. It states that this "does not establish closure under general clique sums of order greater than one, and therefore does not prove the full GNRS conjecture".
- Method, as described: the planar proof represents the graph by a non-crossing column model and builds random families of cuts through charts attached to points. Component separation limits which pairs need further updates, which yields a packing bound for the surviving pairs, and an interpolation step makes local formulas agree exactly at their interfaces, so that the updates combine without a loss proportional to the number of scales. The treewidth proof constructs cut laws on the bags of a tree decomposition, glues consistent laws by the Markov sampling principle of Chlamtáč, Krauthgamer and Raghavendra, and adds anchor cuts built from the padded decompositions of Filtser and coauthors.
- Sources. At commit
1581d4c: Planar Graph Metrics Embed into L1 with Constant Distortion and L1 Embeddings of Graphs of Bounded Treewidth. - Formalization, as described by the repository. The scope note states that the formalization gives one constant for every finite connected planar graph with arbitrary positive real edge lengths, and a constant C(k) for each bag-size bound k ≥ 2, independent of the graph and decomposition size. The Comparator statements are PlanarL1.lean and BoundedTreewidthL1.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 25 October 2026) |
|---|---|---|---|---|
| 2026-10-07 to 2026-10-20 | H. Le, OpenAI Math Dump Hits My Home, blog Rambling on Graphs | Reading (dated reading log of the planar manuscript) | A researcher on both problems records reading Sections 2–9 of the planar manuscript. On 19 October he writes that he is "more confident that the proof is correct (hard to put a percentage, but 90% would be a reasonable number)", identifies the column model and the per-point charts as its two main ideas, and reports that the constant remains very large (about 1073 after an optimization with ChatGPT Astra). He names the minor-free case as a natural next step, via the Robertson–Seymour decomposition. | Blog post with dated updates; personal reading notes, not a published verification. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit 22ef46c, 24 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full" and records sandboxed Comparator passes for PlanarL1 and BoundedTreewidthL1. Its note says that both embedding theorems are stated but the flow–cut-gap corollary is not, and that planarity is defined by a custom drawing predicate. |
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 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the PlanarL1 solution (394 s, run 38019899278) and the BoundedTreewidthL1 solution (349 s, run 38017370880). |
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 lists neither challenge of this family, so both were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-13 | K. Adler, keithadler/planar-l1-companion and keithadler/planar-l1-lean | Reading (section notes) and partial formalization | Section-by-section notes on the planar manuscript, written by an AI for the author and tagged by status, giving "no verdict on the main theorem". The companion Lean repository formalizes selected lemmas of Sections 3, 5 and 6 (356 declarations, standard axioms only), with the inputs from other sections taken as explicit hypotheses. | Both repositories describe themselves as unreviewed by experts; the Lean repository is conditional and states that its authors did not compile OpenAI's formalization. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscripts.
- Independently, Chang, Conroy, Eliot, Le and Vinayak (arXiv:2610.10888, 7 October 2026) embed k-outerplanar graphs into L1 and into distributions over trees with distortion polynomial in k, improving the earlier exponential bound. Their introduction describes the planar conjecture as open and does not cite the OpenAI manuscripts. It also records Lee and Poore's resolution of the 2-sum case of the clique-sum conjecture and that nothing is known for sums of order at least three.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
