Convex and metric geometry·OpenAI Math·Result 099·Lean formalisation listed
The sharp exponential scale of edit-distance distortion
One of the 372 results in OpenAI's public mathematics catalogue, filed under convex and metric geometry: 3 preprints, the latest dated 27 September 2026. This page quotes OpenAI's own summary of the claim, links the papers and abstracts, and will embed the animation.
Latest paper
Edit Distance in l1: Matching Bounds up to Constants in the Exponent
The animation for this result has not been released yet. Subscribe on YouTube to catch it.
What OpenAI claims
Determines the least distortion of embedding edit distance on words of length at most d into real ℓ1: it is exp(Θ(√(log d log log d))). Insertions, deletions and substitutions have unit cost. The constants are uniform over all finite alphabets with at least two symbols, even when the alphabet grows with d; binary words already force the lower bound. (Lean)
Papers (3)
Edit Distance in l1: Matching Bounds up to Constants in the Exponent
We determine the exponential scale of the least ℓ1 distortion of unit-cost edit distance on all strings of length at most d. For every sufficiently large d, uniformly over finite alphabets of size at least two, the distortion lies between exp(c√(log d log log d)) and exp(C√(log d log log d)) for absolute constants c,C > 0. The lower bound already holds on binary strings of one common length. Thus the order of logarithmic distortion is sharp up to absolute constants.
Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance
We give two finite-circle constructions of binary strings whose least ℓ1 distortion is exp(Ω(√(log d log log d))), where d bounds their length. Both constructions supply words of one common length for every sufficiently large cap. Two direct binary coding arguments transfer the constructions with absolute distortion and logarithmic block width. We also develop the overlapping-substring method of Ostrovsky and Rabani into a complete finite histogram embedding at the same exponential scale, uniformly over all finite alphabets and all words of length at most d, including the empty word.
Tree Constructions for the l1 Distortion of Binary Edit Distance
We give two independent constructions of binary words of one length at most d whose ordinary edit-distance metrics require ℓ1 distortion exp(Ω(√(log d log log d))) for every sufficiently large d. We also prove a constant-distortion binary conversion for one prescribed input length. Together with the companion upper embedding theorem, these lower bounds determine the order of logarithmic distortion uniformly over finite alphabets with at least two symbols.
Status
Preprint. The papers have not been independently reviewed. Treat the result as OpenAI's claim until other mathematicians have checked it. If a video exists, it illustrates the statement; it is not the proof.
Related results in Convex and metric geometry
- 100Cylinder coverings below the half-area boundLean
- 101The sharp simplex conjecture for isotropic constants
- 087The Mahler conjectures, functional inequalities and polar-product symplectic widthVideoLean
- 088Sharp projection-body inequalities and a counterexample to simplex maximizationLean
- 089Bounded-distortion L1 embeddings of planar and bounded-treewidth graphsLean
- 090Triangular-lattice optimality, long-range Riesz and Coulomb energies, and spherical logarithmic energyLean