Lean is super cool. If you're curious how proof checking works (on the type system level), I wrote an article about that: https://overreacted.io/beyond-booleans/
I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you run it interactively and observe the goals at each step. In contrast languages like Idris do not use tactics and require explicit manipulation of proof objects; it’s a lot less automated and verbose. Using the function call analogy, it’s like having to write down every argument passed to a function call and name every return value. It’s more tedious to write but both the writer and the reader gain more by the explicitness. But in the age of AI, the tedium to write proofs without tactics really shouldn’t have mattered.
I'll note that not all segments of a proof are equally interesting. Many steps, perhaps even most when it comes to proofs about programs, are "obvious". I find that tactic-based proofs tend to be more legible than providing very explicit proof objects directly, because it allows the obvious but tedious details to be elided. What you are left with are just the most important high-level steps that the automation couldn't infer (or which we just don't wish to delegate). Things like "induct according to this scheme after generalizing this variable" or "first prove this auxiliary lemma" or "apply this inverse function to both sides so that they cancel".
I'd also argue that automation is essential to practical proof engineering. It make the proofs less brittle to minor changes and therefore more maintainable.
Edit: a couple more thoughts. First, there is nothing stopping you from defining proof objects directly in Lean without tactics. That flexibility is quite nice -- you can automate as much or as little as you like. Of course, in practice, people almost always use tactics. Second, I use the ACL2 prover quite a bit, which is not tactic-based. Instead, you give high-level "hints" that steer the aggressively-automated prover. Funny enough, I have colleagues that look at Lean proofs and say "these proofs are so verbose, how does anyone understand them!".
Very well put. I'll just add that there is one more thing one can do to document the important/insightful/interesting parts of a proof, where it makes sense: Write a comment.
> I think the explosion in the popularity of Lean probably means that tactic-based proofs have won
The number of mentions of Lean in HN submissions aside, how do we gauge that? HN has odd trends like that - a decade ago, we loved everything "Bayesian" - but they don't necessarily translate to anything that's happening in the mainstream.
Lean's mostly used for maths, and tactics are much more ergonomic there. For writing correct-by-construction software programs, complex dependently-typed objects can be more ergonomic, as they allow passing a bunch of invariants through a program that are correct by construction, rather than needing to prove them at every stage via tactics.
Great tutorial, really enjoyed it! Personally, I think languages that can check very much at compile time in combinations with LLMs have a bright future ahead. Additionally, if one wanted to give Haskell a try, Lean4 might be a good language to check out before, as it is more modern and ticks many of the same boxes (Still has some unique features, and the communities quite a lot).
Small feedback:
- Great flow, explaination, motivation and so on! :)
- Typo: "conext" at the bottom
- If you want to keyword-hack a bit, you could introduce a paragraph or too about the role the relationship of Lean4 with LLMs/AI ;)
Vitalik recently wrote about vibe-coding in Lean and assembly language, using proof verification in Lean, saying "if done right, this has potential to both output extremely efficient code, and be far more secure than the way programming has been done before."
Yeah, his post resulted in a rise in everyone and their mother becoming formal verification "experts" now. But I think he's right. We no longer have good excuses for not trying to secure code with FV in this brave new world of agentic coding
If you're excited about the relationship of Lean4 to LLMs/AI (like I am), you might find my recent post interesting [1].
TL;DR: I'm using automated theorem provers within my research on AI for automated algorithm design. To make it easier to run/benchmark different models/harnesses, I created an open-source Python package called OpenATP [2]. I recently added support to use Grok 4.5 in the OpenCode harness as a prover and found it to be surprisingly competitive with Claude Code and Codex at a fraction the cost and wall-clock time.
This is super cool! I see you are using Aristotle as the automated theorem prover. I know Aristotle is free (for now at least), and it's hard to beat free... But, you still might be interested in a recent post of mine [1]! I'm working on an open-source Python package called OpenATP [2] to make it easy to run/benchmark different models and harnesses as automated theorem provers. I recently added support for Grok 4.5 and found it to be surprisingly good.
An assert statement requires that you specifically come up with a test case. Lean lets you verify for all possible cases. Infinity is not a problem.
It's similar to a type system in that regard. The same difference could be applied there (comparing a Python type assert). Types, however, generally only cover checks similar to "the shape of the data is X".
Lean is different in that its language for expressing properties is wide enough to express anything you can imagine. The bottleneck becomes accurately stating properties you'd like to enforce and, subsequently, discovering proofs of whether or not they're true.
I’m an noob to Lean myself, but my best explanation is that asserts are checks that happen at runtime. Imagine compile-time asserts, where the compiler is able to determine the validity of assertions without needing to run the program. Formal verification techniques make this possible. In Lean, it is possible to write a proof that, if true, guarantees that the code works.
It works on the type system level instead of at runtime. So you don't actually need to "run" any code to verify it, and you can verify it for all possible inputs, even infinity of them, rather than for the ones that exist in your test.
Assertions are for testing at runtime. They demonstrate that the behavior is correct on one input when it runs. Formal verification proves that the code is correct on _all_ inputs _before_ it runs.
Formal verification proves if your specified theorem is correct. You can state any number of properties, in one extreme you just have basic types.
The interesting, 'hard-to-wrap one's head around' thing is that this verification is done by basically comparing arbitrary computations for equality.
So to prove that `3+3 == 6`, you would create an object with the type being `3+3 == 6`. And the rules of these languages are such, that the only way you can ever create an instance and thus a valid object for this type is if it's a true statement. 3+3==7 has no instance and can never have. (Interestingly, the instance of the above type is called `refl` for reflexivity. This is the only instance possible, and its type is basically a generic expecting a type, and a value of that type (this is where dependent types come in). Its "constructor" will place a single value into both slots, so the only way it can ever be instantiated is via values that the language/compiler itself considers equal.
A proof is just a manipulation of each "side" until they are trivially equal to each other).
One important caveat of the above: these languages evaluate expression not like most ordinary languages, like stopping at a thunk when the outermost value can't be further simplified. They will continue inward simplifying everything, and comparing these together - so even functions can be compared (though implementation matters a lot, and will alter the shape of proofs!)
Assuming you are serious; there is a lot to know conceptually before one can answer the above comprehensively.
Start with Set Theory, Propositional/Predicate Calculus, Hoare Triples, Dijkstra's wp-calculus and Predicate Transformers, then move on to Lambda Calculus, Type Systems (inductive/dependent/function etc.), Curry-Howard Correspondence, Invariants/Verification Conditions/Theorems etc. all leading up to "How the hell do they all come together in a Theorem Prover?"
it is very much a related idea. an `assert` statement in e.g. `python` is a statement your code is making about what it means to be correct, and furthermore a statement about what conditions would have to exist to validate the first statement: for example you might need to run it with certain inputs, on a certain file or kind of file.
`lean4` is very much about the same two ideas. you can make statements about what it means for the code to say something interesting, usually something relevant to whether or not it's correct, and you make statements about the circumstances in which you would evaluate that.
people are interested in `lean4` because it allows you to make more interesting statements of both kinds, and you have tools to be much more specific about the details, the `assert` statements in `python` can't really call each other for example, they don't really compose. in `lean4` the ability to compose such statements is very important.
…and for no discernible reason, too. Ordinarily, irritating stuttering pages like this at least do some sort of visually fun thing. This is just a diabolical Framer design with a ton of needlessly overlapping nested containers. I deleted more than 20 invisible divs from the DOM and scrolling improved dramatically.
I'd inform the webmaster but the telephone number listed on the site is "(123) 456 789", so I guess AI slop is AI slop.
I've often wondered how viable it is to use AI to fill out the ecosystem gaps in awesome but niche languages (still looking at you OCaml...).
I've not gone too deep down this train of thought because a standard library/ecosystem should be solid and I don't think LLMs are quite there... but if we can use LLMs+Lean maybe we can get the quality we need to bootstrap more of the Lean ecosystem?
These are both "tactics". The article defines tactics as "instructions that help reduce the current goal". Writing a proof consists of starting with the thing to be proved and then writing a sequence of tactics to break the problem up into progressively easier and easier problems, until everything is broken down into things that are trivially true.
"rfl" stands for "reflexivity", the mathy term for "everything is equal to itself". As the article says, "[rfl] deems two things equal if they are equal by computation". That is to say, if the current subproblem is of the form "prove x = y" where both x and y are some sort of expressions that clearly evaluate to the same value, then applying rfl will finish the proof and mark this problem as solved.
"decide" is another tactic. Not sure where you got it from, I don't see it mentioned in this article. But basically it's a more powerful "I don't want to write out all the steps of this, please try to prove it for me" command.
In the end I wasn't able to read it on my ebook reader and reading it on a PC or smartphone kinda makes it annoying to read on the commute. So I've only read the first two chapters or so but it seemed like a lot of fun. All this talk about using Lean in AI-powered proofs kinda makes me want to pick it up again.
how is lean different from tlaplus for helping you with reasoning during the design phase?
I literally just discovered tlaplus last week after struggling with reasoning about the explosion of permutations about configuration policies Im designing, and Im still learning the math but Im finding it easier to reason with tlaplus than in code is lean like that?
You can embed TLA+ into Lean. I don't think that there's any benefit to formalization before coding unless you're working on like million dollar projects
Just in case anyone else decides to write along like the article suggests. I chose to use the live.lean-lang.org link, but it seems to default to a newer version of lean where the simp[xor] actually returns both sides still wrapped in the lambdas so the next simp[add_comm] will actually fail. The way to get around it is changing the version to v4.32.0 which the article doesn't seem to mention.
Compile time evaluation is used in Lean all the time for metaprogramming (e.g. proof automation). Any `IO` can be run there (which allows running external solvers, reading a dataset from disk etc).
Perhaps access to IO in metaprograms could be restricted, but it would require substantial changes to the language and it is probably not a priority of the developers right now.
Lean is super cool. If you're curious how proof checking works (on the type system level), I wrote an article about that: https://overreacted.io/beyond-booleans/
Here's another article I wrote that gives some intuition about the role of axioms in Lean: https://overreacted.io/the-math-is-haunted/
And here's a longer primer on Lean's syntax: https://overreacted.io/a-lean-syntax-primer/
Finally, if this got this even a little bit curious, I strongly encourage you to play the Natural Number Game: https://adam.math.hhu.de/#/g/leanprover-community/nng4
This is the best intro to Lean I know, plus it teaches you why a + b = b + a.
I love your posts! The Social Filesystem is amazing!
https://overreacted.io/a-social-filesystem/
I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you run it interactively and observe the goals at each step. In contrast languages like Idris do not use tactics and require explicit manipulation of proof objects; it’s a lot less automated and verbose. Using the function call analogy, it’s like having to write down every argument passed to a function call and name every return value. It’s more tedious to write but both the writer and the reader gain more by the explicitness. But in the age of AI, the tedium to write proofs without tactics really shouldn’t have mattered.
I'll note that not all segments of a proof are equally interesting. Many steps, perhaps even most when it comes to proofs about programs, are "obvious". I find that tactic-based proofs tend to be more legible than providing very explicit proof objects directly, because it allows the obvious but tedious details to be elided. What you are left with are just the most important high-level steps that the automation couldn't infer (or which we just don't wish to delegate). Things like "induct according to this scheme after generalizing this variable" or "first prove this auxiliary lemma" or "apply this inverse function to both sides so that they cancel".
I'd also argue that automation is essential to practical proof engineering. It make the proofs less brittle to minor changes and therefore more maintainable.
Edit: a couple more thoughts. First, there is nothing stopping you from defining proof objects directly in Lean without tactics. That flexibility is quite nice -- you can automate as much or as little as you like. Of course, in practice, people almost always use tactics. Second, I use the ACL2 prover quite a bit, which is not tactic-based. Instead, you give high-level "hints" that steer the aggressively-automated prover. Funny enough, I have colleagues that look at Lean proofs and say "these proofs are so verbose, how does anyone understand them!".
Very well put. I'll just add that there is one more thing one can do to document the important/insightful/interesting parts of a proof, where it makes sense: Write a comment.
I don't really buy this argument because we can all read the code with the Lean LSP.
Also, after using a tactic enough you can guess why it's used.
Agda and Idris are more beautiful for sure, but a proof is a proof (according to the law of the excluded middle)
> I think the explosion in the popularity of Lean probably means that tactic-based proofs have won
The number of mentions of Lean in HN submissions aside, how do we gauge that? HN has odd trends like that - a decade ago, we loved everything "Bayesian" - but they don't necessarily translate to anything that's happening in the mainstream.
The @[grind] tactic has to be the single most important addition to Lean in terms of it's growing popularity
Lean's mostly used for maths, and tactics are much more ergonomic there. For writing correct-by-construction software programs, complex dependently-typed objects can be more ergonomic, as they allow passing a bunch of invariants through a program that are correct by construction, rather than needing to prove them at every stage via tactics.
If you like Lean, here are two more great, short books on proving things about your program (not with Lean, though):
1. https://mitpress.mit.edu/9780262527958/the-little-prover/
2. https://mitpress.mit.edu/9780262536431/the-little-typer/
David Thrane Christiansen, co-author of the second, also wrote Functional Programming in Lean (Lean 4) among many other tutorials and things.
The Natural Numbers Game is amazing, highly recommended.
> In this game you recreate the natural numbers N from the Peano axioms, learning the basics about theorem proving in Lean.
https://adam.math.hhu.de/
Great tutorial, really enjoyed it! Personally, I think languages that can check very much at compile time in combinations with LLMs have a bright future ahead. Additionally, if one wanted to give Haskell a try, Lean4 might be a good language to check out before, as it is more modern and ticks many of the same boxes (Still has some unique features, and the communities quite a lot).
Small feedback: - Great flow, explaination, motivation and so on! :) - Typo: "conext" at the bottom - If you want to keyword-hack a bit, you could introduce a paragraph or too about the role the relationship of Lean4 with LLMs/AI ;)
Vitalik recently wrote about vibe-coding in Lean and assembly language, using proof verification in Lean, saying "if done right, this has potential to both output extremely efficient code, and be far more secure than the way programming has been done before."
https://vitalik.eth.limo/general/2026/05/18/fv.html
Yeah, his post resulted in a rise in everyone and their mother becoming formal verification "experts" now. But I think he's right. We no longer have good excuses for not trying to secure code with FV in this brave new world of agentic coding
If you're excited about the relationship of Lean4 to LLMs/AI (like I am), you might find my recent post interesting [1].
TL;DR: I'm using automated theorem provers within my research on AI for automated algorithm design. To make it easier to run/benchmark different models/harnesses, I created an open-source Python package called OpenATP [2]. I recently added support to use Grok 4.5 in the OpenCode harness as a prover and found it to be surprisingly competitive with Claude Code and Codex at a fraction the cost and wall-clock time.
[1] https://news.ycombinator.com/item?id=49010310
[2] https://github.com/henryrobbins/open-atp
I built an automated math research system using Lean to verify the results: https://alethean.org
This is super cool! I see you are using Aristotle as the automated theorem prover. I know Aristotle is free (for now at least), and it's hard to beat free... But, you still might be interested in a recent post of mine [1]! I'm working on an open-source Python package called OpenATP [2] to make it easy to run/benchmark different models and harnesses as automated theorem provers. I recently added support for Grok 4.5 and found it to be surprisingly good.
[1] https://news.ycombinator.com/item?id=49010310
[2] https://github.com/henryrobbins/open-atp
That is a cool visualization.
(Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?
An assert statement requires that you specifically come up with a test case. Lean lets you verify for all possible cases. Infinity is not a problem.
It's similar to a type system in that regard. The same difference could be applied there (comparing a Python type assert). Types, however, generally only cover checks similar to "the shape of the data is X".
Lean is different in that its language for expressing properties is wide enough to express anything you can imagine. The bottleneck becomes accurately stating properties you'd like to enforce and, subsequently, discovering proofs of whether or not they're true.
I’m an noob to Lean myself, but my best explanation is that asserts are checks that happen at runtime. Imagine compile-time asserts, where the compiler is able to determine the validity of assertions without needing to run the program. Formal verification techniques make this possible. In Lean, it is possible to write a proof that, if true, guarantees that the code works.
It works on the type system level instead of at runtime. So you don't actually need to "run" any code to verify it, and you can verify it for all possible inputs, even infinity of them, rather than for the ones that exist in your test.
Assertions are for testing at runtime. They demonstrate that the behavior is correct on one input when it runs. Formal verification proves that the code is correct on _all_ inputs _before_ it runs.
Formal verification proves if your specified theorem is correct. You can state any number of properties, in one extreme you just have basic types.
The interesting, 'hard-to-wrap one's head around' thing is that this verification is done by basically comparing arbitrary computations for equality.
So to prove that `3+3 == 6`, you would create an object with the type being `3+3 == 6`. And the rules of these languages are such, that the only way you can ever create an instance and thus a valid object for this type is if it's a true statement. 3+3==7 has no instance and can never have. (Interestingly, the instance of the above type is called `refl` for reflexivity. This is the only instance possible, and its type is basically a generic expecting a type, and a value of that type (this is where dependent types come in). Its "constructor" will place a single value into both slots, so the only way it can ever be instantiated is via values that the language/compiler itself considers equal.
A proof is just a manipulation of each "side" until they are trivially equal to each other).
One important caveat of the above: these languages evaluate expression not like most ordinary languages, like stopping at a thunk when the outermost value can't be further simplified. They will continue inward simplifying everything, and comparing these together - so even functions can be compared (though implementation matters a lot, and will alter the shape of proofs!)
Assuming you are serious; there is a lot to know conceptually before one can answer the above comprehensively.
Start with Set Theory, Propositional/Predicate Calculus, Hoare Triples, Dijkstra's wp-calculus and Predicate Transformers, then move on to Lambda Calculus, Type Systems (inductive/dependent/function etc.), Curry-Howard Correspondence, Invariants/Verification Conditions/Theorems etc. all leading up to "How the hell do they all come together in a Theorem Prover?"
Some simple tutorials;
Introduction to Lean for Programmers: The syntax and semantics of mathematics - https://towardsdatascience.com/introduction-to-lean-for-prog...
The hitchhiker's guide to reading Lean 4 theorems - https://blog.lambdaclass.com/the-hitchhikers-guide-to-readin...
it's like proof by induction versus trying every number from 0 to infinity
it is very much a related idea. an `assert` statement in e.g. `python` is a statement your code is making about what it means to be correct, and furthermore a statement about what conditions would have to exist to validate the first statement: for example you might need to run it with certain inputs, on a certain file or kind of file.
`lean4` is very much about the same two ideas. you can make statements about what it means for the code to say something interesting, usually something relevant to whether or not it's correct, and you make statements about the circumstances in which you would evaluate that.
people are interested in `lean4` because it allows you to make more interesting statements of both kinds, and you have tools to be much more specific about the details, the `assert` statements in `python` can't really call each other for example, they don't really compose. in `lean4` the ability to compose such statements is very important.
but you can write regular programs in it too. this is a reverse proxy faster than `nginx`: https://cdn.s4.gl/serve-fd.lean
Please please please don't hijack scrolling :(
…and for no discernible reason, too. Ordinarily, irritating stuttering pages like this at least do some sort of visually fun thing. This is just a diabolical Framer design with a ton of needlessly overlapping nested containers. I deleted more than 20 invisible divs from the DOM and scrolling improved dramatically.
I'd inform the webmaster but the telephone number listed on the site is "(123) 456 789", so I guess AI slop is AI slop.
I'm the webmaster. Another commenter let me know about the scrolling. I'll get onto it. Thank you for the feedback
a) Thanks for putting this together!
b) Please don't hijack my scrolling.
c) I really wish Lean were more mature as an application programming language. Its standard library is really lacking.
I've often wondered how viable it is to use AI to fill out the ecosystem gaps in awesome but niche languages (still looking at you OCaml...).
I've not gone too deep down this train of thought because a standard library/ecosystem should be solid and I don't think LLMs are quite there... but if we can use LLMs+Lean maybe we can get the quality we need to bootstrap more of the Lean ecosystem?
I'll need to fix b! That is not intentional whatsover. Sorry for that. Thank you for the feedback
They’re working on adding a whole HTTP API right now
This is cool and im not familiar with what lean actually does beyond the words "formal methods"
immediate questions from reading:
* what is rfl?
* what is decide?
i spent a lot of time looking for where these keywords(? declarations?) were made and i still dont know what they end up meaning
These are both "tactics". The article defines tactics as "instructions that help reduce the current goal". Writing a proof consists of starting with the thing to be proved and then writing a sequence of tactics to break the problem up into progressively easier and easier problems, until everything is broken down into things that are trivially true.
"rfl" stands for "reflexivity", the mathy term for "everything is equal to itself". As the article says, "[rfl] deems two things equal if they are equal by computation". That is to say, if the current subproblem is of the form "prove x = y" where both x and y are some sort of expressions that clearly evaluate to the same value, then applying rfl will finish the proof and mark this problem as solved.
"decide" is another tactic. Not sure where you got it from, I don't see it mentioned in this article. But basically it's a more powerful "I don't want to write out all the steps of this, please try to prove it for me" command.
https://www.amazon.com/Maths-Proofs-Lean-First-Steps-ebook/d... I like this author and a while ago found that he'd published a book on Lean!
In the end I wasn't able to read it on my ebook reader and reading it on a PC or smartphone kinda makes it annoying to read on the commute. So I've only read the first two chapters or so but it seemed like a lot of fun. All this talk about using Lean in AI-powered proofs kinda makes me want to pick it up again.
how is lean different from tlaplus for helping you with reasoning during the design phase?
I literally just discovered tlaplus last week after struggling with reasoning about the explosion of permutations about configuration policies Im designing, and Im still learning the math but Im finding it easier to reason with tlaplus than in code is lean like that?
You can embed TLA+ into Lean. I don't think that there's any benefit to formalization before coding unless you're working on like million dollar projects
I just wish Lean4 is easier to use. Tried Mathematics in Lean and couldn’t even get the dependencies right
Does anyone do TLA style distributed systems verification with Lean? Curious the experience there and how well supported it is
Just in case anyone else decides to write along like the article suggests. I chose to use the live.lean-lang.org link, but it seems to default to a newer version of lean where the simp[xor] actually returns both sides still wrapped in the lambdas so the next simp[add_comm] will actually fail. The way to get around it is changing the version to v4.32.0 which the article doesn't seem to mention.
Why does Lean always have a way to mess up your file system, writing to any files, rather than just proving proofs?
I found that out when reading the recent articls about counterexamples.
Compile time evaluation is used in Lean all the time for metaprogramming (e.g. proof automation). Any `IO` can be run there (which allows running external solvers, reading a dataset from disk etc).
Perhaps access to IO in metaprograms could be restricted, but it would require substantial changes to the language and it is probably not a priority of the developers right now.