11 ms·

Lean 4.0

130 points by quag 3y ago

garfieldnate 3y ago
I'm a programmer and I'm excited to learn Lean as a new tool for thought. I find that Haskell sells itself as a programming language but the reality is quite arcane, and its tools feel slow and bloated. Lean 4 is sort of the opposite, selling itself as a math toolkit but actually having very considerately (and practically) designed support tools (VSCode integration, build system) and core language features. I'm reading through Functional Programming in Lean now, supplementing with the Lean Manual and also Lean's prelude file, which is well commented and pretty readable. I love that the output window's contents are clickable ("failed to synthesize type class X Y Z" -> click on X, Y or Z to go to the definitions). I'm excited to try out the widget interface, which lets you complete proofs through visuospatial reasoning (see the Rubix cube project). I'm really hoping that this serves as a new tool for programming-minded people to learn math and contribute easy-to-understand proofs in a way that was never possible before. Once I've gone through the beginner materials, I want to try the math problems at the beginning of https://brickisland.net/DDGSpring2023/ https://brickisland.net/DDGSpring2023/, which has great tools for its programming projects but nothing for its proof assignments. The documentation still has holes, but the Lean community is more helpful and welcoming than any other I've ever encountered, and I'm confident that I'll get an answer for every question I have. For the Lean folks: an entry on learnxinyminutes is an absolute must in my book. It would be a great place to demonstrate how familiar and practical Lean can be, with its for loops and arrays and hash maps and whatever else. Generally if a language is not there, I figure it must not be mature enough to try out (Lean has been an exception for me).
- garfieldnate 3y ago
  Reading some of the other comments that say that Functional Programming in Lean is a good enough introduction and a learnxinyminutes is unnecessary, I feel I need to clarify that y should be somewhere between 5 and 15. Functional Programming in Lean is going to be probably 20 hours or more for me.
hackandthink 3y ago
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.
Gys 3y ago
> Lean is a new open source theorem prover being developed at Microsoft Research. It is a research project that aims to bridge the gap between interactive and automated theorem proving. Lean can be also used as a programming language. Actually, some Lean features are implemented in Lean itself.
- karmakaze 3y ago
  I've heard of Lean some time ago and is now v4. Is the opensource part which is new or has this text not been updated since v1?
  - uxp8u61q 3y ago
    I have trouble parsing your sentence, so hopefully what follows will help. - Lean has always been open source. - Lean 4 has been in development for a while, with the first milestone (alpha version) published in January 2021.
taliesinb 3y ago
Does anyone know if Lean 4 has encoded much category theory?
- hackandthink 3y ago
  Everything I can think of and more of what I'll ever need: https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/CategoryTheory https://github.com/leanprover-community/mathlib4/tree/master...
  - hackandthink 3y ago
    Though I did not find Topos Theory.
    - hiker 3y ago
      There are definitions for sheaves, Grothendieck topologies and sites[1] which were extensively used in the Liquid Tensor Experiment[2] [1] https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/CategoryTheory/Sites https://github.com/leanprover-community/mathlib4/tree/master... [2] https://leanprover-community.github.io/blog/posts/lte-final/ https://leanprover-community.github.io/blog/posts/lte-final/
      - hackandthink 3y ago
        Thanks, and there is Subobject, which looks like the subobject classifier. https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory/Subobject/Basic.lean https://github.com/leanprover-community/mathlib4/blob/master...
        generalnonsense 3y ago
        To clarify, this is not really related to subobject classifiers. This defines subobjects of `X` as equivalence classes of monomorphisms with target `X`.
    - 3y ago
