- 2
- 3 315
MathPom
United States
เข้าร่วมเมื่อ 3 ต.ค. 2022
PomMath is a math channel with a computational flavor. It will feature videos both for beginners and people who have experience with math & programming.
If you like food, go check out our food channel: KylaPom.
If you like food, go check out our food channel: KylaPom.
Introductory Proof with Lean 4 - Natural Numbers
Follow along as I learn how to use an automated proof system, Lean 4. We'll do an introductory proof involving natural numbers using Lean's calculational proof mode.
Timecodes:
00:00 - Intro
00:34 - Let's Jump In
01:17 - Variables in Lean
01:34 - How to Read a Type Signature
02:56 - Writing a Theorem
05:00 - Function Application in Lean
05:10 - congrArg
07:25 - Nat.add_comm
08:30 - How to Read a Calculational Proof
09:19 - Eq.symm
10:35 - Typechecking a Theorem
11:00 - Calculational Proof Function Representation
11:35 - Outro
Here are some resources I found helpful when making this video:
leanprover.github.io/theorem_proving_in_lean4/
leanprover.github.io/lean4/doc/
leanprover.github.io/functional_programming_in_lean/getting-to-know/functions-and-definitions.html
leanprover.github.io/logic_and_proof/index.html
leanprover.github.io/tutorial/A1_Quick_Reference.html
I used the following elements in this video/thumbnail:
By Joey-das-WBF at English Wikipedia - Transferred from en.wikipedia to Commons by Common Good using CommonsHelper., Public Domain, commons.wikimedia.org/w/index.php?curid=16472083
leanprover.github.io/images/lean_logo2.svg
editor.codecogs.com
unsplash.com/photos/U8kNV-0dCS0
#leanprover
Timecodes:
00:00 - Intro
00:34 - Let's Jump In
01:17 - Variables in Lean
01:34 - How to Read a Type Signature
02:56 - Writing a Theorem
05:00 - Function Application in Lean
05:10 - congrArg
07:25 - Nat.add_comm
08:30 - How to Read a Calculational Proof
09:19 - Eq.symm
10:35 - Typechecking a Theorem
11:00 - Calculational Proof Function Representation
11:35 - Outro
Here are some resources I found helpful when making this video:
leanprover.github.io/theorem_proving_in_lean4/
leanprover.github.io/lean4/doc/
leanprover.github.io/functional_programming_in_lean/getting-to-know/functions-and-definitions.html
leanprover.github.io/logic_and_proof/index.html
leanprover.github.io/tutorial/A1_Quick_Reference.html
I used the following elements in this video/thumbnail:
By Joey-das-WBF at English Wikipedia - Transferred from en.wikipedia to Commons by Common Good using CommonsHelper., Public Domain, commons.wikimedia.org/w/index.php?curid=16472083
leanprover.github.io/images/lean_logo2.svg
editor.codecogs.com
unsplash.com/photos/U8kNV-0dCS0
#leanprover
มุมมอง: 3 133
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!
4:51 when she applies the succ to both sides of the equality 😩
I'm not sure I understand... can you further explain?
I love the way this started! How do you only have 89 subs!?
thank you! that intro took quite a while to make!
lean sucks
I really like your calm voice and your pace ! Kudos
Thank you!
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.
Good job! Keep’em coming!
Thanks! Will do!
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
Moar please. Moar Lean 4 videos. On any Lean 4 topic.
great vid, very chill too
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.
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".
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.
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!
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.