Upper level undergraduate math course, Johns Hopkins University
This course introduces you to the the language of mathematics and the methods of mathematical proofs. We learn the rules of logic whereby we identify strategies for proving mathematical statements based on their logical structures. We will then learn about some elementary aspects of number systems, sets, functions, relations, inductive types (such as lists, trees, graphs), algebraic structures, and metric spaces. As we learn these topics, we teach our computers every piece of mathematics we learn, that is we learn mathematics by formalizing it in Lean interactive proof assistant. Formalization can be seen as a kind of computer programming: we will write mathematical definitions, theorems, and proofs in a language that Lean can understand. In return, Lean provides instant feedback, helps us with writing our proofs and ultimately certifies the correctness of our proofs.
This course does not have any mathematical prerequisite, however, it is expected that you are familiar with basic high-school algebra. Although a basic programming experience can go far toward your excelling in this course, we actually don’t presuppose any background in formalization or in programming.
Copyright (c) 2022 Sina Hazratpour. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE.