Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

sdiehl.github.io

Post reply on HN
Print view View original

11–20 of 23 posts

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

#11

Post by mutkach »

practal wrote: post #10
mutkach wrote: post #9

Earlier quoted context omitted.

Understanding IMO is "developing a correct mental model of a concept". Some heuristics of correctness: Feynman: "What I cannot build. I do not understand" Einstein: "If you can't explain it to a six year old, you don't understand it yourself" 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 certifica…

Ideas and correctness depend on each other. You usually start with an idea, and check if it is correct. If not, you adjust the idea until it becomes correct. Once you have a correct idea, you can go looking for more ideas based on this. 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. Forma…

I share your fascination with proof assistants and formal verification, but the reality is that I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas, or enthusiastic about putting in the actual (additional) work to build the formalization prerequisites to even begin defining the theorem's statement in that (formal) language.

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

#12

Post by hollerith »

mutkach wrote: post #11
practal wrote: post #10

Earlier quoted context omitted.

Ideas and correctness depend on each other. You usually start with an idea, and check if it is correct. If not, you adjust the idea until it becomes correct. Once you have a correct idea, you can go looking for more ideas based on this. 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. Forma…

I share your fascination with proof assistants and formal verification, but the reality is that I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas, or enthusiastic about putting in the actual (additional) work to build the formalization prerequisites to even begin defining the theorem's statement in that (formal) language.

>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

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

#13

Post by mutkach »

hollerith wrote: post #12
mutkach wrote: post #11

Earlier quoted context omitted.

I share your fascination with proof assistants and formal verification, but the reality is that I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas, or enthusiastic about putting in the actual (additional) work to build the formalization prerequisites to even begin defining the theorem's statement in that (formal) language.

>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 space, and this is what we have done, using the Lean theorem prover.

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

#14

Post by practal »

mutkach wrote: post #11
practal wrote: post #10

Earlier quoted context omitted.

Ideas and correctness depend on each other. You usually start with an idea, and check if it is correct. If not, you adjust the idea until it becomes correct. Once you have a correct idea, you can go looking for more ideas based on this. 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. Forma…

I share your fascination with proof assistants and formal verification, but the reality is that I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas, or enthusiastic about putting in the actual (additional) work to build the formalization prerequisites to even begin defining the theorem's statement in that (formal) language.

You know what? I agree with you. I have not formalised any of my stuff on abstraction logic [1] for that reason (although that would not be too difficult in Isabelle or Lean), I want to write it down in Practal [2], this becoming possible I see as the first serious milestone for Practal. Eventually, I want Practal to feel more natural than paper, and definitely more natural than LaTeX. That's the goal, and I feel many people now see that this will be possible with AI within the next decade.

[1] http://abstractionlogic.com

[2] https://practal.com

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

#16

Post by tuhgdetzhh »

zozbot234 wrote: post #8
randomtoast wrote: post #3

I have been following recent progress in the formalization of mathematical proofs in Lean, particularly in the context of large language models. One prominent advocate of this approach is Terence Tao, who regularly writes about developments in this area. 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 revi…

You don't have to trust the full Lean toolchain, only the trusted proof kernel (which is small enough to be understood by a human) and any desugarings involved in converting the theorem statement from high-level Lean to whatever the proof kernel accepts (these should also be simple enough). The proof itself can be checked automatically.

Lets assume the kenerl is correct and a mathematian trusts it, now what happens if it is the proof itself that he cannot understand anymore because it has gotten too sophisticated? I think that this would indeed be a difference, and a crossing point in history of mathematical proofs.

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

#17

Post by esafak »

randomtoast wrote: post #3

I have been following recent progress in the formalization of mathematical proofs in Lean, particularly in the context of large language models. One prominent advocate of this approach is Terence Tao, who regularly writes about developments in this area. 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 revi…

I am not a mathematician either, but having read Tao's essay on intuition (https://terrytao.wordpress.com/career-advice/theres-more-to-...) I can easily see how he would profitably point an LLM in the right direction and suggest approaches that would conclude in a successful proof upon connecting the dots.

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

#18

Post by zozbot234 »

tuhgdetzhh wrote: post #16
zozbot234 wrote: post #8

Earlier quoted context omitted.

You don't have to trust the full Lean toolchain, only the trusted proof kernel (which is small enough to be understood by a human) and any desugarings involved in converting the theorem statement from high-level Lean to whatever the proof kernel accepts (these should also be simple enough). The proof itself can be checked automatically.

Lets assume the kenerl is correct and a mathematian trusts it, now what happens if it is the proof itself that he cannot understand anymore because it has gotten too sophisticated? I think that this would indeed be a difference, and a crossing point in history of mathematical proofs.

In principle, it's no different than failing to understand the details of any calculation. If the calculating process is executed correctly, you can still trust the outcome.

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

#19

Post by lgas »

practal wrote: post #6
lgas wrote: post #5

Earlier quoted context omitted.

I'm not sure I understand what you're getting at -- your last paragraph suggestions that you understand the point of formal specification languages and theorem provers (ie. for the automated prover to verify the proof such that you just have to trust the toolchain) but in your next to last paragraph you speak as if you think that human mathematicians need to verify the lean 4 code of the proof? It doesn't matter how…

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

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

#20

Post by aejm »

mutkach wrote: post #7
randomtoast wrote: post #3

I have been following recent progress in the formalization of mathematical proofs in Lean, particularly in the context of large language models. One prominent advocate of this approach is Terence Tao, who regularly writes about developments in this area. 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 revi…

> 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.
Post reply on HN