koito17 3y ago
One of my major concerns with Lean 4 is when I asked about mathlib compatibility some 2-3 years ago and the only reply I got was from Kevin Buzzard, implying that the best we can do is essentially rewrite it all! Correct me if I am wrong, but I think mathlib still uses a community-maintained fork of Lean 3. I love Lean and its relative ease-of-use compared to e.g. Coq, but man, having to rewrite all of mathlib is a real bummer if that is indeed what has to happen for Lean 4 compatibility.
- mauricioc 3y ago
  Mathlib was fully ported to Lean 4 (https://github.com/leanprover-community/mathlib4 https://github.com/leanprover-community/mathlib4), and the Lean 3 version is deprecated now. Edit: Adding a little bit more detail, it was ported one file at a time, using the automated translation from mathport (https://github.com/leanprover-community/mathport https://github.com/leanprover-community/mathport) as a starting point.
kristopolous 3y ago
I really find how theoreticians approach things to be challenging. Given that I headed to rosetta code to find some examples. Here's FizzBuzz in Lean 4: https://rosettacode.org/wiki/FizzBuzz#Lean https://rosettacode.org/wiki/FizzBuzz#Lean def fizz : String := "Fizz" def buzz : String := "Buzz" def newLine : String := "\n" def isDivisibleBy (n : Nat) (m : Nat) : Bool := match m with | 0 => false | (k + 1) => (n % (k + 1)) = 0 def getTerm (n : Nat) : String := if (isDivisibleBy n 15) then (fizz ++ buzz) else if (isDivisibleBy n 3) then fizz else if (isDivisibleBy n 5) then buzz else toString (n) def range (a : Nat) (b : Nat) : List (Nat) := match b with | 0 => [] | m + 1 => a :: (range (a + 1) m) def getTerms (n : Nat) : List (String) := (range 1 n).map (getTerm) def addNewLine (accum : String) (elem : String) : String := accum ++ elem ++ newLine def fizzBuzz : String := (getTerms 100).foldl (addNewLine) ("") def main : IO Unit := IO.println (fizzBuzz) #eval main Hopefully that's helpful to others.
- mauricioc 3y ago
  Whoever wrote this was probably trying to showcase more of the language's functional features (or just trying to be clever). This works: def main := for i in [1:101] do if i % 15 == 0 then IO.println "FizzBuzz" else if i % 3 == 0 then IO.println "Fizz" else if i % 5 == 0 then IO.println "Buzz" else IO.println s!"{i}" You can run it with `lean --run FizzBuzz.lean`, and you can read more about programming in Lean 4 at https://leanprover.github.io/functional_programming_in_lean/ https://leanprover.github.io/functional_programming_in_lean/.
  - kristopolous 3y ago
    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.
harel 3y ago
It took me about a minute and more than one click to reach a page which told me what lean IS. Hint: In the Readme, it's the Home Page link, then About.
- kookamamie 3y ago
  Came here to comment the same. The entire GH project seems to assume the visitor knows what Lean is.
hackandthink 3y ago
Is Lean a Category? (like much debated: is Hask(ell) a Category) "In this section we set up the theory so that Lean's types and functions between them can be viewed as a `LargeCategory` in our framework." So it seems to be proven that there is a Category Lean! https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory/Types.lean https://github.com/leanprover-community/mathlib4/blob/master...
- deleted 3y ago
  [deleted]
- hiker 3y ago
  Yes for the fragment of total and noncomputable functions which mathematicians use. For partial functions (which Lean also supports) I think the same arguments hold as for the "Haskell Category".
2pEXgD0fZ5cF 3y ago
Does Lean have something similar to Haskell's List comprehension [1] or some kind of set builder notation for functional programming purposes? [1]: Example: `[x*2 | x <- [1..10]]`
- skavi 3y ago
  never understood the appeal of this syntax over standard do notation or just fmap.
  - nequo 3y ago
    List comprehensions read like math which we know from school. Do notation reads like Haskell which is fine but less accessible to non-Haskellers. Fmap is somewhat less convenient for slightly more complex examples such as [x*y | x <- [1..10], y <- [2,3,5]]
    - sullyj3 3y ago
      For that you'd use Applicative (*) <$> [1..10] <*> [2,3,5] -- or liftA2 (*) [1..10] [2,3,5] Admittedly also not accessible to non-haskellers. But on the other hand, if you're going to learn a language, you ought to learn its idioms at some point.
      - ykonstant 3y ago
        That being said, nequo's request is not unreasonable; given Lean's advanced metaprogramming facilities, their request should be easy to implement. The nice thing nequo's example illustrates is rank polymorphism: list comprehensions work with lists, products of two, three, four,... lists with the same easy notation : `[n-ary function | x_1 <- List_1, ..., x_n <- List_n]`. It is quite nice to have this, especially for complex numerical operations. Note also that unlike Lean 3, in Lean 4 `List` does not inherently implement `Applicative` or `Monad`, so your code cannot work as is.
        eric-wieser 3y ago
DataDaoDe 3y ago
I’ve been very excited by lean, but every time I try to set things up I get riddled with exceptions, errors, library incompatibilities, lean 3/4 problems. Tuts or documentation that is outdated or just doesn’t work. It has made me wonder, is this just really really alpha software, are they working at a bleeding rate? Idk, but I’ve been enticed multiple times by the promise of lean, maybe I’m just missing some info or should stick it out or just wait until it gets more stable. Anyone have any insight here?
- ykonstant 3y ago
  Yes, you should expect some frustration, especially if you want to configure things your way. The least painful pipeline should be the following (only follow the instructions at the pages I am listing, as otherwise things may get too confusing): 1) Install lean as a VS Code extension lean4 following : https://leanprover.github.io/lean4/doc/quickstart.html https://leanprover.github.io/lean4/doc/quickstart.html 2) Read about using the build system `lake` here : https://leanprover.github.io/lean4/doc/setup.html https://leanprover.github.io/lean4/doc/setup.html 3) Note that this does not install mathlib4; leave that for later. 4) Start playing around with basic examples in VS Code by reading the beginning sections of https://leanprover.github.io/functional_programming_in_lean/title.html https://leanprover.github.io/functional_programming_in_lean/... 5) If something does not work on break, ask in the Zulip chat; the devs are gathering pain points to improve tooling every day. If this seems too painful, indeed you may want to wait a bit for the tooling to improve.
