Lean 4 on HN

Stream: general

[Ioannis Konstantoulas]

It seems news about the stable version announcement have hit the first page of Hacker news: https://news.ycombinator.com/item?id=37429938

Check it out if you care to answer people's questions.

[Bulhwi Cha]

kristopolous said:

…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

I'm trying to elevator-pitch Lean.

[Shreyas Srinivas]

Bulhwi Cha said:

I'm trying to elevator-pitch Lean.

Why should research projects have elevator pitches?

[Ruben Van de Velde]

Bulhwi Cha said:

kristopolous said:

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

I'm trying to elevator-pitch Lean.

Is this Reviewer 2?

[Shreyas Srinivas]

This is worse than the typical reviewer 2 who might at least appreciate that there is more to a paper than its title.

[Tyler Josephson ⚛️]

Everyone should learn how to elevator pitch their research! If you have 2 minutes with someone and you want to make an impression, you should be prepared! Otherwise, you'll miss opportunities. Not everyone has lots of time to explore what you care about, but with a good elevator pitch, you might be able to persuade them to spend that time.

For me, my audience is almost always scientists and engineers, especially in computational chemistry. My elevator pitch is first and foremost about bug-free code with rigorously checked mathematics. My pitch is essentially:

When you write code with popular programming languages like Python, you get instant feedback when you make little syntax errors, like failing to close parentheses. But more nuanced bugs, like "missing a minus sign in one of the equations" or "switching indices in a matrix calculation" won't be caught until runtime, or worse, until the program finishes and a human inspects the results and notices something is off. Lean is a new programming language, built by mathematicians, with a type system that allows it to state and prove theorems in math. This makes it unique from languages like Python, in that it can catch math errors before running the program, and provide broad guarantees that code doesn't have bugs." (time for me to say this is < 1 minute)

More specifically, if I'm pitching to this folks at NIST (who really care about nit-picky high standards), I'll point to their current repositories of molecular simulation code that's "state of the art" in terms of rigor, transparency, and reproducibility, and explain how we could do better with Lean.

[Bulhwi Cha]

Bulhwi Cha said:

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

Well, I tried. If there's any grammatical mistake in the above explanation, please let me know!

[Tyler Josephson ⚛️]

Who's your audience? What do they know / care about?

One thing to watch out for is jargon. If your audience doesn't know "univalent mathematics" or "dependent types," then you can either think about a substitute or try explaining in a different way. For example, "dependent types" doesn't mean anything to my audience and trips them up, so I describe it in looser terms, as "type system that allows it to state and prove theorems" -- but even saying "type system" is too technical for an audience that doesn't know some programming already.

Small grammar thing: "praised" to either "praise" or "are praising" or "like" - present tense is more exciting/forward-leaning.

[Shreyas Srinivas]

Tyler Josephson ⚛️ said:

Everyone should learn how to elevator pitch their research!

I have a few problems with this pitch:

1. your pitch works for any formal verification project, and there are a gazillion of them.
2. You compare Lean with python. But the exact same arguments would also justify funding a whole lot of other theorem provers. Why should the agency fund lean over Coq, Agda, or F*.
3. People have been saying this "prove broad guarantees that code doesn't have bugs" bit for a few decades. How's your pitch different? How would you catch people's attention?

[Shreyas Srinivas]

In general the issue with asking for an elevator pitch is, it needs to be brief and skip over enough technical details that it resembles the pitch for other products. And then it wouldn't meet the "new product category" criterion mentioned above.

[Tyler Josephson ⚛️]

Shreyas Srinivas said:

Tyler Josephson ⚛️ said:

Everyone should learn how to elevator pitch their research!

I have a few problems with this pitch:

1. your pitch works for any formal verification project, and there are a gazillion of them
2. You compare Lean with python. But the exact same arguments would also justify funding a whole lot of other theorem provers. Why should the agency fund lean over Coq, Agda, or F*.
3. People have been saying this "prove broad guarantees that code doesn't have bugs" bit for a few decades. How's your pitch different?

Oh absolutely, on all three points. But, my audience doesn't know anything about formal verification, so this is about the right level for them. A pitch to an audience that's familiar with Coq would need to hit a bunch of entirely different points. Elevator pitches ought to be tailored for the audience - I'm in a fun cross-disciplinary position that I get to introduce formal methods to people who don't know anything about it.

