Why Lean is faster than Rust — kim@lean

kim@lean : ~/bloghomepostsgithubrss

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<br># and prints the resulting size in bytes; `time` reports wall-clock.<br>$ time deflate-rust silesia.tar # miniz_oxide (pure Rust, no 'unsafe')<br>68112144<br>real 0m5.78s

$ time deflate-lean silesia.tar # lean-zip<br>67944712<br>real 0m4.97s

What's going on here? This is the lean-zip implementation of DEFLATE<br>compressing the standard silesia compression benchmarking corpus,<br>faster and better than miniz_oxide, the standard pure-Rust implementation.

How is that even remotely possible? The secret is this:

/-- Unified DEFLATE roundtrip: inflating what we deflate returns the input exactly. -/<br>theorem inflate_deflateRaw (data : ByteArray) (level : UInt8)<br>(maxOutputSize : Nat) (hsize : data.size ≤ maxOutputSize) :<br>inflate (deflateRaw data level) maxOutputSize = .ok data :=<br>Zip.Native.Deflate.inflate_deflateRaw data level maxOutputSize hsize<br>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 optimization process (using a combination of Claude and Codex agents).

(Note these graphs are measuring the geometric mean of the compression ratios across the constituent files in silesia.tar, so it's a slightly different measurement than our first measurement.)

We're not nearly as fast as miniz_oxide's L1 (the least compression, fastest throughput setting). At its L2 we now win outright: very slightly better compression, at 20% higher throughput. For miniz_oxide's L3 and L4, at the corresponding compression ratio we're a bit slower (worst is L4, 10% slower), and at L5 we've drawn level. But then for L6-L9, miniz_oxide is dominated: lean-zip is capable of compressing faster and better. The headline numbers in this post are taken from L6, the typical default for zip algorithms. At miniz_oxide's L9 we're nearly twice as fast.

I still can't quite believe that!

You might say, of course "well, no one has tried running these agents on miniz_oxide, trying to optimize it in the same way". And this is certainly fair: I'm sure we could improve the performance! But would we trust it? Are the AIs introducing subtle bugs that aren't picked up by the current test suites? We'd have to carefully audit and review everything it suggests. But on the Lean side we just shrug and say "inflate (deflateRaw data level) = .ok data still holds, so I guess it's fine".

For completeness, here's the Pareto frontier graph showing a number of other DEFLATE libraries:

lean-zip is certainly not the best here: libdeflate unsurprisingly blows it out of the water (unsurprisingly because this is a very carefully tuned implementation using architecture-specific SIMD, that we can't touch in Lean).<br>zlib-ng and zlib-rs are faster than us across most of the range their curves cover, but no longer at the deep end: their L9 lands at exactly the compression ratio lean-zip reaches at L7, and we get there faster than either (a little ahead of zlib-rs, 11% ahead of zlib-ng). zlib-ng is optimized C; zlib-rs is a memory-safe Rust implementation heavily based on zlib-ng, with some carefully contained unsafe internally.

We're competitive with or simply better than the other libraries. We completely dominate the OCaml, JavaScript, and zlib C reference implementations, and lose at lower levels but win at high levels against Go, pure Rust (miniz_oxide), and Zig.

There are also some caveats that are worth thinking about:

The Lean implementation has higher memory consumption than miniz_oxide.

There are some trust gaps because we use Lean's @[extern] annotation to provide a few low-level functions (e.g. word-sized reads from a ByteArray) that are currently missing from the Lean runtime. We're pushing Lean's readiness as a general purpose programming language, so these will probably be added to the runtime soon.

Proving...