- kmill 3y ago
  Re Lean 3/4 problems: the port of mathlib from Lean 3 to Lean 4 just finished this summer, and unfortunately there's still going to be some confusion between the two for a little while! The mathlib community has been working on getting the documentation to all refer to Lean 4 -- if you find anything old please point it out on the Zulip. There's usually someone around who can fix it relatively quickly. I think it's better to think of it as bleeding-edge research software rather than alpha software. There might be a little bit of culture shock if you're used to industry-oriented software, but part of this stable version announcement is that there's a new Lean organization that now has resources to improve the experience.
zone411 3y ago
LeanDojo shows promise in allowing interaction with the proof environment programmatically and through LLMs: https://leandojo.org/ https://leandojo.org/. This NY Times article is a nice overview of AI in math proofs: https://www.nytimes.com/2023/07/02/science/ai-mathematics-machine-learning.html https://www.nytimes.com/2023/07/02/science/ai-mathematics-ma... (https://archive.ph/t0BhD https://archive.ph/t0BhD) Here is a chart of Mathlib's growth: https://leanprover-community.github.io/mathlib_stats.html https://leanprover-community.github.io/mathlib_stats.html
- mcshicks 3y ago
  LeanDojo looks cool! I will check it out. I did the natural number game in lean 3, and was excited to see the author of "How to Prove it" had written an online book, "How to prove it with Lean" to as an accompaniment to the book, but it was written in lean 4. I decided to redo it in Lean 4 (still working on it) and had some troubles but was super happy with the responses I got on the Zulip Chat. It was a bit tricky to install it but the lake system seems like a big improvement over how I installed lean 3. I used the emacs version of lean mode for lean 4. How to Prove it with lean https://djvelleman.github.io/HTPIwL/ https://djvelleman.github.io/HTPIwL/ Lean 4 Natural Number Game https://adam.math.hhu.de/#/g/hhu-adam/NNG4 https://adam.math.hhu.de/#/g/hhu-adam/NNG4 Lean Zulip Chat https://leanprover.zulipchat.com/ https://leanprover.zulipchat.com/ Emacs lean 4 mode https://github.com/leanprover/lean4-mode https://github.com/leanprover/lean4-mode
agentultra 3y ago
Exciting! I've been picking up some small side projects in Lean again to add more to https://agentultra.github.io/lean-4-hackers/ https://agentultra.github.io/lean-4-hackers/ -- a guide for programmers interested in using it as a programming language. Congrats on the milestone!
- ykonstant 3y ago
  That's an excellent starting guide, nice!
ykonstant 3y ago
The Lean Zulip chat includes a "Is there code for X" section; you can go there and ask if a specific theorem or research problem has been formalized/verified in Lean, and if not, whether someone is working or intends to work on it. This way you can form impromptu working groups if you find others interested in your problem.

