# Almost-linear approximation of edit distance

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

- [An Almost-Linear Approximation Scheme for Edit Distance](../../preprints/An-Almost-Linear-Approximation-Scheme-for-Edit-Distance-September-24-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Almost-linear randomized approximation of edit distance | [EditApproximation.lean](../ComparatorChallenges/EditApproximation.lean) |