Adam Langley published an experience report on using large language models as proof automation in the dependently-typed language Lean, built around a toy Zstandard (RFC 8878) decompressor he wrote to learn the language and the format. He states that several LLMs automatically produced a proof of a four-part well-formedness theorem about his FSE table-construction implementation — covering table size, per-symbol state counts, valid next-state arithmetic, and unique reachability of every target state per symbol — in roughly 20 minutes and within a fraction of a $20/month subscription quota, with the proofs type-checking and containing no sorrys. He frames this against the seL4 retrospective, which reported about 10x more time spent proving than designing and implementing, and more than 20x as many lines of proof as C code.