130 points by quag 3y ago

I'm a programmer and I'm excited to learn Lean as a new tool for thought. I find that Haskell sells itself as a programming language but the reality is quite arcane, and its tools feel slow and bloated. Lean 4 is sort of the opposite, selling itself as a math toolkit but actually having very considerately (and practically) designed support tools (VSCode integration, build system) and core language features. I'm reading through Functional Programming in Lean now, supplementing with the Lean Manual and also Lean's prelude file, which is well commented and pretty readable. I love that the output window's contents are clickable ("failed to synthesize type class X Y Z" -> click on X, Y or Z to go to the definitions). I'm excited to try out the widget interface, which lets you complete proofs through visuospatial reasoning (see the Rubix cube project). I'm really hoping that this serves as a new tool for programming-minded people to learn math and contribute easy-to-understand proofs in a way that was never possible before. Once I've gone through the beginner materials, I want to try the math problems at the beginning of https://brickisland.net/DDGSpring2023/ https://brickisland.net/DDGSpring2023/, which has great tools for its programming projects but nothing for its proof assignments. The documentation still has holes, but the Lean community is more helpful and welcoming than any other I've ever encountered, and I'm confident that I'll get an answer for every question I have. For the Lean folks: an entry on learnxinyminutes is an absolute must in my book. It would be a great place to demonstrate how familiar and practical Lean can be, with its for loops and arrays and hash maps and whatever else. Generally if a language is not there, I figure it must not be mature enough to try out (Lean has been an exception for me).

garfieldnate 3y ago
Reading some of the other comments that say that Functional Programming in Lean is a good enough introduction and a learnxinyminutes is unnecessary, I feel I need to clarify that y should be somewhere between 5 and 15. Functional Programming in Lean is going to be probably 20 hours or more for me.

hackandthink 3y ago

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.

Gys 3y ago

> Lean is a new open source theorem prover being developed at Microsoft Research. It is a research project that aims to bridge the gap between interactive and automated theorem proving. Lean can be also used as a programming language. Actually, some Lean features are implemented in Lean itself.

karmakaze 3y ago
I've heard of Lean some time ago and is now v4. Is the opensource part which is new or has this text not been updated since v1?
- uxp8u61q 3y ago
  I have trouble parsing your sentence, so hopefully what follows will help. - Lean has always been open source. - Lean 4 has been in development for a while, with the first milestone (alpha version) published in January 2021.

taliesinb 3y ago

Does anyone know if Lean 4 has encoded much category theory?

hackandthink 3y ago
Everything I can think of and more of what I'll ever need: https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/CategoryTheory https://github.com/leanprover-community/mathlib4/tree/master...
- hackandthink 3y ago
  Though I did not find Topos Theory.
  - hiker 3y ago
    There are definitions for sheaves, Grothendieck topologies and sites[1] which were extensively used in the Liquid Tensor Experiment[2] [1] https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/CategoryTheory/Sites https://github.com/leanprover-community/mathlib4/tree/master... [2] https://leanprover-community.github.io/blog/posts/lte-final/ https://leanprover-community.github.io/blog/posts/lte-final/
    - hackandthink 3y ago
      Thanks, and there is Subobject, which looks like the subobject classifier. https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory/Subobject/Basic.lean https://github.com/leanprover-community/mathlib4/blob/master...
      - generalnonsense 3y ago
        To clarify, this is not really related to subobject classifiers. This defines subobjects of `X` as equivalence classes of monomorphisms with target `X`.
  - 3y ago

koito17 3y ago

One of my major concerns with Lean 4 is when I asked about mathlib compatibility some 2-3 years ago and the only reply I got was from Kevin Buzzard, implying that the best we can do is essentially rewrite it all! Correct me if I am wrong, but I think mathlib still uses a community-maintained fork of Lean 3. I love Lean and its relative ease-of-use compared to e.g. Coq, but man, having to rewrite all of mathlib is a real bummer if that is indeed what has to happen for Lean 4 compatibility.

