undefined | Better HN

0 pointskristopolous2y ago0 comments

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

0 comments

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

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

kristopolousOP2y 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/CrossingTheCh...

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

1 more reply

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