AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

L_1 Embeddings of Graphs of Bounded Treewidth

Can the mathematical statement in L_1 Embeddings of Graphs of Bounded Treewidth be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 089)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'L_1 Embeddings of Graphs of Bounded Treewidth'. For every fixed treewidth bound, the shortest-path metrics of finite connected graphs with arbitrary positive real edge lengths embed into real L1 with uniformly bounded distortion. This resolves the bounded-treewidth case of the Gupta–Newman–Rabinovich–Sinclair conjecture positively.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 089). The Lean development was not rebuilt locally.