mauricioc 3y ago
Mathlib was fully ported to Lean 4 (https://github.com/leanprover-community/mathlib4 https://github.com/leanprover-community/mathlib4), and the Lean 3 version is deprecated now. Edit: Adding a little bit more detail, it was ported one file at a time, using the automated translation from mathport (https://github.com/leanprover-community/mathport https://github.com/leanprover-community/mathport) as a starting point.

kristopolous 3y ago

I really find how theoreticians approach things to be challenging. Given that I headed to rosetta code to find some examples. Here's FizzBuzz in Lean 4: https://rosettacode.org/wiki/FizzBuzz#Lean https://rosettacode.org/wiki/FizzBuzz#Lean def fizz : String := "Fizz" def buzz : String := "Buzz" def newLine : String := "\n" def isDivisibleBy (n : Nat) (m : Nat) : Bool := match m with | 0 => false | (k + 1) => (n % (k + 1)) = 0 def getTerm (n : Nat) : String := if (isDivisibleBy n 15) then (fizz ++ buzz) else if (isDivisibleBy n 3) then fizz else if (isDivisibleBy n 5) then buzz else toString (n) def range (a : Nat) (b : Nat) : List (Nat) := match b with | 0 => [] | m + 1 => a :: (range (a + 1) m) def getTerms (n : Nat) : List (String) := (range 1 n).map (getTerm) def addNewLine (accum : String) (elem : String) : String := accum ++ elem ++ newLine def fizzBuzz : String := (getTerms 100).foldl (addNewLine) ("") def main : IO Unit := IO.println (fizzBuzz) #eval main Hopefully that's helpful to others.

mauricioc 3y ago
Whoever wrote this was probably trying to showcase more of the language's functional features (or just trying to be clever). This works: def main := for i in [1:101] do if i % 15 == 0 then IO.println "FizzBuzz" else if i % 3 == 0 then IO.println "Fizz" else if i % 5 == 0 then IO.println "Buzz" else IO.println s!"{i}" You can run it with `lean --run FizzBuzz.lean`, and you can read more about programming in Lean 4 at https://leanprover.github.io/functional_programming_in_lean/ https://leanprover.github.io/functional_programming_in_lean/.
- kristopolous 3y ago
  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.

harel 3y ago

It took me about a minute and more than one click to reach a page which told me what lean IS. Hint: In the Readme, it's the Home Page link, then About.

kookamamie 3y ago
Came here to comment the same. The entire GH project seems to assume the visitor knows what Lean is.

hackandthink 3y ago

Is Lean a Category? (like much debated: is Hask(ell) a Category) "In this section we set up the theory so that Lean's types and functions between them can be viewed as a `LargeCategory` in our framework." So it seems to be proven that there is a Category Lean! https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory/Types.lean https://github.com/leanprover-community/mathlib4/blob/master...

deleted 3y ago
[deleted]
hiker 3y ago
Yes for the fragment of total and noncomputable functions which mathematicians use. For partial functions (which Lean also supports) I think the same arguments hold as for the "Haskell Category".

2pEXgD0fZ5cF 3y ago

Does Lean have something similar to Haskell's List comprehension [1] or some kind of set builder notation for functional programming purposes? [1]: Example: `[x*2 | x <- [1..10]]`

skavi 3y ago
never understood the appeal of this syntax over standard do notation or just fmap.
- nequo 3y ago
  List comprehensions read like math which we know from school. Do notation reads like Haskell which is fine but less accessible to non-Haskellers. Fmap is somewhat less convenient for slightly more complex examples such as [x*y | x <- [1..10], y <- [2,3,5]]
  - sullyj3 3y ago
    For that you'd use Applicative (*) <$> [1..10] <*> [2,3,5] -- or liftA2 (*) [1..10] [2,3,5] Admittedly also not accessible to non-haskellers. But on the other hand, if you're going to learn a language, you ought to learn its idioms at some point.
    - ykonstant 3y ago
      That being said, nequo's request is not unreasonable; given Lean's advanced metaprogramming facilities, their request should be easy to implement. The nice thing nequo's example illustrates is rank polymorphism: list comprehensions work with lists, products of two, three, four,... lists with the same easy notation : `[n-ary function | x_1 <- List_1, ..., x_n <- List_n]`. It is quite nice to have this, especially for complex numerical operations. Note also that unlike Lean 3, in Lean 4 `List` does not inherently implement `Applicative` or `Monad`, so your code cannot work as is.
      - eric-wieser 3y ago

DataDaoDe 3y ago

I’ve been very excited by lean, but every time I try to set things up I get riddled with exceptions, errors, library incompatibilities, lean 3/4 problems. Tuts or documentation that is outdated or just doesn’t work. It has made me wonder, is this just really really alpha software, are they working at a bleeding rate? Idk, but I’ve been enticed multiple times by the promise of lean, maybe I’m just missing some info or should stick it out or just wait until it gets more stable. Anyone have any insight here?

ykonstant 3y ago
Yes, you should expect some frustration, especially if you want to configure things your way. The least painful pipeline should be the following (only follow the instructions at the pages I am listing, as otherwise things may get too confusing): 1) Install lean as a VS Code extension lean4 following : https://leanprover.github.io/lean4/doc/quickstart.html https://leanprover.github.io/lean4/doc/quickstart.html 2) Read about using the build system `lake` here : https://leanprover.github.io/lean4/doc/setup.html https://leanprover.github.io/lean4/doc/setup.html 3) Note that this does not install mathlib4; leave that for later. 4) Start playing around with basic examples in VS Code by reading the beginning sections of https://leanprover.github.io/functional_programming_in_lean/title.html https://leanprover.github.io/functional_programming_in_lean/... 5) If something does not work on break, ask in the Zulip chat; the devs are gathering pain points to improve tooling every day. If this seems too painful, indeed you may want to wait a bit for the tooling to improve.
kmill 3y ago
Re Lean 3/4 problems: the port of mathlib from Lean 3 to Lean 4 just finished this summer, and unfortunately there's still going to be some confusion between the two for a little while! The mathlib community has been working on getting the documentation to all refer to Lean 4 -- if you find anything old please point it out on the Zulip. There's usually someone around who can fix it relatively quickly. I think it's better to think of it as bleeding-edge research software rather than alpha software. There might be a little bit of culture shock if you're used to industry-oriented software, but part of this stable version announcement is that there's a new Lean organization that now has resources to improve the experience.

