3 ms·

Thanks. I appreciate it. According to $ find leanprover.github.io/functional_programming_in_lean -name \*.html -exec html2text {} \; | wc -w 271248 T

Thanks. I appreciate it. According to $ find leanprover.github.io/functional_programming_in_lean -name \*.html -exec html2text {} \; | wc -w 271248 That's about 1,000 pages. Some of us who are less ambitious and motivated need an under 5-minutes example to feel compelled to engage with such a large amount of documentation. Essentially the problem is "There's hundreds of programming languages I'll never have the time to learn. Show me why I should care about this one and do it quickly." Given that, I actually appreciate the fancy example. It really shows off some interesting features in reaching a goal that's really simple to understand. It looks similar to Haskell in that it approaches programming in a mathematically formal and rigorous way. If you're deeply involved in the project, an example that would be really exciting to me would be a lean version of one of these proofs: https://en.wikipedia.org/wiki/Category:Computer-assisted_proofs https://en.wikipedia.org/wiki/Category:Computer-assisted_pro... or https://en.wikipedia.org/wiki/Computer-assisted_proof#Theorems_proved_with_the_help_of_computer_programs https://en.wikipedia.org/wiki/Computer-assisted_proof#Theore... Start the example with how the proof was initially tackled on a computer and show the challenges faced and then demonstrate how lean can do it more elegantly. I appreciate your time.

ykonstant 3y ago
I do not see how you are getting 1000 pages; the pdf is about 400 pages with copious amounts of sparse code blocks, and the introductory stuff (The chapters Getting to know Lean and Hello World) run about 86 pages. Certainly not "Lean in 5 minutes" for sure, but not a spellbook either. In any case, Lean is a proof formalization and verification language doubling as a general purpose programming language still in its research phase. If you are interested in how this sounds, you can check it out. If not, there is no need.
- kristopolous 3y ago
  I just did a recursive scrape of the tutorial site, converted the html to text, then did a word count using wc and simply divided it by the average number of words per page. Word in this case includes things like '(' and syntax characters. Regardless it was a rough metric meant to be demonstrative of the level of effort to go through the tutorial. The point is as an answer to the basic question "what is this and why should I care?" Responding with something over 10 pages is likely unadvisable, yet alone over 100. "Over 100" here is effectively equivalent to "over 5,000". The target should be like 0.25-5, and closer to the 0.25. Elevator pitch it. 1. For (target customers) 2. Who are dissatisfied with (the current market alternative) 3. Lean is a (new product category) 4. That provides (key problem-solving capability). 5. Unlike (the product alternative), 6. Lean (describe the key product features). https://www.elevatorpitchessentials.com/essays/CrossingTheChasmElevatorPitchTemplate.html https://www.elevatorpitchessentials.com/essays/CrossingTheCh...
  - uxp8u61q 3y ago
    If you have to listen to such an elevator pitch, you're not the target audience. This is bleeding-edge math/CS research. Talking about a "product" just shows that you have a fundamental misconception regarding what this is all about.
    - kristopolous 3y ago
      It's a way to describe things. You can describe, for example, the James Webb space telescope or the Large Hadron Collider in that way. You can also describe say, the Frankfurt school of critical theory or every other programming language. A product is an act of production here, as in some kind of process. Even things like classes of clouds and rocks can be described in that framework I don't expect Lean to be an exception Also to respond to the idea that I'm fundamentally unworthy of an explanation: I'm also not the target audience for the LHC or James Webb but effort has been made to describe it. They don't demand advanced physics degrees to unveil its purpose like they're some kind of secret society.
      - uxp8u61q 3y ago
        Don't be coy. Your use of words like "market", "features" or "customers" made it pretty clear what you meant by "product". > I'm also not the target audience for the LHC or James Webb but effort has been made to describe it. And there is an effort to describe Lean on their webpage. But I would be curious to know if you would be able to recall the "elevator pitch" you heard for the LHC that doesn't grossly gloss over any kind of relevant actual information. "Customers were dissatisfied because previous colliders were too small, so we made a bigger one. This allows us to hurl particles very fast at each other." Huzzah, you've just been elevator pitched. Do you actually know anything significant about the LHC after that pitch? I sincerely doubt it. You're also glossing over the fact that the LHC was started in 1998. The James Webb telescope has been in the works since the 90's. Meanwhile, Lean started as a research project in 2013, and Lean 4 is only 1.5 years old. Being angry that scientists have been developing the fundamentals before engaging in outreach is misguided at best.
