Planar Graph Metrics Embed into L1 with Constant Distortion

Comments and discussion

• Hung Le, OpenAI Math Dump Hits My Home (Rambling on Graphs, 2026-10-07; updated through 2026-10-20). Discusses both embedding claims and records an ongoing detailed reading of the planar proof, highlighting the column model and charts; the author reports increasing confidence while still working to internalize the argument. [family-level]

Formalization

• OpenAI math release, Bounded-distortion L₁ embeddings of planar and bounded-treewidth graphs: Lean scope (lean/docs/089.md, 2026). Describes the scope of the release's own Lean formalization of the planar result (one constant $C$ for all finite connected planar graphs with positive real edge lengths) and links the Comparator statement PlanarL1.lean. [family-level]

Possibly relevant literature (found by the agent, not checked)

• Hsien-Chih Chang, Jonathan Conroy, William Eliot, Hung Le, Vinayak, Peeling Half the Onion: Embedding k-Outerplanar Graphs into ℓ1 and Trees with a Polynomial Distortion (in k) (arXiv:2610.10888, 7 October 2026). Improves the $2^{O(k)}$ bound of Chekuri et al. for $k$-outerplanar graphs, which the paper cites as prior work, to a bound polynomial in $k$; it calls the planar ℓ1-embedding conjecture "still-open" and does not mention the release.
• Yuri Rabinovich, On average distortion of embedding metrics into the line and into L1 (STOC 2003, doi:10.1145/780606.780609). Shows that planar shortest-path metrics embed into $\ell_1$ with constant average distortion, a weaker form of the paper's Theorem 1.1 that the paper's bibliography does not cite.

Digests and expositions

• Latent Seminar, Constant-distortion L1 embeddings of planar and bounded-treewidth graphs (2026-10-06). Explains cut metrics, the planar column and scale constructions, and the treewidth particle and reservation mechanisms, explicitly limiting its review to statements and selected proof mechanisms rather than independent verification of the complete proofs. [family-level]