- Sources: ImperialViolet, HN 49062291
- Summary: Adam Langley published a post dated 2026-07-26 describing a Zstandard decompressor written in Lean. What he proves is one scoped theorem about FSE table construction, named
ofDistribution_wellFormed, not the decompressor as a whole, and he states he is not publishing the code. He cites the seL4 retrospective, which reported roughly ten times as much time spent proving as designing and implementing and more than twenty times as many lines of proof code as C code, as the cost that made dependently-typed languages niche. He writes that LLMs promise to be an extremely capable form of proof automation, that perhaps proof engineering no longer needs as much attention, and that LLMs potentially make dependent-type systems dramatically more practical. He qualifies that much more experience would be needed and that proof effort may scale poorly in larger systems. He contrasts LLM proof automation with SMT-based approaches such as F*, where he describes solver behaviour as difficult to predict, and reports that in his limited tests LLMs avoided blowing up the type checker. The post also carries his own compression measurements on 64 MiB of Lean and mathlib source taken on an Apple machine, and notes that Apple's gzip is unusually optimised. - Why it matters: The suggestion is that machine-generated proofs could remove much of the proof-engineering overhead that kept dependent types out of production, which is distinct from the usual code-generation claims and is testable by anyone with a spec-heavy component.
send feedback on this story