Bounded-distortion L₁ embeddings of planar and bounded-treewidth graphs

2 papersLean

Resolves the planar and bounded-treewidth cases of the Gupta–Newman–Rabinovich–Sinclair conjecture. Shortest-path metrics of finite connected graphs with arbitrary positive edge lengths embed into real L₁ with universal distortion for planar graphs, and distortion depending only on treewidth for bounded-treewidth graphs. The corresponding multicommodity flow–cut gaps are uniformly bounded.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

Planar Graph Metrics Embed into L1 with Constant Distortion

OpenAI · September 23, 2026

We prove that every finite connected planar graph with arbitrary positive real edge lengths embeds into real L₁ with a universal distortion bound. This resolves the planar embedding conjecture positively.

Read PDF Download Source

Cite

@misc{OAI:Planar-Graph-Metrics-Embed-into-L1-with-Constant-Distortion-September-23-2026,
  author = {{OpenAI}},
  title = {{Planar Graph Metrics Embed into $L_1$ with Constant Distortion}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Planar-Graph-Metrics-Embed-into-L1-with-Constant-Distortion-September-23-2026/paper.pdf}{OAI:Planar-Graph-Metrics-Embed-into-L1-with-Constant-Distortion-September-23-2026}},
  year = {2026}
}

L1 Embeddings of Graphs of Bounded Treewidth

OpenAI · September 23, 2026

For every fixed treewidth bound, the shortest-path metrics of finite connected graphs with arbitrary positive real edge lengths embed into real L₁ with uniformly bounded distortion. This resolves the bounded-treewidth case of the Gupta–Newman–Rabinovich–Sinclair conjecture positively.

Read PDF Download Source

Cite

@misc{OAI:L1-Embeddings-of-Graphs-of-Bounded-Treewidth-September-23-2026,
  author = {{OpenAI}},
  title = {{$L_1$ Embeddings of Graphs of Bounded Treewidth}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/L1-Embeddings-of-Graphs-of-Bounded-Treewidth-September-23-2026/paper.pdf}{OAI:L1-Embeddings-of-Graphs-of-Bounded-Treewidth-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The planar case of the Gupta–Newman–Rabinovich–Sinclair embedding problem asks for a universal distortion bound in \(L_1\). The formalized result gives one constant \(C\) for every finite connected planar graph with arbitrary positive real edge lengths: its weighted shortest-path metric embeds into real \(L_1\) with distortion at most \(C\). The constant is independent of the number of vertices and the ratios between edge lengths; singleton graphs are included.

The formalized result gives a uniform \(L_1\) embedding bound for each bounded-treewidth class. For every bag-size bound \(k\ge2\), there is a constant \(C(k)\) such that the weighted shortest-path metric of every nonempty finite connected graph with a tree decomposition of bag size at most \(k\) embeds into finite-dimensional real \(L_1\) with distortion at most \(C(k)\). Edge lengths may be arbitrary positive real numbers, and the constant is independent of the graph and decomposition size.

Comparator links

Result	Comparator statement
Planar graph metrics in \(L_1\)	PlanarL1.lean
Bounded-treewidth graph metrics in \(L_1\)	BoundedTreewidthL1.lean

Scope note on GitHub →