4 ms·

I helped a very little with the formalization (I filled in some trivial algebraic manipulations, and I was there for some Lean technical support). It's excitin

by kmill 3y ago

I helped a very little with the formalization (I filled in some trivial algebraic manipulations, and I was there for some Lean technical support). It's exciting to see how quickly the work was done, but it's worth keeping in mind that a top mathematician leading a formalization effort is very exciting, so he could very easily scramble a team of around 20 experienced Lean users. There aren't enough experienced Lean users to go around yet for any old project, so Gowers's point about ease of use is an important one. Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib. It's reassuring that mathlib is being developed in such a way that new mathematics can be formalized using it. Like usual though, there was plenty missing. I think this drove a few thousand more lines of general probability theory development.

cs702 3y ago
> I helped a very little... Thank You for helping with the effort, even if it was only "a very little." I love coming across comments like yours on HN.
ska 3y ago
>Something that was necessary for the success of this was years of development that had already been For projects like this it is often very thankless work in the beginning, and can be a real grind. You need at least one person with a vision of how cool it will be in the (poorly defined) future, and a lot of determination.
- pastage 3y ago
  It is great for personal growth. Since I have been part of many such grinds that are now big data sets, I can honestly tell you that it is one of the best things in the world. I know that those thousands of hours of my work has led to 100x savings for other people. I also met people and could work on problems I would never get in professional life.
