Upper level undergraduate math course, Johns Hopkins University, 2021
This course introduces students to the natural deduction style of encoding proofs in intuitionistic propositional logic and first order logic. Proof strategies such as proof by cases, negation introduction, proof by contradiction, induction, etc are justified by natural deduction. Later, students are familiarized with proofs on abstract mathematical structures such as finite and infinite sets, ordered sets, metric spaces, and topological spaces. They are introduced to methods of writing proofs which are rigorous, readable, and elegant. Mathematical communication, both written and spoken, is emphasized throughout the course. In this course, students also explore proof-relevant mathemetics by interacting with the Lean proof assistant.