Lean 4 + LLMs: Proof Automation Gets Real

A developer built a complete Zstandard (zstd) decompressor in Lean 4, using LLMs to automate proof generation. The project shows that combining dependently-typed languages with modern AI can slash the proof overhead that has historically limited these tools to niche use.

The Proof Burden

Dependently-typed languages like Lean, Coq (now Rocq), and F* let you encode invariants in the type system. But the cost is high: the seL4 project reported spending 10x more time proving than implementing, with 20x more proof code than C code. Traditional automation via SMT solvers (F*) works for simple cases but often sends solvers into infinite loops.

Proof Irrelevance + LLMs

A key insight: once a statement is proven correct, the proof's content doesn't matter — only its existence does. This "proof irrelevance" means an LLM can generate a proof that just needs to type-check, not be elegant. The author tested this with Lean's by blocks and found LLMs rarely trigger type-checker blowups.

Zstandard and FSE Entropy Coding

Zstandard is winning the compression war. On 64 MiB of Lean source, zstd achieves ~500 MiB/s decompression vs gzip's ~200 MiB/s (Apple's optimised gzip) and bzip2's ~50 MiB/s. The key is FSE (Finite State Entropy), a state-machine-based entropy coder.

FSE uses a table of states (minimum 32 in zstd). Each symbol gets a fraction of states proportional to its probability. For example, with 16 states and symbol B at probability 5/16, B gets 5 states. Some states read 1 bit, others 2, averaging to the ideal fractional bits (-log2(5/16) = 1.68). The encoder works backwards: it must choose which state to land in, carrying fractional bits forward.

Lean Implementation Details

The decompressor implements the full zstd RFC. A key function type: read n bytes from stream, returning a proof that bytes were read. The LLM (here, Claude) generates the proof automatically. The author notes that the RFC is terse — section 4.1 required multiple reads — but the LLM handled the logic.

Practical Takeaways

  1. LLMs eliminate proof engineering overhead: You no longer need to structure proofs for maintainability; just regenerate them after code changes.
  2. Type-checker blowups are rare: In limited tests, LLM-generated proofs avoided the exponential blowups that hand-written proofs can cause.
  3. Zstandard is a good target: Its RFC is complex enough to test formal verification but not so large as to be impractical.

The full decompressor code is available on GitHub. For developers considering dependently-typed languages for production, this project suggests the proof cost may finally be manageable.

Getting Started

If you want to try this yourself:

  • Install Lean 4 (nightly 2026-07-01+)
  • Use an LLM API (Claude or GPT-4) with a prompt like: "Prove the following Lean theorem: ..."
  • Start with simple lemmas, then work up to complex state machines.

The author's zstd decompressor is at github.com/imperialviolet/zstd-lean. Study the FSE.lean file for a concrete example of LLM-generated proofs in action.