from Hacker News

Lean 4.0

by quag on 9/8/23, 5:59 AM with 91 comments

  • by Gys on 9/8/23, 7:21 AM

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

  • by zone411 on 9/8/23, 1:18 PM

    LeanDojo shows promise in allowing interaction with the proof environment programmatically and through LLMs: 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-ma... (https://archive.ph/t0BhD)

    Here is a chart of Mathlib's growth: https://leanprover-community.github.io/mathlib_stats.html

  • by agentultra on 9/8/23, 1:23 PM

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

    Congrats on the milestone!

  • by koito17 on 9/8/23, 9:03 AM

    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.

  • by ykonstant on 9/8/23, 1:25 PM

    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.

  • by garfieldnate on 9/13/23, 4:15 PM

    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/, 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).

  • by hackandthink on 9/8/23, 6:40 AM

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

  • by kristopolous on 9/8/23, 9:07 AM

    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

      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.

  • by DataDaoDe on 9/8/23, 1:18 PM

    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?

  • by 2pEXgD0fZ5cF on 9/8/23, 10:37 AM

    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]]`

  • by hackandthink on 9/8/23, 9:45 AM

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

  • by harel on 9/8/23, 9:08 AM

    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.

  • by taliesinb on 9/8/23, 8:09 AM

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