zone411 3y ago

LeanDojo shows promise in allowing interaction with the proof environment programmatically and through LLMs: https://leandojo.org/ https://leandojo.org/. This NY Times article is a nice overview of AI in math proofs: https://www.nytimes.com/2023/07/02/science/ai-mathematics-machine-learning.html https://www.nytimes.com/2023/07/02/science/ai-mathematics-ma... (https://archive.ph/t0BhD https://archive.ph/t0BhD) Here is a chart of Mathlib's growth: https://leanprover-community.github.io/mathlib_stats.html https://leanprover-community.github.io/mathlib_stats.html

mcshicks 3y ago
LeanDojo looks cool! I will check it out. I did the natural number game in lean 3, and was excited to see the author of "How to Prove it" had written an online book, "How to prove it with Lean" to as an accompaniment to the book, but it was written in lean 4. I decided to redo it in Lean 4 (still working on it) and had some troubles but was super happy with the responses I got on the Zulip Chat. It was a bit tricky to install it but the lake system seems like a big improvement over how I installed lean 3. I used the emacs version of lean mode for lean 4. How to Prove it with lean https://djvelleman.github.io/HTPIwL/ https://djvelleman.github.io/HTPIwL/ Lean 4 Natural Number Game https://adam.math.hhu.de/#/g/hhu-adam/NNG4 https://adam.math.hhu.de/#/g/hhu-adam/NNG4 Lean Zulip Chat https://leanprover.zulipchat.com/ https://leanprover.zulipchat.com/ Emacs lean 4 mode https://github.com/leanprover/lean4-mode https://github.com/leanprover/lean4-mode

agentultra 3y ago

Exciting! I've been picking up some small side projects in Lean again to add more to https://agentultra.github.io/lean-4-hackers/ https://agentultra.github.io/lean-4-hackers/ -- a guide for programmers interested in using it as a programming language. Congrats on the milestone!

ykonstant 3y ago
That's an excellent starting guide, nice!

ykonstant 3y ago

The Lean Zulip chat includes a "Is there code for X" section; you can go there and ask if a specific theorem or research problem has been formalized/verified in Lean, and if not, whether someone is working or intends to work on it. This way you can form impromptu working groups if you find others interested in your problem.