Lean 4.0
github.com
github.com
- 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
[1]: https://leanprover.github.io/functional_programming_in_lean/...
Are people like these not programmers? https://leandojo.org/
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/
I only had a basic knowledge of first-order logic and set theory before reading TPiL4. It wasn't easy, but now I can prove theorems in Lean. By the way, I still can't write a program in any language.
Does Lean have docstrings with embedded markup like Python?
The Python Language Reference: https://docs.python.org/3/reference/
The Python Language Reference > 10. Full Grammar specification: https://docs.python.org/3/reference/grammar.html
LearnXinYminutes > Where X=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#colle...
In Python, they're not interfaces, they're ABCs.
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.
In any case, Lean is a proof formalization and verification language doubling as a general purpose programming language still in its research phase. If you are interested in how this sounds, you can check it out. If not, there is no need.
Regardless it was a rough metric meant to be demonstrative of the level of effort to go through the tutorial.
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/CrossingTheCh...
You can also describe say, the Frankfurt school of critical theory or every other programming language.
A product is an act of production here, as in some kind of process. Even things like classes of clouds and rocks can be described in that framework
I don't expect Lean to be an exception
Also to respond to the idea that I'm fundamentally unworthy of an explanation: I'm also not the target audience for the LHC or James Webb but effort has been made to describe it. They don't demand advanced physics degrees to unveil its purpose like they're some kind of secret society.
> I'm also not the target audience for the LHC or James Webb but effort has been made to describe it.
And there is an effort to describe Lean on their webpage. But I would be curious to know if you would be able to recall the "elevator pitch" you heard for the LHC that doesn't grossly gloss over any kind of relevant actual information. "Customers were dissatisfied because previous colliders were too small, so we made a bigger one. This allows us to hurl particles very fast at each other." Huzzah, you've just been elevator pitched. Do you actually know anything significant about the LHC after that pitch? I sincerely doubt it.
You're also glossing over the fact that the LHC was started in 1998. The James Webb telescope has been in the works since the 90's. Meanwhile, Lean started as a research project in 2013, and Lean 4 is only 1.5 years old. Being angry that scientists have been developing the fundamentals before engaging in outreach is misguided at best.
The LHC example is so simple ChatGPT did it in a single go. Again, this is generative AI
"For particle physics researchers seeking to unravel the cosmos, the Large Hadron Collider (LHC) offers an unparalleled solution. Unlike conventional particle accelerators, the LHC achieves extraordinary collision energies, enabling experiments that mirror the early universe's conditions. This distinctive feature has led to groundbreaking discoveries, notably the Higgs boson. In contrast to other accelerators, the LHC's unmatched power and global scientific network establish it as the premier choice for unlocking the universe's deepest secrets, setting it apart in its capacity to explore uncharted frontiers in particle physics."
In fact, I asked it to do it for Lean and it could do it just fine.
In contrast, the main lean website starts like this:
The Lean (jargon) is a (jargon) developed principally by Leonardo de Moura.
There's this bizarre fetishism for making things inaccessible and then personally belittling and insulting people when they state the obvious.
The other inexplicable behavior is the tendency to give "answers" by pointing to giant manuals that don't answer the question.
This is endemic to ML. Someone asks what say "Vit-L" versus "Vit-H" means and the answer is usually a link to some ~40 page peer reviewed LaTeX that mentions the acronyms but doesn't define it either.
The strategy is to do anything but be transparent and direct.
That's a buzzword soup with barely any actual substance. You're illustrating what I meant. It's also full of jargon (particle accelerators, collision energies, Higgs boson...)
> This is endemic to ML.
Lean and ML are completely unrelated topics.
This is so bad that different fields within the discipline can't even understand each other and they wear that as a badge of honor as if being opaque, uninformative, and misleading people is a natural law they're obligated to follow.
It's a truly bizarre social game. A cycle of gaslighting and abuse as an institution.
I don't know who goes this deep in to these threads so this is mostly for myself.
My primary critique is from a lifelong love of mathematics. I actually hold a few fancy degrees in the subject.
I cannot stand however, power structures for the sake of power structures. The primary reason I left academia and broke away from the field is my, well, disgust really, with how, I believe willfully obtuse things are.
It's not so much how things are stated although there's problems there, it's the relationship dynamics, interactions, and style of expressions.
Before the rise of the term science, math was called a "natural philosophy" and I really have felt that the mathematics community, at least on the west coast, which is what I've experienced, has an accentuated form of the most off-putting characteristics of philosophy including a steadfast refusal and denial to acknowledge it.
I really think it makes what I consider a beautiful field of study to be hostile, insular and needlessly esoteric.
I still care a lot about it and I want it to be healthier and more open.
Lean started as a small research project hidden away within Microsoft Research, and mathematicians learned about it and have built a community by word of mouth. There is no accountability needed at all for the project, and there's no need to advertise it -- that's not to say that there hasn't been any effort put into advertising it to mathematicians. I just advertised the system myself an hour ago during a talk that explained Lean and Mathlib to a group of mathematicians, computer scientists, and linguists.
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 praise Lean's extensible syntax and editor support.
See also: https://leanprover.zulipchat.com/#narrow/stream/113488-gener...
The main difference between most of the examples you list via the Wikipedia page and the examples listed in the URL I cited above is how the computer is being used: in many cases, "computer-assisted" means an ad-hoc program was used to check a bunch of cases which would be too tedious for a human to check. But what happens if there is a bug in the used ad-hoc program (or, e.g., in a linear programming solver)? To increase confidence in the verification result, ideally both the validity of the case-checking and the logic for deducing the main theorem from the checked cases would be verified by a small and general "kernel"/proof checker. This is what theorem provers such as Lean, Coq and Isabelle allow.
def f (n : Nat) : String :=
String.append
(if n % 3 = 0 then "Fizz" else "")
(if n % 5 = 0 then "Buzz" else "")
#eval List.map f (List.range 100)
theorem poop (n : Nat) : f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = "" := by
unfold f
split <;> split
· exact Or.inl rfl
· exact Or.inr (Or.inl rfl)
· exact Or.inr (Or.inr (Or.inl rfl))
· exact Or.inr (Or.inr (Or.inr rfl))Just for comparison, in Typescript you can write:
function f(n:number){
if (n%3==0 && n%5==0) return "FizzBuzz"
if (n%3==0) return "Fizz"
if (n%5==0) return "Buzz"
return "";
}
Then, I can write:
function *iFizzBuzz(steps:number){
for (let i=0; i<steps; i++){
const fb = f(i);
if (fb) yield fb;
}
}
const fizzBuzz100 = Array.from(iFizzBuzz(100));
inductive FizzBuzz where
| fizz
| buzz
| fizzBuzz
| none
def fizzBuzz (n : Nat) : FizzBuzz :=
if n % 15 == 0 then .fizzBuzz
else if n % 3 == 0 then .fizz
else if n % 5 == 0 then .buzz
else .none
instance : ToString FizzBuzz where
toString : FizzBuzz → String
| .none => ""
| .fizz => "Fizz"
| .buzz => "Buzz"
| .fizzBuzz => "FizzBuzz"
def stringFizz (n : Nat) : String :=
toString <| fizzBuzz n
def printFizz (n : Nat) : IO Unit := do
println! s!"{fizzBuzz n}" def f (n : Nat) : String :=
Option.getD
(Option.merge String.append
(if n % 3 = 0 then "Fizz" else none)
(if n % 5 = 0 then "Buzz" else none))
(toString n)
#eval List.map (fun k => f (k + 1)) (List.range 100)
theorem poop (n : Nat) :
f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = toString n := by
unfold f
split <;> split
· exact Or.inl rfl
· exact Or.inr (Or.inl rfl)
· exact Or.inr (Or.inr (Or.inl rfl))
· exact Or.inr (Or.inr (Or.inr rfl))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]]`
[x*y | x <- [1..10], y <- [2,3,5]] (*) <$> [1..10] <*> [2,3,5]
-- or
liftA2 (*) [1..10] [2,3,5]
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.
It's not rocket science why someone would ask this. I don't always use list comprehensions. But sometimes I do. They have open arity and the syntax doesn't as often require things like parenthesis to handle fixity conflicts between other (non-applicative) operators. They are asking about list comprehensions, just because they think it's nice. It is a very simple question and talking about applicative is irrelevant.
(. * 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)
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)]
(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...
[1] https://github.com/leanprover-community/mathlib4/tree/master...
[2] https://leanprover-community.github.io/blog/posts/lte-final/
and there is Subobject, which looks like the subobject classifier.
https://github.com/leanprover-community/mathlib4/blob/master...