§ About the course

This course is derived from the 18.100A: Real Analysis material developed by the MIT math department during the Covid pandemic in 2020. The lectures were given by Casey Rodriguez, who is now an assistant professor at UNC at Chapel Hill.

MIT OpenCourseWare hosts the original material, including video lectures, lecture notes, readings, recitations, assignments and exams which are licensed under the creative commons CC BY-NC-SA 4.0

This course is a remix of 18.100A. It includes additional exercises and solutions that use the Lean4 proof assistant. This means we now have a way to learn real analysis on our own and still be confident that the proofs we build are correct.

§ Prerequisites

Multivariable Calculus.

MITxOnline

The prerequisite for the Lean component is:

The Mechnics of Proof
by Heather MacBeth

However, if you are just getting started with proving in lean, then you should definitely start with the following browser games:

The Natural Number game
by Kevin Buzzard, Jon Eugster, Sian Carey, Ivan Farabella, Archie Browne.

The Set Theory game
by Daniel J. Velleman

§ Setup

This course uses some free books. The primary text is:
Basic Analysis I, version 6.0, by Jiří Lebl.

Some recommended readings will be selected from: Mathematics for Computer Science

As for installing the lean proof assistent .. Hey! Wait a second! You already have it installed, right?! AHEM, (please see prerequisites). You really need to work through those prereqs because this course builds on those skills and simultaneously introduces real analysis.

If you're ready, then it's time to sharpen your pencils and keyboards, grab some toast and a hot beverage.

Onto Lecture 1!