An introduction to formal real analysis (Lecture 2: Newton's computation of π. Formal definition of the limit of a sequence). ~ Alex Kontorovich. https://alexkontorovich.github.io/2025F311H/Lecture2.pdf #ITP #LeanProver #Math