Disclaimer: All information appearing below is subject to revision until the first lecture. Given the experimental nature of the course, there might be some minor revisions even after that.
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. But this subject moves fast and so there will be many new things to discuss!
Although it is possible to use Lean from a virtual environment such as GitHub Codespace or the Lean 4 Web calculator, it is strongly recommended that you install it locally on your machine via VSCode. Here are instructions for doing so.
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 lecture on Monday, April 20 or Friday, May 15. Lectures will be livestreamed over Zoom and recorded; both the livestream and the recording are accessible via Zulip (see below).
Office hours: Kedlaya: Mon 12-1pm, APM 7202 and Thu 6-7pm, online; Liao: Thu 1-3pm, HSS 3044; Qu: Tu 4-6pm, HSS 3044. Note: I am bad with names, so I will probably ask for a reminder when you come to office hours.
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 please indicated 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; instead, there will be a final project due at the end of week 10 (see below).
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:
| Percentage | 97 | 93 | 90 | 87 | 83 | 80 | 77 | 73 | 70 |
| Minimum grade | A+ | A | A- | B+ | B | B- | C+ | C | C- |
AI policy: AI (academic integrity) matters even in the age of AI (artificial intelligence)! While you are encouraged to make thoughtful use of AI tools during the course, you must cite all sources (including collaborators, static websites, LLMs, etc.) and retain logs of all relevant chatbot transcripts; we reserve the right to request these transcripts.
Violations of AI policy include plagiarism, bullying, harassment, or inappropriate behavior. This covers both in-person settings and online spaces.
Recommendations: Many students ask me for letters of recommendation after taking one of my classes. For a class of this size, I cannot agree to write a meaningful letter based solely on participation in this class. See this page for more advice.