Why Lean is faster than Rust — kim@lean

kim@lean:~$ cat posts/2026·07·24.md

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
68054183
real    0m4.57s

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:

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.)

lean-zip beats every single compression level miniz_oxide provides, i.e. we're capable of providing the same compression at higher throughput. At its fastest setting we're 15% quicker and the output is 8.8% smaller. At L6, the typical default for zip algorithms and where this post's headline numbers come from, we're 30% faster. At its L9 we're twice as fast.

(Slight caveat: to strictly beat miniz_oxide L3, we'd have to use a mixture of our L3 and L4.)

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). zlib-ng and zlib-rs are faster than us across most of the range their curves cover, though not at the deep end: their L9 lands at exactly the compression ratio lean-zip reaches at L7, and we reach it at about the same speed as zlib-rs, a few percent 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 that our implementation round-trips, produces a valid DEFLATE stream, and accepts any valid stream, is a good start, but doesn't address other interesting questions, e.g. absence of side channels or verified performance guarantees.

• Our decompression implementation is still slower: miniz_oxide decompresses about 1.45x faster.

I'm not really claiming that "Lean is faster than Rust". It's still much easier to sit down and produce a performant implementation in Rust than it is in Lean! This experiment merely shows that:

• It is possible, with lots of tuning, to get basic algorithms written in Lean competitive with implementations in "fast" languages.

• That effort is happily and surprisingly delegatable to AIs, when you can write theorems characterising the algorithm, allowing aggressive optimization without human review.

Still, it's food for thought, that we can get this close at all!