Fast DEFLATE compression in Lean

Summary

kim@lean:~$ cat posts/2026·07·24.md Why Lean is faster than Rust 2026·07·24 [performance] [lean] I can't possibly be serious, can I, claiming that Lean is faster than Rust? Let me show you something: # silesia.tar: the 212 MB standard corpus. Each tool compresses at level 6 # and prints the resulting size in bytes; `time` reports wall-clock. $ time deflate-rust silesia.tar # miniz_oxide (pure Rust, no 'unsafe') 68112144 real 0m5.77s $ time deflate-lean silesia.tar # lean-zip 67944712 real 0m5.24s What's going on here? This is the lean-zip implementation of DEFLATE compressing the standard silesia compression benchmarking corpus, faster and better than miniz_oxide, the standard pure-Rust implementation. How is that even remotely possible? The secret is this: theorem inflate_deflateRaw (data : ByteArray) (level : UInt8) (maxOutputSize : Nat) (hsize : data.size ≤ maxOutputSize) : inflate (deflateRaw data level) maxOutputSize = .ok data := Zip.Native.Deflate.inflate_deflateRaw data level maxOutputSize hsize The Lean library isn't just tested and validated, it's proved correct. This allows us to let AIs loose optimizing the code, requiring that they update the proof whenever the implementation materially changes. This gives us the confidence to allow them to work autonomously in a way that would be unthinkable in other languages. What comes out of this process is astonishing. These graphs show the "Pareto frontier", describing the compression ratio vs throughput tradeoff for the lean-zip and miniz_oxide implementations. Like all DEFLATE implementations, both libraries have a tunable knob (the "level") that gives better compression in exchange for lower throughput. The way these graphs are set up, further left is better compression, further up is better throughput. The green line shows what you get as you sweep through the levels using miniz_oxide, compressing the silesia corpus. The animated red line shows what you get for lean-zip, over the course of the autonomous opti...