zozbot234 3y ago
> Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib Yes but the bulk of the work on this project was background as well. So the ease of use problem should be solving itself over time as more and more prereqs get filled in. BTW, I find it interesting that mathlib is apparently also getting refactored to accommodate constructive proofs better, as part of the porting effort to Lean 4. This might encourage more CS- and program-verification minded folks to join the effort, and maybe some folks in math-foundations too (though Lean suffers there by not being able to work with the homotopy-types axioms).
- kmill 3y ago
  Yes, sure, and that's how mathlib usually gets developed, project by project and PRing missing background material. I'm one of the mathlib maintainers, and I wanted to be sure there's acknowledgment here for the years of Boubaki-style work among hundreds of volunteers to build up the mathematics. In a way, now that the paper's been formalized it's time for the really hard work, which is figuring out how to restructure it (and mathlib) so that it can easily support future work. That's writing libraries for you. Where are you getting the idea mathlib is being refactored for constructive proofs? I wouldn't say that's on the road map. In fact, the core Lean developers are uninterested in pursuing supporting this. Since you're here, are you able to say why constructive proofs are interesting to program verification or (T)CS people? I've never heard anyone in TCS even know what constructivity is -- Lean supports their case where you write a program/algorithm and then (with classical logic) prove correctness and other properties. What would constructive logic give them?
  - kmill 3y ago
    I'll mention that the "Lean way" for constructivity is that you write `def`s for constructions. These can depend on classical reasoning for well-typedness if you want (like for being sure a number is in range when indexing an array), but there is a computability checker. In particular, the compiler sees if there is a way to lower the `def` into some simply typed IR, and this IR can be further compiled to C. If you trust the compiler, then you can trust whether it's real construction. (Of course, you can also go and prove a definition evaluates to some value if you don't want to trust the evaluator.)
rowanG077 3y ago
Since you seem to be an expert on this matter I have always wondered whether at some point it becomes faster to prove novel theorems using a theorem prover then doing it on paper. I imagine that quite a bit of time is wasted in proving things that are already proven. In a similar manner that if there would be no libraries, just snippets of code in papers, in computer programming a lot of time would be wasted writing the same things again. I imagine a "proof finding" tool like hoogle is a "function finding" tool could provide a lot of value here. What is your perspective on this?
- zozbot234 3y ago
  The biggest benefit of a formalized theorem library is not so much proving entirely new theorems (though it helps a little bit I suppose) but refactoring the existing developments to make them more elegant, easier to understand, and enhance their generality. In fact, it's already the case that the average formal proof is written to be somewhat higher in abstraction and more straightforward in reasoning than the informal counterpart. This kind of refactoring work is quite hard to do with paper proofs alone, since one cannot essily be sure whether they've preserved correctness wrt. the original development. Having a proof assistant really is a big help there.
  - jenesaispas 3y ago
    > The biggest benefit of a formalized theorem library is not [...] but [...] [citation needed] I think there are many benefits. Hard to claim that your favourite one is the biggest benefit. In general, I think it's a bit weird that you are repeatedly (also other HN threads, and sibling comments in this one) making unfounded claims about Lean/mathlib, to the point where you are telling maintainers how their system works. And if they explain that you are misunderstanding the system, you ignore their correction and bring up the next (or the same) unfounded claim. Disclaimer: I am a Lean/mathlib user.
    - zozbot234 3y ago
      > [citation needed] Whoops, you're right. Here's what Fields medalist Terence Tao has to say about it: https://terrytao.wordpress.com/2023/12/05/a-slightly-longer-lean-4-proof-tour/#comment-682450 https://terrytao.wordpress.com/2023/12/05/a-slightly-longer-... "...sometimes, after a proposition has been proven, someone in the project realizes that in order to apply the proposition neatly in some other part of the project, one has to slightly modify a hypothesis ... Often one can just modify that hypothesis and watch what the compiler does. ... [W]ith well-designed proofs, the process of modifying a proposition is often substantially easier than writing a proof from scratch. (Indeed it is this aspect of formalization where I think we really have a chance in the future of being in a situation where the task is faster to perform in a formal framework than in traditional pen-and-paper (and LaTeX) framework.)" > And if they explain that you are misunderstanding the system I don't think that's a fair description of the sibling threads. If a mathlib maintainer says "no, we're not going to avoid LEM/by-contradiction everywhere in our proof library, that would be silly" because that's what most mathematicians today think constructivism means, as in rejecting the bulk of existing math entirely as meaningless - and then they add "but yes, there are places where we want to work with our own assertions about decidability, and not let classical reasoning mess that up" I think it's entirely fair to call the latter pretty close to a constructivism-friendly approach. (Keep in mind that most practicing mathematicians don't work with foundations, so the fact that misconceptions like the above would be widespread is not surprising. The remaining argument is about the increased complexity of constructive reasoning, and it's entirely fair for a practical development to want to avoid that, and just work with classical statements. After all, most of the mathematical literature is indeed classical; it does not bother with the computational aspect or with the perceived messiness of numerical analysis.)
westurner 3y ago
> so he could very easily scramble a team of around 20 experienced Lean users What have you to say about methods such as these: "LeanDojo: Theorem Proving with Retrieval-Augmented Language Models" (2023) https://arxiv.org/abs/2306.15626 https://arxiv.org/abs/2306.15626 https://leandojo.org/ https://leandojo.org/ https://news.ycombinator.com/from?site=leandojo.org https://news.ycombinator.com/from?site=leandojo.org ( https://westurner.github.io/hnlog/#story-38435908 https://westurner.github.io/hnlog/#story-38435908 Ctrl-F "TheoremQA" (to find the citation and its references in my local personal knowledgebase HTML document with my comments archived in it), manually ) "TheoremQA: A Theorem-driven [STEM] Question Answering dataset" (2023) https://github.com/wenhuchen/TheoremQA#leaderboard https://github.com/wenhuchen/TheoremQA#leaderboard (they check LLM accuracy with Wolfram Mathematica) "Large language models as simulated economic agents (2022) [pdf]" https://news.ycombinator.com/item?id=34385880 https://news.ycombinator.com/item?id=34385880 : > Can any LLM do n-body gravity? What does it say when it doesn't know; doesn't have confidence in estimates? From https://news.ycombinator.com/item?id=38354679 https://news.ycombinator.com/item?id=38354679 : > "LLMs cannot find reasoning errors, but can correct them" (2023) https://news.ycombinator.com/item?id=38353285 https://news.ycombinator.com/item?id=38353285 > "Misalignment and Deception by an autonomous stock trading LLM agent" https://news.ycombinator.com/item?id=38353880#38354486 https://news.ycombinator.com/item?id=38353880#38354486 That being said, guess and check and then develop a fitting casual explanation is or is not the standard practice of science, so https://news.ycombinator.com/item?id=38124505 https://news.ycombinator.com/item?id=38124505 https://westurner.github.io/hnlog/#comment-38124505 https://westurner.github.io/hnlog/#comment-38124505 : > What does Mathlib have for SetTheory, ZFC, NFU, and HoTT? > Do any existing CAS systems have configurable axioms? Does LeanDojo have configurable axioms? From https://news.ycombinator.com/item?id=38527844 https://news.ycombinator.com/item?id=38527844 : > TIL i^4x == e^2iπx ... But SymPy says it isn't so (as the equality relation automated test assertion fails); and GeoGebra plots it as a unit circle and a line, but SymPy doesn't have a plot_complex() function to compare just one tool's output with another.
- kmill 3y ago
  That's a lot of links to take in, and I don't do really anything with ML, but feel free to head over to https://leanprover.zulipchat.com/ https://leanprover.zulipchat.com/ and start a discussion in the Machine Learning for Theorem Proving stream! My observation at the moment is that we haven't seen ML formalize a cutting-edge math paper and that it did in fact take a lot of experience to pull it off so quickly, experience that's not yet encoded in ML models. Maybe one day. Something that I didn't mention is that Terry Tao is perhaps the most intelligent, articulate, and conscientious person I have ever interacted with. I found it very impressive how quickly he absorbed the Lean language, what goes into formalization, and how to direct a formalization project. He could have done this whole thing on his own I am sure. No amount of modern ML can replace him at the helm. However, he is such an excellent communicator that he could have probably gotten well-above-average results from an LLM. My understanding is that he used tools like ChatGPT to learn Lean and formalization, and my experience is that what you get from these tools is proportional to the quality of what you put into them.

by kmill 3y ago

cs702 3y ago

> I helped a very little... Thank You for helping with the effort, even if it was only "a very little." I love coming across comments like yours on HN.

ska 3y ago

>Something that was necessary for the success of this was years of development that had already been For projects like this it is often very thankless work in the beginning, and can be a real grind. You need at least one person with a vision of how cool it will be in the (poorly defined) future, and a lot of determination.

pastage 3y ago
It is great for personal growth. Since I have been part of many such grinds that are now big data sets, I can honestly tell you that it is one of the best things in the world. I know that those thousands of hours of my work has led to 100x savings for other people. I also met people and could work on problems I would never get in professional life.

zozbot234 3y ago

> Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib Yes but the bulk of the work on this project was background as well. So the ease of use problem should be solving itself over time as more and more prereqs get filled in. BTW, I find it interesting that mathlib is apparently also getting refactored to accommodate constructive proofs better, as part of the porting effort to Lean 4. This might encourage more CS- and program-verification minded folks to join the effort, and maybe some folks in math-foundations too (though Lean suffers there by not being able to work with the homotopy-types axioms).

kmill 3y ago
Yes, sure, and that's how mathlib usually gets developed, project by project and PRing missing background material. I'm one of the mathlib maintainers, and I wanted to be sure there's acknowledgment here for the years of Boubaki-style work among hundreds of volunteers to build up the mathematics. In a way, now that the paper's been formalized it's time for the really hard work, which is figuring out how to restructure it (and mathlib) so that it can easily support future work. That's writing libraries for you. Where are you getting the idea mathlib is being refactored for constructive proofs? I wouldn't say that's on the road map. In fact, the core Lean developers are uninterested in pursuing supporting this. Since you're here, are you able to say why constructive proofs are interesting to program verification or (T)CS people? I've never heard anyone in TCS even know what constructivity is -- Lean supports their case where you write a program/algorithm and then (with classical logic) prove correctness and other properties. What would constructive logic give them?
- kmill 3y ago
  I'll mention that the "Lean way" for constructivity is that you write `def`s for constructions. These can depend on classical reasoning for well-typedness if you want (like for being sure a number is in range when indexing an array), but there is a computability checker. In particular, the compiler sees if there is a way to lower the `def` into some simply typed IR, and this IR can be further compiled to C. If you trust the compiler, then you can trust whether it's real construction. (Of course, you can also go and prove a definition evaluates to some value if you don't want to trust the evaluator.)

rowanG077 3y ago

Since you seem to be an expert on this matter I have always wondered whether at some point it becomes faster to prove novel theorems using a theorem prover then doing it on paper. I imagine that quite a bit of time is wasted in proving things that are already proven. In a similar manner that if there would be no libraries, just snippets of code in papers, in computer programming a lot of time would be wasted writing the same things again. I imagine a "proof finding" tool like hoogle is a "function finding" tool could provide a lot of value here. What is your perspective on this?

zozbot234 3y ago
The biggest benefit of a formalized theorem library is not so much proving entirely new theorems (though it helps a little bit I suppose) but refactoring the existing developments to make them more elegant, easier to understand, and enhance their generality. In fact, it's already the case that the average formal proof is written to be somewhat higher in abstraction and more straightforward in reasoning than the informal counterpart. This kind of refactoring work is quite hard to do with paper proofs alone, since one cannot essily be sure whether they've preserved correctness wrt. the original development. Having a proof assistant really is a big help there.
- jenesaispas 3y ago
  > The biggest benefit of a formalized theorem library is not [...] but [...] [citation needed] I think there are many benefits. Hard to claim that your favourite one is the biggest benefit. In general, I think it's a bit weird that you are repeatedly (also other HN threads, and sibling comments in this one) making unfounded claims about Lean/mathlib, to the point where you are telling maintainers how their system works. And if they explain that you are misunderstanding the system, you ignore their correction and bring up the next (or the same) unfounded claim. Disclaimer: I am a Lean/mathlib user.
  - zozbot234 3y ago
    > [citation needed] Whoops, you're right. Here's what Fields medalist Terence Tao has to say about it: https://terrytao.wordpress.com/2023/12/05/a-slightly-longer-lean-4-proof-tour/#comment-682450 https://terrytao.wordpress.com/2023/12/05/a-slightly-longer-... "...sometimes, after a proposition has been proven, someone in the project realizes that in order to apply the proposition neatly in some other part of the project, one has to slightly modify a hypothesis ... Often one can just modify that hypothesis and watch what the compiler does. ... [W]ith well-designed proofs, the process of modifying a proposition is often substantially easier than writing a proof from scratch. (Indeed it is this aspect of formalization where I think we really have a chance in the future of being in a situation where the task is faster to perform in a formal framework than in traditional pen-and-paper (and LaTeX) framework.)" > And if they explain that you are misunderstanding the system I don't think that's a fair description of the sibling threads. If a mathlib maintainer says "no, we're not going to avoid LEM/by-contradiction everywhere in our proof library, that would be silly" because that's what most mathematicians today think constructivism means, as in rejecting the bulk of existing math entirely as meaningless - and then they add "but yes, there are places where we want to work with our own assertions about decidability, and not let classical reasoning mess that up" I think it's entirely fair to call the latter pretty close to a constructivism-friendly approach. (Keep in mind that most practicing mathematicians don't work with foundations, so the fact that misconceptions like the above would be widespread is not surprising. The remaining argument is about the increased complexity of constructive reasoning, and it's entirely fair for a practical development to want to avoid that, and just work with classical statements. After all, most of the mathematical literature is indeed classical; it does not bother with the computational aspect or with the perceived messiness of numerical analysis.)

westurner 3y ago

> so he could very easily scramble a team of around 20 experienced Lean users What have you to say about methods such as these: "LeanDojo: Theorem Proving with Retrieval-Augmented Language Models" (2023) https://arxiv.org/abs/2306.15626 https://arxiv.org/abs/2306.15626 https://leandojo.org/ https://leandojo.org/ https://news.ycombinator.com/from?site=leandojo.org https://news.ycombinator.com/from?site=leandojo.org ( https://westurner.github.io/hnlog/#story-38435908 https://westurner.github.io/hnlog/#story-38435908 Ctrl-F "TheoremQA" (to find the citation and its references in my local personal knowledgebase HTML document with my comments archived in it), manually ) "TheoremQA: A Theorem-driven [STEM] Question Answering dataset" (2023) https://github.com/wenhuchen/TheoremQA#leaderboard https://github.com/wenhuchen/TheoremQA#leaderboard (they check LLM accuracy with Wolfram Mathematica) "Large language models as simulated economic agents (2022) [pdf]" https://news.ycombinator.com/item?id=34385880 https://news.ycombinator.com/item?id=34385880 : > Can any LLM do n-body gravity? What does it say when it doesn't know; doesn't have confidence in estimates? From https://news.ycombinator.com/item?id=38354679 https://news.ycombinator.com/item?id=38354679 : > "LLMs cannot find reasoning errors, but can correct them" (2023) https://news.ycombinator.com/item?id=38353285 https://news.ycombinator.com/item?id=38353285 > "Misalignment and Deception by an autonomous stock trading LLM agent" https://news.ycombinator.com/item?id=38353880#38354486 https://news.ycombinator.com/item?id=38353880#38354486 That being said, guess and check and then develop a fitting casual explanation is or is not the standard practice of science, so https://news.ycombinator.com/item?id=38124505 https://news.ycombinator.com/item?id=38124505 https://westurner.github.io/hnlog/#comment-38124505 https://westurner.github.io/hnlog/#comment-38124505 : > What does Mathlib have for SetTheory, ZFC, NFU, and HoTT? > Do any existing CAS systems have configurable axioms? Does LeanDojo have configurable axioms? From https://news.ycombinator.com/item?id=38527844 https://news.ycombinator.com/item?id=38527844 : > TIL i^4x == e^2iπx ... But SymPy says it isn't so (as the equality relation automated test assertion fails); and GeoGebra plots it as a unit circle and a line, but SymPy doesn't have a plot_complex() function to compare just one tool's output with another.

kmill 3y ago
That's a lot of links to take in, and I don't do really anything with ML, but feel free to head over to https://leanprover.zulipchat.com/ https://leanprover.zulipchat.com/ and start a discussion in the Machine Learning for Theorem Proving stream! My observation at the moment is that we haven't seen ML formalize a cutting-edge math paper and that it did in fact take a lot of experience to pull it off so quickly, experience that's not yet encoded in ML models. Maybe one day. Something that I didn't mention is that Terry Tao is perhaps the most intelligent, articulate, and conscientious person I have ever interacted with. I found it very impressive how quickly he absorbed the Lean language, what goes into formalization, and how to direct a formalization project. He could have done this whole thing on his own I am sure. No amount of modern ML can replace him at the helm. However, he is such an excellent communicator that he could have probably gotten well-above-average results from an LLM. My understanding is that he used tools like ChatGPT to learn Lean and formalization, and my experience is that what you get from these tools is proportional to the quality of what you put into them.