String compression algorithms

Stream: Is there code for X?

[Shreyas Srinivas]

Do we have proofs of correctness of compression algorithms? I am specifically interested in Lempel-Ziv. I know this stuff isn't in mathlib but I recall someone bringing this up before. Searching on zulip doesn't yield any results though