Examples for mathematical theories in lean4 (commented in Japanese).
- Cantor's Theorem
- Fibonacci sequence
$\sqrt{2} \not\in \mathbb{Q}$ - AC
$\implies$ LEM - Basic properties of combination and the binomial theorem
lean: 4.0.0-nightly-2023-03-09 (TODO: fix version)