--- title: We have proof automation now | daily.dev description: Adam Langley explores using LLMs to automate proof generation in Lean, a dependently-typed programming language, by building a Zstandard decompressor. The post... canonical: https://daily.dev/posts/we-have-proof-automation-now-pwem29i8q twitter:card: summary_large_image twitter:site: @dailydotdev og:type: website og:site_name: daily.dev og:title: We have proof automation now | daily.dev og:description: Adam Langley explores using LLMs to automate proof generation in Lean, a dependently-typed programming language, by building a Zstandard decompressor. The post... og:url: https://daily.dev/posts/we-have-proof-automation-now-pwem29i8q og:image: https://api.daily.dev/og/posts/PweM29I8Q.png og:image:alt: We have proof automation now og:image:width: 1200 og:image:height: 630 og:locale: en --- > ## Documentation Index > Fetch the complete documentation index at: https://daily.dev/llms.txt > Use this file to discover all available pages before exploring further. # We have proof automation now **[Hacker News](https://daily.dev/sources/hn)** · 18 min read · 0 upvotes · 0 comments ## Summary Adam Langley explores using LLMs to automate proof generation in Lean, a dependently-typed programming language, by building a Zstandard decompressor. The post explains Zstandard's FSE entropy encoder in detail, then demonstrates how Lean's dependent types can encode and enforce subtle invariants — like array bounds safety — that would otherwise be mere comments in conventional languages. The key insight is that LLMs can now automatically discharge complex proof obligations in ~20 minutes for a fraction of a $20/month subscription, potentially making dependent-type systems practical for everyday software engineering. The post also covers Lean's practical features (strictness, monadic do-notation, in-place mutation optimization) and briefly explores verified assembly via AWS's LNSym project. ## Full article daily.dev links to this article rather than hosting it. Read it at the original source: ## Community take How the wider developer community reacted, aggregated from 1 discussion and 50 comments across hackernews (as of 2026-08-03). **TL;DR:** The community is cautiously optimistic that LLMs combined with theorem provers (especially Lean 4) represent a genuine step-change in making formal verification practical, but significant skepticism remains around the difficulty of writing correct specifications, choosing good abstractions, and scaling dependent types in real-world codebases. **Sentiment:** 45% positive · 35% mixed · 20% skeptical **The case for** - LLMs can fill in proof obligations automatically, meaning hallucinations are self-correcting since a wrong proof simply gets rejected by the type checker. - Even partial specifications (e.g., compress/decompress must be inverses) rule out vast classes of bugs cheaply. - Writing a clear spec is often much easier than writing the efficient implementation (e.g., the Quake III inverse square root example). - Recent tooling improvements (Lean 4, Mathlib, Batteries) and LLM capability have dramatically lowered the barrier compared to even 5 years ago. - Verified assembly optimization (à la Fiat Crypto/CryptOpt) is already deployed in production at Google, showing the approach is real. **The pushback** - Writing the correct specification is itself as hard as—or harder than—writing the program, and bugs in the spec propagate directly to the code. - LLMs are poor at choosing the right abstractions and proof decomposition strategies, which is often the crux of formal verification. - Dependent types intermingled with proofs across a codebase make maintenance very painful when new invariants need to be added. - LLMs tend to avoid fulfilling proof obligations unless heavily prompted, preferring to overfit or shortcut rather than do the hard proof search. - Lean has captured most mindshare but other mature systems (Coq/Rocq, Isabelle) risk being left behind, fragmenting the ecosystem. **By community** - hackernews (mixed): Commenters are genuinely excited about the LLM+theorem-prover combination but repeatedly stress that specification correctness, abstraction choice, and long-term maintenance of dependent types remain hard unsolved problems. **Hottest debate:** Whether writing a formal specification is substantially easier than writing the correct program itself, or whether it merely moves the bug-writing problem up one level. **Open questions** - How do you prevent specification drift from the original intent without continuous human supervision? - Will Lean's dominance crowd out more mature systems like Isabelle/HOL and Rocq, and does that matter? - Can LLMs be reliably prompted to conjure good proof obligations rather than just satisfying ones the user already specified? - Is there a practical path to a self-hosting, formally verified compiler that transfers proofs from source down to assembly? **Highlights** > Theorem provers have always made extensive use of AI and automation. Formal logic is insanely laborious, and it took Russell a monumental effort to not get very far with his manual verifications in Principia Mathematica, working out all the details by hand. In 1956, Newell came up with the Logic Theorist which was able to prove a decent chunk of the Principia automatically. When Newell informed him, Russell conceded that his manual efforts had turned out to be wasted effort. I used HOL Light about 15 years ago. The vast majority of the proof details are done by a machine, generally split between term rewriting and then offloads to a generic automated prover for first-order logic. Your job then is formalising the theorem statements and orchestrating the automation, and the latter still takes an enormous amount of labour. Around this time, we were getting excited about recommender systems for lemma selection. The idea was that you turn every theorem into a bunch of features and train a recommender system against the lemma needed to prove it. Then when you face a new problem, you use its features to recommend which lemmas are likely to be needed. You then throw those lemmas and your conjecture at a bunch of industrial strength automated provers, get the provers to come back with a minimal set of necessary lemmas, and then use your verified automated prover to do the real proof with a tractable set of inputs. It first got implemented in Isabelle/HOL as Sledgehammer, and was a massive improvement to tooling. Now LLMs are here and the game looks completely different. I went back over some verification I spent a week on about 5 years ago, in a pretty obscure formal verifier called HOL Light, on a problem of my own making. I'd seen how terrible ChatGPT was at propositional logic a few years back, so this is the sort of thing I'd had in my back-pocket as an "impossible benchmark" for LLMs. So as a half-joke, I gave Claude the main theorem I wanted proving, hoping to watch it embarrass itself. In a minute or two, it has come up with the same proof strategy I had used, proving four lemmas to get to the main theorem. This was impressive, but that's not the laborious part, and I was pretty confident it would die trying to prove just the first lemma. It has its four lemmas enumerated and goes to thinking, while I go off for a cup of tea. I come back five minutes later and it has scratched off the first goal. I'm pretty shaken, and go off again trying to process that. Come back, the second goal has gone. And then the third. And then the fourth. And then, after just fifteen minutes, it's pulled off a week of my work, done it more efficiently, and near enough one-shotted each proof. That took me a while to process. I realised that if I had this 15 years ago, it would have done 95% of my PhD, which is to say that 15 years ago, I would have done a 20x more ambitious thesis. I contacted my old supervisor, who said the theorem proving community are all on top of this, including the creator of HOL Light, now at AWS. HOL Light, incidentally, was used on what I still believe is the most ambitious mathematical theorem proving project to date, the verification of the Kepler Conjecture. The lead on that project recruited a team to get the proof through over about 5 years. Today, I wouldn't be surprised if he could have solo'd it in 6 months. The same goes for another extremely ambitious project, the verification of the seL4 microkernel. And for another open problem, I know there are people seriously wanting to get a verification of Fermat's Last Theorem, which sounded delusional 15 years ago, but sounds pretty plausible now. Exactly where this goes, I am not sure. I suspect we can now start on verification projects that would have been insane to contemplate. But a few things concern me. One is that Lean seems to have all the mind-share. Maybe it deserves it, but there are very major and mature theorem proving technologies such as Coq (now Rocq), Isabel > — [momentoftop on hackernews](https://news.ycombinator.com/item?id=49065741) > It is true that finding the correct specification is a formidable task; knowing what correctness even means is arguably most of the difficulty of programming. However! "Moving bugs up from programs to types" isn't how this shakes out in practice, at all. Another commenter already noted that it's often much easier to communicate your intent through specifications, because you can essentially always say what a computation should do much more simply than you can say exactly how to do it. I think it's also important not to miss the forest for the trees: even relatively simple specifications like "the compress and decompress functions must be inverses for all inputs" rules out vast classes of bugs in a compression library. This is not a complete specification; for instance, it does not speak about how the decompressor behaves on malicious input. But in my experience, even partial specifications carry the promise of hitting warp speed with LLMs in a way that I haven't seen anywhere else. After a certain level of specification, you have decent guarantees of being able to whole-heartedly forget about the implementation details of the synthesized program. And you get a better-built, more robust program out of it at the end! The comment at the end of the article about having LLMs directly generate assembly against specifications and letting them rip with finding custom optimizations is the sort of crazy stuff this enables. I really think we're only seeing the tip of the iceberg here. People keep asking what genuinely new things we can do now with LLMs that we couldn't before; this is the answer. > — [cayley\_graph on hackernews](https://news.ycombinator.com/item?id=49065390) > I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible. Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, with more elaborate properties and longer proofs. Suddenly, you realize that you need to prove a new property of your program. Can you keep your existing work and build on top of it? In general, no, you have to refine every dependent type everywhere by adding a new conjunct expressing a new invariant, and adapt every proof, as the new property is threaded in the existing program. That is because dependent types (and other staples of naive approaches to proving program properties, like a unique invariant per loop) structure the program along the wrong dimension: they encourage grouping everything that concerns a value ("put this value in a dependent type that encodes everything known about it") or a program point ("write the precondition for this function as a big conjunction mixing all the concerns"), where it works much better, for long-term maintenance, to structure the development along concerns: computational parts of the program, basic functional properties and absence of UB, termination, other functional properties, security, etc., where each layer builds on top of the previous ones without requiring them to change. That is not to say that dependent types do not have their use. Where they shine is a module boundaries. Consider a library that exposes an opaque type and operations on it. Users of the library can only build and modify values of that type through the library's API. This type should be a dependent type. If it needs to be refined at any point to encode a new invariant, this will have no impact on the library's users, since all they do is pass around values without interpreting them. However, inside the library, I would recommend unpacking/repacking the dependent type at the library's entry points and handling the concerns separately. > — [el\_pollo\_diablo on hackernews](https://news.ycombinator.com/item?id=49066421) > As a meta-comment on the topic, something I have noticed is that there still exists confusion what it means to use theorem provers for projects -- the other day I read a tweet from Paradigm, a crypto-VC now seemingly AI-pilled. Some LP of theirs had made a Lean 4 formalization of the Ethereum's virtual machine. The tweet said this would have cost like $150k in API tokens ("would have", as in, I guess they get theirs for free), and took a week of inference time for an LLM to produce. I somehow got distracted to actually take a look at the code, which I found rather light on theorems. Nor did the project make use of Batteries or Mathlib which are arguably the one of the strongest motivation for me personally to use Lean4. That is, I generally rather rely on someone else getting the category theory and algebraic structures right, which then leaves me the proof obligation to show the correspondence with whatever toy I'm working on. Here I'm fine to use LLMs for proof search, very similar to how would I use a SMT solver. But what I have found is that the language models have to be really coerced into using these libraries, because otherwise the models much rather overfit and overclaim a solution with a 3 minute inference task rather than attempt to fulfill the proof obligations over 3 hours. And I feel nauseated when I need to convince the LLM (I use Claude) that filling the proof obligation is for "academic exercise" or because I'm coerced into doing so, because otherwise it will come up with reasons of its own why it does not want to do it. Now, this happens under the mental model in which I'm interested in finding equivalences with prior work. Many LLM generated Lean code reads more as if someone was interested whether X can be turned into a Lean 4 program, which is mostly yes, and that in general is a positive thing. But, if you are not interested in refinement types and theorems, why not just choose Haskell? The point is, I strongly sense that unless you have good questions to ask, then that's very evident in these languages. And, this is something the LLM won't help you -- if you don't impose a proof obligation for it, it certainly will not try to go the extra mile to conjure one for you. > — [Jhsto on hackernews · 1 comments](https://news.ycombinator.com/item?id=49063008) > Self-insert time. I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes. The cost of finding and developing exploits also was high. That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost. We've seen how Mythos has found more vulnerabilities than the rest of the security industry combined. (you can argue about the quality and what counts as a vulnerability, but not the point) So the cost of finding and developing exploits has dropped dramatically. On the other hand, formal verification is now much easier, since LLMs can automate the proof. You don't even need to worry about hallucinations, you merely need to trust Lean core. If the LLM is wrong, the proof will get rejected! The problem of exploits gets bigger, and the solution of formal verification gets cheaper. As a result, the needle is now moving in the direction of "more formal verification". I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time. My (ambitious) goal is to have a self-hosting, formally verified compiler, which allows proof transfer from source code down to assembly. I have not achieved that goal yet. What I have so far: - one (non-optimized) compiler step which is formally verified - three simple functions (hex, hex with labels, strtoull) formally verified, against RISC-V assembly, and against a custom IR https://github.com/m1el/riscv-fv-bootstrap The project is in quite a bad shape, and I am trying to improve my skills in that direction. > — [m1el on hackernews · 1 comments](https://news.ycombinator.com/item?id=49065254) **Source threads** - [hackernews](https://news.ycombinator.com/item?id=49062291) · 64 points · 50 comments ## Similar posts on daily.dev - [Creator of Lean: Handwritten Math Will Change Dramatically](https://daily.dev/posts/creator-of-lean-handwritten-math-will-change-dramatically-ssexcp90l) · The Developing Dev · 0 upvotes · 0 comments - [Introduction to Lean for Programmers](https://daily.dev/posts/introduction-to-lean-for-programmers-zyd84tuax) · Towards Data Science · 0 upvotes · 0 comments - [From Zero to QED](https://daily.dev/posts/from-zero-to-qed-h3omgvjou) · Hacker News · 2 upvotes · 0 comments --- Tags: [#llm](https://daily.dev/tags/llm) [View this post on daily.dev](https://daily.dev/posts/we-have-proof-automation-now-pwem29i8q) ```json {"@context":"https://schema.org","@graph":[{"@type":"Organization","@id":"https://daily.dev/#organization","name":"daily.dev","url":"https://daily.dev","logo":{"@type":"ImageObject","url":"https://daily.dev/apple-touch-icon.png","width":180,"height":180},"sameAs":["https://twitter.com/dailydotdev","https://github.com/dailydotdev","https://www.linkedin.com/company/daily-dev-ltd"]},{"@type":"WebSite","@id":"https://daily.dev/#website","url":"https://daily.dev","name":"daily.dev","publisher":{"@id":"https://daily.dev/#organization"},"potentialAction":{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https://daily.dev/search?q={search_term_string}"},"query-input":"required name=search_term_string"}}]} {"@context":"https://schema.org","@type":"TechArticle","headline":"We have proof automation now","url":"https://daily.dev/posts/we-have-proof-automation-now-pwem29i8q","mainEntityOfPage":{"@type":"WebPage","@id":"https://daily.dev/posts/we-have-proof-automation-now-pwem29i8q"},"datePublished":"2026-07-27T01:25:40.320Z","dateModified":"2026-08-03T10:46:37.029Z","description":"Adam Langley explores using LLMs to automate proof generation in Lean, a dependently-typed programming language, by building a Zstandard decompressor. The post...","image":"https://media.daily.dev/image/upload/s--CxzD6vbw--/f_auto/v1722860399/public/Placeholder%2005","thumbnailUrl":"https://media.daily.dev/image/upload/s--CxzD6vbw--/f_auto/v1722860399/public/Placeholder%2005","isAccessibleForFree":true,"articleSection":"Hacker News","inLanguage":"en","publisher":{"@type":"Organization","name":"daily.dev","url":"https://daily.dev","logo":{"@type":"ImageObject","url":"https://daily.dev/apple-touch-icon.png","width":180,"height":180}},"author":{"@type":"Organization","name":"Hacker News","logo":"https://media.daily.dev/image/upload/t_logo,f_auto/v1/logos/hn","url":"https://daily.dev/sources/hn"},"commentCount":0,"discussionUrl":"https://daily.dev/posts/we-have-proof-automation-now-pwem29i8q","interactionStatistic":[{"@type":"InteractionCounter","interactionType":{"@type":"LikeAction"},"userInteractionCount":0},{"@type":"InteractionCounter","interactionType":{"@type":"CommentAction"},"userInteractionCount":0}],"keywords":"llm","timeRequired":"PT18M"} {"@context":"https://schema.org","@type":"BreadcrumbList","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https://daily.dev"},{"@type":"ListItem","position":2,"name":"Hacker News","item":"https://daily.dev/sources/hn"},{"@type":"ListItem","position":3,"name":"We have proof automation now"}]} ```