LLMs as Proof Automation: Building a Zstandard Decompressor in Lean

Dependently-typed languages like Lean and Rocq (formerly Coq) can encode arbitrarily subtle invariants directly into the type system and have a machine check them — the kind of correctness guarantee that decays into stale comments in ordinary code. The catch has always been cost: proving simple facts can eat entire days, and the seL4 project famously spent roughly 10x more effort on proofs than on design and implementation, ending with over 20x more proof code than C. Earlier automation attempts, like F*‘s reliance on an SMT solver, help in easy cases but turn into ‘mysticism’ when the solver wanders off for hours, forcing developers to intuit what will keep it happy.

The author’s bet is that LLMs change this calculus. Because proofs are largely irrelevant once a statement is shown true — only the proof’s existence matters — an LLM that can grind out and repair proofs cheaply removes much of the ‘proof engineering’ burden that made these languages niche, while still managing to avoid blowing up the type checker in early tests. If it holds up, dependent types could become dramatically more practical for everyday code.

To kick the tires, the author implemented a Zstandard decompressor in Lean. The piece doubles as a clear explainer of Zstandard’s entropy coding: Huffman trees are fast but waste bits by rounding each symbol to a whole number of bits, so Zstandard adds FSE, a state machine where each symbol gets a share of states proportional to its probability. By splitting a symbol’s states between reading one bit and two bits, FSE hits fractional bit-lengths on average — and since the state table is rebuilt from transmitted probabilities via the RFC’s algorithm, it never has to be sent.