An introduction to formal real analysis (Lecture 1: The story of real analysis. Lean tactics (exact, rfl, rewrite, ring_nf, use, intro, specialize, choose)). ~ Alex Kontorovich. https://alexkontorovich.github.io/2025F311H/Lecture1.pdf #ITP #LeanProver #Math