Using Astra to re-derive the optimal edit distance embedding bound
A researcher used Astra to produce a cleaner 2.5-page version of the 2005 proof that an edit distance embedding into l1 is optimal, checking steps in Lean and still seeking peer review.
One of the OpenAI results that dropped was some sharp lower bound for some known embedding result (that an embedding of edit distance into l1 that was published in 2005 is optimal). I saw this and used it as an opportunity to understand this embedding finally. The 2005 paper is quite finicky, and I was never able to fully understand what’s going on, but given how fundamental the problem is, and neat the answer is, I was always curious! (The optimal distortion is exp(sqrt(log n log log n)), and when it’s a bound like this, usually something interesting is going on). So I tried to prompt a cleaner version of the upper bound yesterday from Astra, and I think I succeeded (not in one shot, it required quite a bit of tinkering and understanding of what’s going on and where the bottlenecks are in the original proof)! The result is just 2.5 pages, where 1.5 pages are completely standard, and 1 page is some clean combinatorial fact about edit distance. I used Lean along the way to verify the steps in the proof. But most importantly, it allowed me to digest and enjoy the proof, while historically edit distance results like this were impenetrable for me. I am of course cautious that it can be slop and LLM psychosis, but after I slept I think it stands? Currently running it by some friends who understand this area well. I am obviously not going to post it or anything (our world does not need more math slop floating around right now), but I just thought it was a very satisfying experience intellectually.