mauricioc 3y ago
None of these proofs listed in the Wikipedia page are formalized in Lean at the moment, although a few are formalized in other theorem provers (Four Color Theorem in Coq, Kepler Conjecture in Isabelle). The "Formalization papers using Lean" section of https://leanprover-community.github.io/papers.html https://leanprover-community.github.io/papers.html lists some theorems whose proofs have been verified in Lean, but (despite being written in Isabelle) I think the Kepler Conjecture formalization is the best example of what you have in mind. The main difference between most of the examples you list via the Wikipedia page and the examples listed in the URL I cited above is how the computer is being used: in many cases, "computer-assisted" means an ad-hoc program was used to check a bunch of cases which would be too tedious for a human to check. But what happens if there is a bug in the used ad-hoc program (or, e.g., in a linear programming solver)? To increase confidence in the verification result, ideally both the validity of the case-checking and the logic for deducing the main theorem from the checked cases would be verified by a small and general "kernel"/proof checker. This is what theorem provers such as Lean, Coq and Isabelle allow.

ykonstant 3y ago

I do not see how you are getting 1000 pages; the pdf is about 400 pages with copious amounts of sparse code blocks, and the introductory stuff (The chapters Getting to know Lean and Hello World) run about 86 pages. Certainly not "Lean in 5 minutes" for sure, but not a spellbook either. In any case, Lean is a proof formalization and verification language doubling as a general purpose programming language still in its research phase. If you are interested in how this sounds, you can check it out. If not, there is no need.

kristopolous 3y ago
I just did a recursive scrape of the tutorial site, converted the html to text, then did a word count using wc and simply divided it by the average number of words per page. Word in this case includes things like '(' and syntax characters. Regardless it was a rough metric meant to be demonstrative of the level of effort to go through the tutorial. The point is as an answer to the basic question "what is this and why should I care?" Responding with something over 10 pages is likely unadvisable, yet alone over 100. "Over 100" here is effectively equivalent to "over 5,000". The target should be like 0.25-5, and closer to the 0.25. Elevator pitch it. 1. For (target customers) 2. Who are dissatisfied with (the current market alternative) 3. Lean is a (new product category) 4. That provides (key problem-solving capability). 5. Unlike (the product alternative), 6. Lean (describe the key product features). https://www.elevatorpitchessentials.com/essays/CrossingTheChasmElevatorPitchTemplate.html https://www.elevatorpitchessentials.com/essays/CrossingTheCh...
- uxp8u61q 3y ago
  If you have to listen to such an elevator pitch, you're not the target audience. This is bleeding-edge math/CS research. Talking about a "product" just shows that you have a fundamental misconception regarding what this is all about.
  - kristopolous 3y ago
    It's a way to describe things. You can describe, for example, the James Webb space telescope or the Large Hadron Collider in that way. You can also describe say, the Frankfurt school of critical theory or every other programming language. A product is an act of production here, as in some kind of process. Even things like classes of clouds and rocks can be described in that framework I don't expect Lean to be an exception Also to respond to the idea that I'm fundamentally unworthy of an explanation: I'm also not the target audience for the LHC or James Webb but effort has been made to describe it. They don't demand advanced physics degrees to unveil its purpose like they're some kind of secret society.
    - uxp8u61q 3y ago
      Don't be coy. Your use of words like "market", "features" or "customers" made it pretty clear what you meant by "product". > I'm also not the target audience for the LHC or James Webb but effort has been made to describe it. And there is an effort to describe Lean on their webpage. But I would be curious to know if you would be able to recall the "elevator pitch" you heard for the LHC that doesn't grossly gloss over any kind of relevant actual information. "Customers were dissatisfied because previous colliders were too small, so we made a bigger one. This allows us to hurl particles very fast at each other." Huzzah, you've just been elevator pitched. Do you actually know anything significant about the LHC after that pitch? I sincerely doubt it. You're also glossing over the fact that the LHC was started in 1998. The James Webb telescope has been in the works since the 90's. Meanwhile, Lean started as a research project in 2013, and Lean 4 is only 1.5 years old. Being angry that scientists have been developing the fundamentals before engaging in outreach is misguided at best.

mauricioc 3y ago

None of these proofs listed in the Wikipedia page are formalized in Lean at the moment, although a few are formalized in other theorem provers (Four Color Theorem in Coq, Kepler Conjecture in Isabelle). The "Formalization papers using Lean" section of https://leanprover-community.github.io/papers.html https://leanprover-community.github.io/papers.html lists some theorems whose proofs have been verified in Lean, but (despite being written in Isabelle) I think the Kepler Conjecture formalization is the best example of what you have in mind. The main difference between most of the examples you list via the Wikipedia page and the examples listed in the URL I cited above is how the computer is being used: in many cases, "computer-assisted" means an ad-hoc program was used to check a bunch of cases which would be too tedious for a human to check. But what happens if there is a bug in the used ad-hoc program (or, e.g., in a linear programming solver)? To increase confidence in the verification result, ideally both the validity of the case-checking and the logic for deducing the main theorem from the checked cases would be verified by a small and general "kernel"/proof checker. This is what theorem provers such as Lean, Coq and Isabelle allow.