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_...
leanprover.github.io/lean4/doc/
leanprover.github.io/function...
leanprover.github.io/logic_an...
leanprover.github.io/tutorial...
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...
leanprover.github.io/images/l...
editor.codecogs.com
unsplash.com/photos/U8kNV-0dCS0
#leanprover

[@kemijarks]

I really like your calm voice and your pace ! Kudos

[@acortis]

Good job! Keep’em coming!

[@alfonsobustamante6937]

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!

[@mathpom]

Thank you for the kind comment! I deliberately tried to keep the example simple.

[@alfonsobustamante6937]

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 🎭

[@mathpom]

ha call anytime!

[@bobvance9519]

great vid, very chill too

[@mohamedtalaatharb2441]

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.

[@mathpom]

Thank you -- I'm glad it was helpful.

[@phurisottatipreedawong1618]

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.

[@davidstainton8337]

Moar please. Moar Lean 4 videos. On any Lean 4 topic.

[@marcourielmedinamandujano5872]

But how do I install lean? :(((

[@mathpom]

It's not too bad! Check out leanprover-community.github.io/install/linux.html and github.com/leanprover/elan.

[@andresgoens]

Oops, Lean is not automated :/ Lean is an interactive theorem prover. Nice style for the video otherwise!

[@mathpom]

good catch! I shouldn't have used a term with specific meaning. I meant more the tactics people can get "for free".

[@feraudyh]

I find the equating of function and theorem a little off-putting.