This repo is served as notes for Lean 4 minicourse series taught by me in Dept of Math @ NUS. The object for this series is to get students handed on with Lean 4 and start to formalize things of their interests within fastest possible time. For this purpose, unlike Mathematics in Lean, the design of learning process is more 'practical' rather than 'structured'. For example, I will not avoid powerful tactics for high-level automation in the first place. And theorems and lemmas will be introduced progressively and more based on their day-to-day frequency.
This course also featuring various LLM tools, such as LeanSearch, Auto-formalizer, and step-prover. I will try my best to combine these tools in my teaching.
Chapter 1: Introduction and Basic Syntax Chapter 2: Advanced Tactics Chapter 3: Structures and Organizations