4 ms·

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 Get

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.
      - kristopolous 3y ago
        It's a quote from a famous book, crossing the chasm and it's a trivial exercise that you're refusing to engage with and mocking me in bad faith, violating HN rules. The LHC example is so simple ChatGPT did it in a single go. Again, this is generative AI "For particle physics researchers seeking to unravel the cosmos, the Large Hadron Collider (LHC) offers an unparalleled solution. Unlike conventional particle accelerators, the LHC achieves extraordinary collision energies, enabling experiments that mirror the early universe's conditions. This distinctive feature has led to groundbreaking discoveries, notably the Higgs boson. In contrast to other accelerators, the LHC's unmatched power and global scientific network establish it as the premier choice for unlocking the universe's deepest secrets, setting it apart in its capacity to explore uncharted frontiers in particle physics." In fact, I asked it to do it for Lean and it could do it just fine. In contrast, the main lean website starts like this: The Lean (jargon) is a (jargon) developed principally by Leonardo de Moura. There's this bizarre fetishism for making things inaccessible and then personally belittling and insulting people when they state the obvious. The other inexplicable behavior is the tendency to give "answers" by pointing to giant manuals that don't answer the question. This is endemic to ML. Someone asks what say "Vit-L" versus "Vit-H" means and the answer is usually a link to some ~40 page peer reviewed LaTeX that mentions the acronyms but doesn't define it either. The strategy is to do anything but be transparent and direct.
- chabulhwi 3y ago
  Lean is an interactive theorem prover. It can verify proofs written in Lean by humans. Mathlib is a monolithic library of classical mathematics written in Lean. Mathematicians contributing to Mathlib love it because it has all the interconnected subdisciplines they need in one place, and most of them aren't huge fans of constructive mathematics or univalent mathematics. Lean is also a strict pure functional programming language with dependent types. You can write correct and maintainable programs in Lean. You can also write proofs showing that a program terminates or it computes the desired answer, etc. Some computer scientists and programmers praise Lean's extensible syntax and editor support. See also: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.204.20on.20HN/near/389898786 https://leanprover.zulipchat.com/#narrow/stream/113488-gener...
  - kristopolous 3y ago
    Awesome!

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.
    - kristopolous 3y ago
      It's a quote from a famous book, crossing the chasm and it's a trivial exercise that you're refusing to engage with and mocking me in bad faith, violating HN rules. The LHC example is so simple ChatGPT did it in a single go. Again, this is generative AI "For particle physics researchers seeking to unravel the cosmos, the Large Hadron Collider (LHC) offers an unparalleled solution. Unlike conventional particle accelerators, the LHC achieves extraordinary collision energies, enabling experiments that mirror the early universe's conditions. This distinctive feature has led to groundbreaking discoveries, notably the Higgs boson. In contrast to other accelerators, the LHC's unmatched power and global scientific network establish it as the premier choice for unlocking the universe's deepest secrets, setting it apart in its capacity to explore uncharted frontiers in particle physics." In fact, I asked it to do it for Lean and it could do it just fine. In contrast, the main lean website starts like this: The Lean (jargon) is a (jargon) developed principally by Leonardo de Moura. There's this bizarre fetishism for making things inaccessible and then personally belittling and insulting people when they state the obvious. The other inexplicable behavior is the tendency to give "answers" by pointing to giant manuals that don't answer the question. This is endemic to ML. Someone asks what say "Vit-L" versus "Vit-H" means and the answer is usually a link to some ~40 page peer reviewed LaTeX that mentions the acronyms but doesn't define it either. The strategy is to do anything but be transparent and direct.
chabulhwi 3y ago
Lean is an interactive theorem prover. It can verify proofs written in Lean by humans. Mathlib is a monolithic library of classical mathematics written in Lean. Mathematicians contributing to Mathlib love it because it has all the interconnected subdisciplines they need in one place, and most of them aren't huge fans of constructive mathematics or univalent mathematics. Lean is also a strict pure functional programming language with dependent types. You can write correct and maintainable programs in Lean. You can also write proofs showing that a program terminates or it computes the desired answer, etc. Some computer scientists and programmers praise Lean's extensible syntax and editor support. See also: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.204.20on.20HN/near/389898786 https://leanprover.zulipchat.com/#narrow/stream/113488-gener...
- kristopolous 3y ago
  Awesome!