[Tyler Josephson ⚛️]

If the audience is already familiar with Coq, then start over the with elevator pitch. I have much less practice with this one, but I think the points to hit might be the functional-but-in-place features of Lean 4, the large math library (not actually a great point, since other provers have their own, but the nuanced point is that Lean's is growing faster / has more popularity right now?), the straightforward extraction of executable C code.

[Arthur Paulino]

I think Tyler's main point is crucial. Just look at the history of Lean itself and you'll see that the struggle to keep a project alive is real - especially if its nature is not inherently commercial.

The Lean FRO is a huge victory for the entire community for sure. But the long term success is still reliant on getting more people out there (not only mathematicians, but also software engineers, I'd say) to know and experiment Lean 4.

[Tyler Josephson ⚛️]

But I'd love to hear what y'all say - because I did have one person that I talked to say, "but I think you should do your research program with Isabelle/HOL instead," and I really wasn't sure what to say to that

[Shreyas Srinivas]

Agreed. But I find it easier to pitch ideas in a conversation with a few people since it allows for immediate follow-up questions and clarifications, since your target audience is small. HN, being a public forum attracts a large variety of people, especially if passive readers are included. So what would the target audience be. If you write a pitch for one type of person, another might be unimpressed and since this is the internet, they might add a dismissive and authoritative sounding comment.

[Tyler Josephson ⚛️]

Shreyas Srinivas said:

Agreed. But I find it easier to pitch ideas in a conversation with a few people since it allows for immediate follow-up questions and clarifications, since your target audience is small. HN, being a public forum attracts a large variety of people, especially if passive readers are included. So what would the target audience be. If you write a pitch for one type of person, another might be unimpressed and since this is the internet, they might add a dismissive and authoritative sounding comment.

Mmm. Indeed. Super fine line to walk when the audience is "anyone on the Internet who might stop by."

[Shreyas Srinivas]

Tyler Josephson ⚛️ said:

If the audience is already familiar with Coq, then start over the with elevator pitch. I have much less practice with this one, but I think the points to hit might be the functional-but-in-place features of Lean 4, the large math library (not actually a great point, since other provers have their own, but the nuanced point is that Lean's is growing faster / has more popularity right now?), the straightforward extraction of executable C code.

I have heard this Isabelle argument with algorithms formalisation. My response would be that Isabelle is a nightmare from a usability perspective. For just one example, one is forced to work on jedit or isabelle's own crippled version of vscodium. Another is the difficulty of metaprogramming (I might be biased on this one, but I found lean metaprogramming easier to learn thanks to the book).

[Shreyas Srinivas]

One can perhaps give (semi-)technical reasons for lean. Being easier to work with classical basic math out of the box is a major plus point for lean (specifically mathlib), since most systems are analysed with such math. For example, if I am designing a control system, I seriously cannot care one tiny bit about constructivism or even trying to work out which axioms are "fine". I just want to write a good old fashioned math proof that my system does what it should. Another plus point for lean is the functional programming aspect. Coq users might point out how programming language stuff and verification is easy on Coq, or more abstruse aspects like not implicitly including axioms, guarantees on strong normalisation, coinductive types etc. Isabelle and F* seem to have more powerful automation (although, optimistically it is a matter of time before other provers catch up).

But in the end I doubt any of these technical issues are such difficult barriers that they cannot be overcome in other theorem provers for practical use cases. For instance, Isabelle might have its sledgehammer but coq has coqhammer and lean will hopefully have a hammer soon. One of the basic promises of a theorem prover is that some day it will assist us in working with math. This promise cannot be met without addressing usability issues for programmers and mathematicians who are new to this stuff. This often conflicts with the needs of existing power users who cannot be ignored, and who have fallen in love with the current ways of using the system. So any established prover will have a difficult time overhauling its UX. It can get even harder if aspects of the UX are tightly coupled with the system and disentangling them is hard. In that sense, Lean's separation of concerns is a major plus.

[Sven Nilsen]

(deleted)

[Shreyas Srinivas]

For algorithms, if your goal is to verify algorithms, Isabelle is great. If you want to build a unified library of algorithms that eventually attracts contributors from the algorithms community who have never seen a theorem prover before, the choice becomes less clear.