Mathematics for the 21st Century: An Introduction to Logic and Proof using Spaced Repetition and an Interactive Theorem Prover

The introduction to math I wish I had 10 years ago while I was in school

Welcome to "Mathematics for the 21st Century". This is the introduction to math I wish I had 10 years ago while I was in school. The goal of the series is to gain enough math knowledge in a few fundamental areas that we can just learn whatever we want without getting bogged down by not understanding basic things like how to do a proof.

This is a Substack page linking to all of the chapters in the series which were written and published as shared documents through the spaced repetition app RemNote. You don’t need to sign up or pay a single penny to view any of the material or exercises in this series! It’s all free and can be completed in any note-taking app or spaced repetition system, it’s just more convenient to do it in RemNote because I wrote a plugin adding support for the Lean theorem proving language to RemNote.

There are a few things which will distinguish this series from other intro to logic and proof courses and books.

The first is that we are going to learn how to turn math knowledge and proofs into flashcards and review them using spaced repetition. Every part of the series comes with pre-made flashcards and you'll learn how to create your own from scratch too. This is going to make the learning process 10x easier and by the end of the series you will have theorems and proofs at the tips of your fingers! The note-taking and spaced repetition app I will use in this series is RemNote, but you can use a different app, like Anki or just pen and paper if you prefer. Everything is free by the way, so anyone who wants to learn some math can follow along!

Secondly we are going to be using an interactive theorem proving language called Lean. Lean is a programming language for math which will function as a digital math tutor giving us instantaneous feedback on our proofs. Lean turns math into a game and gives you a bulletproof understanding of the rules of proof. I built a plugin which allows you to write Lean code inside RemNote and created templates for all of the exercises so you don't have to mess around setting up any software or learning the intricacies of the Lean programming language, you can just immediately start learning.

My hope is that after finishing this series math will become an open world RPG where you have complete freedom to explore and follow your interests. The material we'll cover is very general foundational stuff which will apply to whatever you decide to study next. The series covers roughly what you would expect to see in a first year intro to proof course at university with some additional material related to spaced repetition, flashcards and meta-learning.

Chapters

• What is Logic? History and Motivation: “In the history of logic there is one philosopher whose name stands above all others. Not only did he make significant contributions to natural science, philosophy and politics, but he also founded the field that would later go on to change the world more than any other by giving rise to computers, the internet and artificial intelligence…“

• Intro to Propositional Logic: “Today we are going to review each of the basic Logical Connectives to make sure you are familiar with them before we move on to doing proofs…”

• Intro to Proof: “Today we are going to do our first simple proof and learn how to use the Lean theorem proving language to check that it's correct…”

• Logic and Deduction: “Last time we learned about Proof and Proof Systems. We also did our first proof and checked it with the Lean theorem proving language! We are ready to learn more about Natural Deduction and gain more experience doing proofs…”

• How to Create Good Math Flashcards: Proofs: “In this article, I want to explain how to turn the proofs we have done so far into flashcards that you can review with spaced repetition to keep them fresh in your memory over time. We'll cover the theory behind flashcard formulation, common mistakes people make and more…”

• More Logic and Deduction: “We already learned many of the fundamental inference rules in natural deduction. Today we will learn a few more…”

• Classical Reasoning: “All of the rules of inference we have learned so far are part of ‘constructive’ logic. Today we are going to extend our system with new rules which come under the name of "classical" logic…”