Summary and warning: Although the course catalog does not (yet) reflect this, this will be a radically different course than previous versions of Math 157, focusing on the burgeoning topic of mathematical formalization and the tools used in this subject, especially the Lean proof assistant and its associated MathLib library. One side effect is that, while Math 109 is not a formal prerequisite, it is strongly recommended as at least a corequisite.
As a loose model for the structure of the course, we will use this course taught by Jarod Alper at U. Washington in spring 2025.
All information appearing below is subject to revision until the first lecture.
Instructor: Kiran Kedlaya, kedlaya [at] ucsd [etcetera].
TAs: Yuan Liao (y2liao [at] ucsd [etcetera]), Haotian Qu (haqu [at] ucsd [etcetera]).
Lectures: MWF 11:00-11:50am in Center 109. No lectures on the following university holidays: Monday, May 25 (Memorial Day). Also, no lectures on Monday, April 20 or Friday, May 15. Lectures will be recorded and made available via Zulip (see below).
Sections: Tue 4:00-4:50pm, 5:00-5:50pm, 6:00-6:50pm, or 7:00-7:50pm in APM 2402. You may attend any section; however, students attending their registered section have priority in case the room is full.Office hours: TBA.
Communication: All communication regarding the course will take place on the Zulip platform; we will not be using Canvas. An invite link to Zulip will be sent to all enrolled students. You must use your UCSD email address to sign into Zulip, but you may use your preferred name and pronouns.
Prerequisites: MATH 18 or MATH 20F or MATH 31AH and a course with programming content in one of C, C++, Java, Python, or R. Acceptable courses include BILD 62, COGS 18, CSE 5A, CSE 6R, CSE 8A, CSE 11, DSC 10, ECE 15, ECE 143, or MATH 189; if the course you wish to use is not listed here, contact the instructor directly. Also, MATH 109 is strongly recommended as a prerequisite or corequisite.
Final exam: None; there will be a final project instead.
Text: No required text. In lieu of a textbook, we will refer frequently to the tutorial Mathematics in Lean. If you have not taken Math 109, I would strongly recommend as prereading Macbeath's Mechanics of Proof for a Lean-based introduction to mathematical proof techniques.
Grading: TBA.