- 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.
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
How to Prove it with lean https://djvelleman.github.io/HTPIwL/ Lean 4 Natural Number Game https://adam.math.hhu.de/#/g/hhu-adam/NNG4 Lean Zulip Chat https://leanprover.zulipchat.com/ Emacs lean 4 mode https://github.com/leanprover/lean4-mode
Congrats on the milestone!
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.
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) as a starting point.
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).
https://github.com/blanchette/logical_verification_2023
The hitchhiker's guide
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
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}"
$ find leanprover.github.io/functional_programming_in_lean -name \*.html -exec html2text {} \; | wc -w
271248
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.
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
2) Read about using the build system `lake` here : 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/...
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.
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.
[1]: Example: `[x*2 | x <- [1..10]]`
do let x ← List.range' 1 10; return x^2
macro "[" r:term "|" preamble:doElem "]" : term => `(do
$preamble; return $r)
#eval [x^2 | let x ← List.range' 1 10] declare_syntax_cat compClause
syntax "for " term " in " term : compClause
syntax "if " term : compClause
syntax "[" term " | " compClause,* "]" : term
macro_rules
| `([$t:term |]) => `([$t])
| `([$t:term | for $x in $xs]) => `(List.map (λ $x => $t) $xs)
| `([$t:term | if $x]) => `(if $x then [$t] else [])
| `([$t:term | $c, $cs,*]) => `(List.join [[$t | $cs,*] | $c])
#eval [x+1| for x in [1,2,3]]
-- [2, 3, 4]
#eval [4 | if 1 < 0]
-- []
#eval [4 | if 1 < 3]
-- [4]
#eval [(x, y) | for x in List.range 5, for y in List.range 5, if x + y <= 3]
-- [(0, 0), (0, 1), (0, 2), (0, 3), (1, 0), (1, 1), (1, 2), (2, 0), (2, 1), (3, 0)]
(. * 2) <$> [1,2,3]
def byTwo (inputList : List Nat) :=
(. * 2) <$> inputList
#eval byTwo [1, 2, 3]
-- [2, 4, 6]Why not? I was curious, Haskell is the functional language I know. Lean is the language I do not know.
Since Lean leans even heavier towards mathematics, set builder style notation seems like a natural fit. Now whether or not such notation is actually needed or worth it, that is a whole different question.
I think you'll usually see
def byTwo (inputList : List.Nat) := inputList.map (. \* 2)
[x*y | x <- [1..10], y <- [2,3,5]](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...
https://github.com/leanprover-community/mathlib4/tree/master...