<p>As pointed out in a comment above, the answer is yes, in Lean.  See the paper and the code as linked into comments.</p>
<p>I was rather hoping Agda or Idris... but perhaps the Lean formalization is actually constructive.</p>

CC BY-SA 4.0
2021-02-16T12:15:43.347Z
I can't imagine they managed to make it non-constructive...
Andrej Bauer
CC BY-SA 4.0
2021-02-09T15:52:19.940Z
2021-02-09T15:52:19.940Z
Jacques Carette
<p>Has anyone formalized, in a proof assistant (constructively!) the correctness of the computation of <a href="https://en.wikipedia.org/wiki/Levenshtein_distance" rel="nofollow noreferrer">Levenshtein distance</a> ? The <a href="https://cstheory.stackexchange.com/questions/10391/proof-of-levenshtein-distance">related Q&amp;A</a> on here is about paper proofs.  Searching around did not come up with any leads.</p>
<p>Note that I'm equally interested in correctness as that of a proof of optimality, i.e. knowing that an algorithm returns a correct sequence of edits, from which the distance is trivially computed, is quite interesting too. That the sequence is optimal can be a second step.</p>

CC BY-SA 4.0
2021-02-08T18:25:50.697Z
Have you seen https://ieeexplore.ieee.org/document/8664354?
Tyilo
CC BY-SA 4.0
2021-02-09T15:50:10.243Z
I had not, thanks. This leads to https://manau.jp/Lean/cotoleta/ as a place where I can download a Lean formalization.
Jacques Carette
CC BY-SA 4.0
2021-02-11T22:02:41.777Z
@Tyilo your comment should be the accepted answer.
Hermann Gruber
<proof-assistants><edit-distance>
Formal proof of correctness of Levenshtein distance
Jacques Carette
# Formal proof of correctness of Levenshtein distance

(Asked by: username_0 on 2021-02-04)

Has anyone formalized, in a proof assistant (constructively!) the correctness of the computation of [Levenshtein distance](https://en.wikipedia.org/wiki/Levenshtein_distance) ? The [related Q&A](https://cstheory.stackexchange.com/questions/10391/proof-of-levenshtein-distance) on here is about paper proofs. Searching around did not come up with any leads.

Note that I'm equally interested in correctness as that of a proof of optimality, i.e. knowing that an algorithm returns a correct sequence of edits, from which the distance is trivially computed, is quite interesting too. That the sequence is optimal can be a second step.

**Tags:** proof-assistants, edit-distance

> **Comments:**
> **username_1**: Have you seen https://ieeexplore.ieee.org/document/8664354?  
> **username_0**: I had not, thanks. This leads to https://manau.jp/Lean/cotoleta/ as a place where I can download a Lean formalization.  
> **username_2**: @username_1 your comment should be the accepted answer.  

---

## 1 answers

### Answer by username_0 on 2021-02-09. Score: 1

As pointed out in a comment above, the answer is yes, in Lean. See the paper and the code as linked into comments.

I was rather hoping Agda or Idris... but perhaps the Lean formalization is actually constructive.

> **Comments:**
> **username_3**: I can't imagine they managed to make it non-constructive...  

---

