5 ms·

There is no excuse anymore. I have to try it out.

fithisux 3y ago
Me too, I want to follow https://github.com/blanchette/logical_verification_2023 https://github.com/blanchette/logical_verification_2023 The hitchhiker's guide
xigoi 3y ago
I tried Lean twice and what caused me to stop both times was a severe lack of documentation. That's a shame, because it's an awesome language.
- bmitc 3y ago
  I also tried to get into it recently, and I feel theorem proving has been pretty substantially oversold. It seems that if you wanted to work through the proofs in even an advanced undergraduate or early graduate textbook, you would basically have publishable material at the end because of the lack of cohesive libraries. There is a lot that gets buried in and is still open to implementation details, and I don't see any clear way of simply proceeding. It started to feel like a major distraction from just doing the mathematics rather than an aid, like it's supposed to be. It feels a little like the Rust ecosystem, where there is a land grab rush to introduce various libraries.
  - jhanschoo 3y ago
    I agree that there's generally too little results in mathlib and for that matter in any theorem prover, but I didn't think that work on formalizing such stuff (advanced undergrad results / early grad results) is publishable. Was I wrong in this?
    - zozbot234 3y ago
      There's plenty of published papers about newly formalized proofs, even in "undergrad" math. A formal proof development generally brings to light new information about the original proof, both by plugging all potential inaccuracies/missing steps and in being especially easy to refactor, abstracting out common patterns that might be reused elsewhere.
- 7373737373 3y ago
  Same, I also found no good "for programmers" introduction.
  - crvdgc 3y ago
    There is a short one[1] from Functional Programming in Lean, which is itself an introduction to Lean 4 from the programming's perspective. Highly recommended if you're interested in dependent types. [1]: https://leanprover.github.io/functional_programming_in_lean/introduction.html https://leanprover.github.io/functional_programming_in_lean/...
  - uxp8u61q 3y ago
    Because the audience isn't "programmers".
    - ykonstant 3y ago
      I think that is unnecessarily hostile; I believe Lean 4 can become a very capable programming language for mundane tasks!
      - uxp8u61q 3y ago
        Hostile? I just stated that the audience isn't programmers.
        7373737373 3y ago
        The age of guilds has long passed Are people like these not programmers? https://leandojo.org/ https://leandojo.org/
    - siknad 3y ago
      How can the audience of a general-purpose programming language not be "programmers"?
    - nequo 3y ago
      I don’t think that your post is hostile. But from what I’ve heard, it is untrue because Lean 4 is intended to be a general purpose programming language, not only a theorem prover. I can’t find a source that directly states this goal but at the least this paper by Leo de Moura and Sebastian Ullrich presents it as a programming language: https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37 https://link.springer.com/chapter/10.1007/978-3-030-79876-5_... Microsoft also sponsored David Thrane Christiansen’s book, Functional Programming in Lean[1] (which I’m sure you know about!). That is another indication that they intend to reach programmers. [1] https://leanprover.github.io/functional_programming_in_lean/ https://leanprover.github.io/functional_programming_in_lean/
- brohee 3y ago
  Kinda agree but Mathlib and its documentation makes for a big corpus to learn by example from. Not ideal but it helps. https://github.com/leanprover-community/mathlib https://github.com/leanprover-community/mathlib
- westurner 3y ago
  A https://learnxinyminutes.com/ https://learnxinyminutes.com/ for Lean and Lean Mathlib would be a helpful resource
  - xigoi 3y ago
    On the contrary, I think the basics are covered pretty well by the official documentation, but it's lacking the more advanced stuff.
    - ykonstant 3y ago
      I agree; for simple and "beginning intermediate" tasks, Functional Programming in Lean has it all; but the more advanced features are only documented in the source code and doc-strings. There is also a lack of general listings: for data structures, for file access API, for algorithms etc.
      - westurner 3y ago
        Is there an eBNF+PEG or similar grammar for the language parser that a more complete language reference can be generated from? Does Lean have docstrings with embedded markup like Python? The Python Language Reference: https://docs.python.org/3/reference/ https://docs.python.org/3/reference/ The Python Language Reference > 10. Full Grammar specification: https://docs.python.org/3/reference/grammar.html https://docs.python.org/3/reference/grammar.html LearnXinYminutes > Where X=Python: https://learnxinyminutes.com/docs/python/ https://learnxinyminutes.com/docs/python/ In the language and then the docs, Python's collections.abc Abstract Base Classes did not initially exist. There's now a table of ABCs in the docs: https://docs.python.org/3/library/collections.abc.html#collections-abstract-base-classes https://docs.python.org/3/library/collections.abc.html#colle... In Python, they're not interfaces, they're ABCs.
- hiker 3y ago
  Get on Zulip[1] and ask for help when stuck. The community is friendly and has gotten quite large although they are mostly mathematicians at the moment. [1] https://leanprover.zulipchat.com/ https://leanprover.zulipchat.com/

