From Zero to QED: An informal introduction to formality with Lean 4 • Hacker News Board

Re: From Zero to QED: An informal introduction to formality with Lean 4

#21

Post by practal » Fri, Dec 19, 2025, 10:19 PM UTC

lgas wrote: post #19

practal wrote: post #6

Earlier quoted context omitted.

> Well, assuming it's free of escape hatches like `sorry` 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 origina…

> 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 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.

In principle, this is how these systems work. In practice, there are usually plenty of things that make it difficult to say for sure if you have a proof of something.

Re: From Zero to QED: An informal introduction to formality with Lean 4

#22

Post by peterkagey » Fri, Dec 19, 2025, 11:32 PM UTC

aejm wrote: post #20

mutkach wrote: post #7

Earlier quoted context omitted.

> more than 1,000,000 lines of Lean 4 code and concluding with a QED. 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 ki…

No, the point of proofs in mathematics IS to prove a particular statement is true, given certain axioms (accepted truths). Yes, there are numerous benefits beyond demonstrating something is undeniably true, given certain accepted truths, perhaps more “useful” than the proof itself, but math is a method of formal knowledge that doesn’t accept shortcuts.

A lot of mathematicians (myself included) would say that the point of proofs isn’t entirely to know whether or not a statement is true, but that it exists to promote human understanding. In fact, I’d argue that at some level, knowing whether or not a theorem is true can be less important than understanding an argument.

This is why having multiple different proofs is valuable to the math community—because different proofs offer different perspectives and ways of understanding.

Re: From Zero to QED: An informal introduction to formality with Lean 4

#23

Post by hollerith » Sun, Dec 21, 2025, 1:50 PM UTC

mutkach wrote: post #13

hollerith wrote: post #12

Earlier quoted context omitted.

>I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas British mathematician Kevin Buzzard has been evangelizing proof assistants since 2017. I'll leave it to you to decide whether he is working on frontier research: https://profiles.imperial.ac.uk/k.buzzard/publications

Sure, he is one of biggest advocates for it, and yet he was quite clear that it is not yet possible for him to do his actual research in Lean. Quoting one of the recent papers (2020): > With current technology, it would take many person-decades to formalise Scholze’s results. Indeed, even stating Scholze’s theorems would be an achievement. Before that, one has of course to formalise the definition of a perfectoid spa…

Thanks for that.