∑math20

Theoretical computer science · Result 121

Almost-linear approximation of edit distance

1 paperLean

For every fixed rational \(\varepsilon\in(0,1)\), gives a randomized \((1+\varepsilon)\) approximation to unit-cost edit distance in worst-case expected time \(N^{1+o(1)}\), with success probability at least 2/3. The strings have total length N and polynomially bounded integer symbols. This is an asymptotic guarantee at fixed accuracy.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of An Almost-Linear Approximation Scheme for Edit Distance

An Almost-Linear Approximation Scheme for Edit Distance

OpenAI · September 24, 2026

We give a uniform randomized approximation scheme for unit-cost edit distance. For every fixed rational \(\varepsilon\in(0,1)\), it estimates the distance between arbitrary explicitly stored strings of total length N within a factor \(1+\varepsilon\) with probability at least 2/3, in worst-case expected time \(N^{1+o(1)}\) on a logarithmic-word RAM. The algorithm supports polynomially bounded integer alphabets and returns zero deterministically on equal strings.

Read PDF Download Source

Cite
@misc{OAI:An-Almost-Linear-Approximation-Scheme-for-Edit-Distance-September-24-2026,
  author = {{OpenAI}},
  title = {{An Almost-Linear Approximation Scheme for Edit Distance}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-Almost-Linear-Approximation-Scheme-for-Edit-Distance-September-24-2026/paper.pdf}{OAI:An-Almost-Linear-Approximation-Scheme-for-Edit-Distance-September-24-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 formalization gives a randomized \((1+\varepsilon)\)-approximation for unit-cost edit distance between explicitly stored integer strings, for every fixed rational \(0<\varepsilon<1\). Its estimate is at least the true distance and at most \((1+\varepsilon)\) times it with probability at least \(2/3\); equal strings return zero on every execution.

For total length at most \(N\) and integer symbols bounded by a fixed polynomial in \(N\), expected work is at most \((N+2)^{1+\eta}\) for every fixed \(\eta>0\) and all sufficiently large \(N\). Space is polynomially bounded on every execution.

Comparator links

ResultComparator statement
Almost-linear randomized approximation of edit distanceEditApproximation.lean

Scope note on GitHub →