Me too, I want to follow https://github.com/blanchette/logical_verification_2023 https://github.com/blanchette/logical_verification_2023 The hitchhiker's guide

xigoi 3y ago

I tried Lean twice and what caused me to stop both times was a severe lack of documentation. That's a shame, because it's an awesome language.

bmitc 3y ago
I also tried to get into it recently, and I feel theorem proving has been pretty substantially oversold. It seems that if you wanted to work through the proofs in even an advanced undergraduate or early graduate textbook, you would basically have publishable material at the end because of the lack of cohesive libraries. There is a lot that gets buried in and is still open to implementation details, and I don't see any clear way of simply proceeding. It started to feel like a major distraction from just doing the mathematics rather than an aid, like it's supposed to be. It feels a little like the Rust ecosystem, where there is a land grab rush to introduce various libraries.
- jhanschoo 3y ago
  I agree that there's generally too little results in mathlib and for that matter in any theorem prover, but I didn't think that work on formalizing such stuff (advanced undergrad results / early grad results) is publishable. Was I wrong in this?
  - zozbot234 3y ago
    There's plenty of published papers about newly formalized proofs, even in "undergrad" math. A formal proof development generally brings to light new information about the original proof, both by plugging all potential inaccuracies/missing steps and in being especially easy to refactor, abstracting out common patterns that might be reused elsewhere.
7373737373 3y ago
Same, I also found no good "for programmers" introduction.
- crvdgc 3y ago
  There is a short one[1] from Functional Programming in Lean, which is itself an introduction to Lean 4 from the programming's perspective. Highly recommended if you're interested in dependent types. [1]: https://leanprover.github.io/functional_programming_in_lean/introduction.html https://leanprover.github.io/functional_programming_in_lean/...
- uxp8u61q 3y ago
  Because the audience isn't "programmers".
  - ykonstant 3y ago
    I think that is unnecessarily hostile; I believe Lean 4 can become a very capable programming language for mundane tasks!
    - uxp8u61q 3y ago
      Hostile? I just stated that the audience isn't programmers.
      - 7373737373 3y ago
        The age of guilds has long passed Are people like these not programmers? https://leandojo.org/ https://leandojo.org/
  - siknad 3y ago
    How can the audience of a general-purpose programming language not be "programmers"?
  - nequo 3y ago
    I don’t think that your post is hostile. But from what I’ve heard, it is untrue because Lean 4 is intended to be a general purpose programming language, not only a theorem prover. I can’t find a source that directly states this goal but at the least this paper by Leo de Moura and Sebastian Ullrich presents it as a programming language: https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37 https://link.springer.com/chapter/10.1007/978-3-030-79876-5_... Microsoft also sponsored David Thrane Christiansen’s book, Functional Programming in Lean[1] (which I’m sure you know about!). That is another indication that they intend to reach programmers. [1] https://leanprover.github.io/functional_programming_in_lean/ https://leanprover.github.io/functional_programming_in_lean/
brohee 3y ago
Kinda agree but Mathlib and its documentation makes for a big corpus to learn by example from. Not ideal but it helps. https://github.com/leanprover-community/mathlib https://github.com/leanprover-community/mathlib
westurner 3y ago
A https://learnxinyminutes.com/ https://learnxinyminutes.com/ for Lean and Lean Mathlib would be a helpful resource
- xigoi 3y ago
  On the contrary, I think the basics are covered pretty well by the official documentation, but it's lacking the more advanced stuff.
  - ykonstant 3y ago
    I agree; for simple and "beginning intermediate" tasks, Functional Programming in Lean has it all; but the more advanced features are only documented in the source code and doc-strings. There is also a lack of general listings: for data structures, for file access API, for algorithms etc.
    - westurner 3y ago
      Is there an eBNF+PEG or similar grammar for the language parser that a more complete language reference can be generated from? Does Lean have docstrings with embedded markup like Python? The Python Language Reference: https://docs.python.org/3/reference/ https://docs.python.org/3/reference/ The Python Language Reference > 10. Full Grammar specification: https://docs.python.org/3/reference/grammar.html https://docs.python.org/3/reference/grammar.html LearnXinYminutes > Where X=Python: https://learnxinyminutes.com/docs/python/ https://learnxinyminutes.com/docs/python/ In the language and then the docs, Python's collections.abc Abstract Base Classes did not initially exist. There's now a table of ABCs in the docs: https://docs.python.org/3/library/collections.abc.html#collections-abstract-base-classes https://docs.python.org/3/library/collections.abc.html#colle... In Python, they're not interfaces, they're ABCs.
hiker 3y ago
Get on Zulip[1] and ask for help when stuck. The community is friendly and has gotten quite large although they are mostly mathematicians at the moment. [1] https://leanprover.zulipchat.com/ https://leanprover.zulipchat.com/