From Zero to Qed: an Informal Introduction to Formality with Lean 4
Key topics
Diving into the world of formalizing mathematical proofs, a new tutorial on Lean 4 has sparked a lively discussion on the intersection of math, programming, and artificial intelligence. Commenters are buzzing about the potential of Lean 4, with some highlighting the importance of trusted proof kernels and others pondering the role of formal specification languages in verifying mathematical truths. As one commenter astutely pointed out, the real value of a proof lies not just in verifying a statement, but in understanding the underlying concepts - echoing the wisdom of Feynman and Einstein. The discussion reveals a consensus on the significance of building a correct mental model, with Lean 4 emerging as a promising tool in this pursuit.
Snapshot generated from the HN discussion
Discussion Activity
Active discussionFirst comment
5d
Peak period
16
132-144h
Avg / period
7
Based on 21 loaded comments
Key moments
- 01Story posted
Dec 13, 2025 at 6:42 PM EST
20 days ago
Step 01 - 02First comment
Dec 19, 2025 at 4:23 AM EST
5d after posting
Step 02 - 03Peak activity
16 comments in 132-144h
Hottest window of the conversation
Step 03 - 04Latest activity
Dec 21, 2025 at 8:50 AM EST
12 days ago
Step 04
Generating AI Summary...
Analyzing up to 500 comments to identify key contributors and discussion patterns
Want the full context?
Jump to the original sources
Read the primary article or dive into the live Hacker News thread when you're ready.
From a programmer's perspective, this puts up an interesting parallel. Models such as Sonnet or Opus 4.5 can generate thousands of lines of code per hour. I can review the output, ask the model to write tests, iterate on the result, and after several cycles become confident that the software is sufficiently correct.
For centuries, mathematicians developed proofs by hand, using pen and paper, and were able to check the proofs of their peers. In the context of LLMs, however, a new problem may arise. Consider an LLM that constructs a proof in Lean 4 iteratively over several weeks, resulting in more than 1,000,000 lines of Lean 4 code and concluding with a QED. At what point is an ordinary mathematician no longer able to confirm with confidence that the proof is correct?
Such a mathematician might rely on another LLM to review the proof, and that system might also report that it is correct. We may reach a stage where humans can no longer feasibly verify every proof produced by LLMs due to their length and complexity. Instead, we rely on the Lean compiler and LLMs, which confirm formal correctness, and we are effectively required to trust the toolchain rather than our own direct understanding.
There are bugs in theorem provers, which means there might be "sorries", maybe even malicious ones (depending on what is at stake) that are not that easy to detect. Personally, I don't think that is much of a problem, as you should be able to come up with a "superlean" version of your theorem prover where correctness is easier to see, and then let the original prover export a proof that the superlean prover can check.
I think more of a concern is that mathematicians might not "understand" the proof anymore that the machine generated. This concern is not about the fact that the proof might be wrong although checked, but that the proof is correct, but cannot be "understood" by humans. I don't think that is too much of a concern either, as we can surely design the machine in a way that the generated proofs are modular, building up beautiful theories on their own.
A final concern might be that what gets lost is that humans understand what "understanding" means. I think that is the biggest concern, and I see it all the time when formalisation is discussed here on HN. Many here think that understanding is simply being able to follow the rules, and that rules are an arbitrary game, and that is simply not true. Obviously not, because think about it, what does it mean to "correctly follow the rules"?
I think the way to address this final concern is to put beauty at the heart of our theorem provers. We need beautiful proofs, written in a beautiful language, checked and created by a beautiful machine.
Of course none of this changes anything around the machine generated proofs. The point of the proof is to communicate ideas; formalization and verification is simply a certificate showing that those ideas are worth checking out.
Formalisation and (formulating) ideas are not separate things, they are both mathematics. In particular, it is not that one should live in Lean, and the other one in blueprints.
Formalisation and verification are not simply certificates. For example, what language are you using for the formalisation? That influences how you can express your ideas formally. The more beautiful your language, the more the formal counter part can look like the original informal idea. This capability might actually be a way to define what it means for a language to be beautiful, together with simplicity.
[1] http://abstractionlogic.com
[2] https://practal.com
I think this is sort of how lean itself already works. It has a minimal trusted kernel that everything is forced through. Only the kernel has to be verified.
Usually the point of the proof is not to figure out whether a particular statement is true (which may be of little interest by itself, see Collatz conjecture), but to develop some good ideas _while_ proving that statement. So there's not much value in verified 1mil lines of Lean by itself. You'd want to study the (Lean) proof hoping to find some kind of new math invented in it or a particular trick worth noticing.
LLM may first develop a proof in natural language, then prove its correctness while autoformalizing it in Lean. Maybe it will be worth something in that case.
This is why having multiple different proofs is valuable to the math community—because different proofs offer different perspectives and ways of understanding.
https://sdiehl.github.io/zero-to-qed/02_why.html