El proyecto lean-zip, una implementación del algoritmo de compresión DEFLATE escrita en el lenguaje de programación Lean, consigue resultados de compresión más rápidos y con mejor ratio que miniz_oxide, la implementación de referencia en Rust puro. Sobre el corpus estándar Silesia (212 MB), lean-zip produce un archivo de 67.944.712 bytes frente a los 68.112.144 de miniz_oxide en 5,24 segundos frente a 5,77 segundos, usando el nivel 6 por defecto. En el nivel 9, lean-zip es un 70 % más rápido.
La clave del experimento no es solo el rendimiento, sino el método. La biblioteca está formalmente verificada: un teorema garantiza que descomprimir lo comprimido devuelve exactamente los datos originales. Esa prueba permite delegar la optimización del código a agentes de IA (Claude y Codex) de forma autónoma, ya que cualquier cambio material en la implementación exige actualizar la demostración. En Rust, confiar en optimizaciones automáticas requeriría auditoría humana continua.
En la frontera de Pareto global, lean-zip no vence a libdeflate, ajustado con SIMD específico de arquitectura, ni a zlib-ng (C optimizado) ni a zlib-rs (Rust seguro basado en zlib-ng). Sí domina las implementaciones en OCaml y JavaScript, y supera a Go, Zig y a la zlib de referencia en niveles altos de compresión. Sus limitaciones incluyen mayor consumo de memoria, uso de la anotación @[extern] para operaciones de bajo nivel aún no cubiertas por el runtime de Lean, y una descompresión un 45 % más lenta que miniz_oxide. El autor concluye que el resultado no demuestra que Lean sea más rápido que Rust en general, sino que un algoritmo básico en Lean puede acercarse al rendimiento de lenguajes optimizados para velocidad, y que el trabajo de afinado es delegable a IA cuando existen teoremas que certifican la corrección.