Why Lean is faster than Rust
3 days ago
- Lean's DEFLATE implementation (lean-zip) outperforms pure Rust's miniz_oxide in both compression speed and ratio at most levels, e.g., 30% faster at level 6.
- The performance advantage is enabled by a formal proof of correctness (inflate_deflateRaw theorem), which allows AI agents to optimize the code autonomously without human review, ensuring no bugs are introduced.
- Pareto frontier graphs show lean-zip dominates miniz_oxide across all compression levels, and is competitive with optimized libraries like zlib-ng and zlib-rs at high levels.
- Caveats include higher memory consumption, slower decompression (1.45x slower), reliance on Lean's extern annotations for low-level functions, and that the proof only covers round-trip correctness, not side channels or performance.
- The experiment demonstrates that with formal verification, AI-driven optimization can make Lean competitive with fast languages for basic algorithms, but it is not a general claim that Lean is faster than Rust.