The presentation component of the course has been replaced by a Lean project. You will contribute approximately 100 lines of proof to the class's Lean library. You may work alone or in a group of two. Groups of three require permission.
Follow the Lean project setup instructions to set up the project and learn how to submit your work.
Possible projects
- Prove strong induction using ordinary induction.
- Prove the division algorithm.
- Prove Fermat's little theorem.
- Prove unique factorization of (positive) natural numbers into primes.
- Prove the effectiveness of the Euclidean algorithm.
- Prove cancellation laws for addition and for multiplication by a nonzero natural number.
- Prove that the square root of 2 is irrational.
- Classify the integers whose square roots are rational.
- Prove the Cantor–Schröder–Bernstein theorem.
- Prove Euclid's lemma relating irreducible and prime numbers.
- Classify Pythagorean triples.
- Prove the pigeonhole principle and some of its applications.
- Compare the cardinalities of infinite sets.
- Prove Cantor's theorem on cardinalities.
- Prove that the Ramsey number R(3, 3) is 6.
- Count the subsets and multisubsets of an n-element set.
- Prove the handshake lemma and use it to solve the Königsberg bridges problem.
- Count subsets and multisubsets of specified sizes.
- Construct new number systems (integers, rationals, reals, complexes, finite fields, ...) and their arithmetic.