There was recently a decently fast implementation of DEFLATE in Lean: https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-t...