Sign up to save your podcasts
Or
Share Is This the End of Handwritten Math? Introducing Lean
Share to email
Share to Facebook
Share to X
Share to email
Share to Facebook
Share to X
Or
Is This the End of Handwritten Math? Introducing Lean
A first guide to the Lean 4 Proof Assistant.
To learn for free on Brilliant, go to https://brilliant.org/AnkYog . You’ll also get 20% off an annual premium subscription.
You can try out Lean at Lean 4 Web: https://live.lean-lang.org/ (no installation required)
The code for the video is given at https://github.com/AnkYog/LeanTutorial1
You can copy this code into Lean 4 Web to follow along the video.
Learning Lean 4: https://leanprover-community.github.io/learn.html
Proof assistants are insane -
Errors that might take months to find can be done in minutes.
Math problems become open-source projects as anyone can contribute verified math code.
AIs now have an environment to learn and generate verified math proofs.
This video is the ultimate tutorial on the Lean 4 proof assistant.
By the end, we’ll be able to formalize these three big proofs:
This video was sponsored by Brilliant.
Twitter: https://twitter.com/ank_yog
00:00 Intro
00:46 Basic Syntax
01:41 Prop-as-Types
03:28 Tactic Mode
04:09 Mathlib
07:00 Intro and Elim Rules
08:52 Proof: 10 is even
09:43 Proof: If a number is even, 2 divides it
12:53 Define PrimeNum
13:19 Proof: 1 is not prime
14:18 Proof: 9 is not prime
16:01 Proof: 5 is prime
19:37 Final 3 Proofs
20:01 Irrational to the power Irrational can be Rational
24:44 There exist infinite primes
31:22 Every onto (surjective) function has a right inverse
34:21 End
View all episodes
By A first guide to the Lean 4 Proof Assistant.
To learn for free on Brilliant, go to https://brilliant.org/AnkYog . You’ll also get 20% off an annual premium subscription.
You can try out Lean at Lean 4 Web: https://live.lean-lang.org/ (no installation required)
The code for the video is given at https://github.com/AnkYog/LeanTutorial1
You can copy this code into Lean 4 Web to follow along the video.
Learning Lean 4: https://leanprover-community.github.io/learn.html
Proof assistants are insane -
Errors that might take months to find can be done in minutes.
Math problems become open-source projects as anyone can contribute verified math code.
AIs now have an environment to learn and generate verified math proofs.
This video is the ultimate tutorial on the Lean 4 proof assistant.
By the end, we’ll be able to formalize these three big proofs:
This video was sponsored by Brilliant.
Twitter: https://twitter.com/ank_yog
00:00 Intro
00:46 Basic Syntax
01:41 Prop-as-Types
03:28 Tactic Mode
04:09 Mathlib
07:00 Intro and Elim Rules
08:52 Proof: 10 is even
09:43 Proof: If a number is even, 2 divides it
12:53 Define PrimeNum
13:19 Proof: 1 is not prime
14:18 Proof: 9 is not prime
16:01 Proof: 5 is prime
19:37 Final 3 Proofs
20:01 Irrational to the power Irrational can be Rational
24:44 There exist infinite primes
31:22 Every onto (surjective) function has a right inverse
34:21 End