The best tutorial on Lean ive seen so far. So clear and loved the fact that i wasnt needed to use any library, which really alouded to grasp the main concepts to set a theorem with its hypothesies and its variables. Thank you!
That is a new mode for proofs that i didn't know about, I almost exclusively use tactics mode but this one seems nice for simple calculations. Thank you for the video.
I’m working on an educational project where I plan to use Manim and/or Matplotlib (in Python) to visualize basic Real Analysis theorems verified by the Lean prover. I’m new to Lean and haven’t found many beginner-friendly tutorials. Since I am only familiar with Python, I would greatly appreciate any advice on how to get started with Lean or resources that can help me integrate Lean with Python visualization tools like Manim and Matplotlib. Additionally, I’m looking for guidance on a suitable folder structure for a Lean project. P.S. Thank you very much for your video and for reading my comment.
do you mean you'd prefer if I highlight that using the "theorem" keyword implies the function is not used for computation? from Functional Programming in Lean: "Generally speaking, with a proof, what matters is that there is evidence that a proposition is true, but it's not particularly important which evidence was provided. With definitions, on the other hand, it matters very much which particular value is selected-after all, a definition of addition that always returns 0 is clearly wrong." The book also shows the equivalence of: def onePlusOneIsTwo : 1 + 1 = 2 := rfl and def OnePlusOneIsTwo : Prop := 1 + 1 = 2 theorem onePlusOneIsTwo : OnePlusOneIsTwo := rfl
this is so calm to watch
pls keep doing these! it was really simple to understand and follow!
Thank you -- I'm glad it was easy to understand!
I love the way this started! How do you only have 89 subs!?
thank you! that intro took quite a while to make!
The best tutorial on Lean ive seen so far. So clear and loved the fact that i wasnt needed to use any library, which really alouded to grasp the main concepts to set a theorem with its hypothesies and its variables. Thank you!
Thank you for the kind comment! I deliberately tried to keep the example simple.
I really like your calm voice and your pace ! Kudos
Thank you!
And by the way, loved the saul goodman style of opening of your video! So i know who i gonna call to defend my math statements and theorems 🎭
ha call anytime!
That is a new mode for proofs that i didn't know about, I almost exclusively use tactics mode but this one seems nice for simple calculations. Thank you for the video.
Thank you -- I'm glad it was helpful.
4:51 when she applies the succ to both sides of the equality 😩
I'm not sure I understand... can you further explain?
Good job! Keep’em coming!
Thanks! Will do!
I’m working on an educational project where I plan to use Manim and/or Matplotlib (in Python) to visualize basic Real Analysis theorems verified by the Lean prover. I’m new to Lean and haven’t found many beginner-friendly tutorials. Since I am only familiar with Python, I would greatly appreciate any advice on how to get started with Lean or resources that can help me integrate Lean with Python visualization tools like Manim and Matplotlib. Additionally, I’m looking for guidance on a suitable folder structure for a Lean project.
P.S. Thank you very much for your video and for reading my comment.
great vid, very chill too
Moar please. Moar Lean 4 videos. On any Lean 4 topic.
Oops, Lean is not automated :/ Lean is an interactive theorem prover. Nice style for the video otherwise!
good catch! I shouldn't have used a term with specific meaning. I meant more the tactics people can get "for free".
But how do I install lean? :(((
It's not too bad! Check out leanprover-community.github.io/install/linux.html and github.com/leanprover/elan.
I find the equating of function and theorem a little off-putting.
do you mean you'd prefer if I highlight that using the "theorem" keyword implies the function is not used for computation?
from Functional Programming in Lean:
"Generally speaking, with a proof, what matters is that there is evidence that a proposition is true, but it's not particularly important which evidence was provided. With definitions, on the other hand, it matters very much which particular value is selected-after all, a definition of addition that always returns 0 is clearly wrong."
The book also shows the equivalence of:
def onePlusOneIsTwo : 1 + 1 = 2 := rfl
and
def OnePlusOneIsTwo : Prop := 1 + 1 = 2
theorem onePlusOneIsTwo : OnePlusOneIsTwo := rfl
lean sucks