Solving mathematical puzzles with proof-assistant Lean

Learn how to use an advanced programming language to solve mathematical puzzles and verify them.

• Introduction to the mathematical proof assistant and programming language Lean4.
• Introduction Mathlib, the standard library for Lean.
• Practice Lean by solving and analyzing riddles from the Riddle Repository.