Syllabus: This course will explore how mathematical theorems can be formalized in the interactive theorem
prover Lean. We will focus on topics in undergraduate mathematics such as set theory, logic, functions, induction,
number theory, and other topics typically encountered in Math 300: Introduction to Mathematical Reasoning. For each
topic, we will review the mathematical foundations, and then attempt to formalize main theorems and exercises. As
the course progresses, we will learn more and more sophisticated high-level tactics that can help automate the
formalization. By the end of the quarter, we will have group projects, where each group chooses a mathematical
statement to formalize, depending on the interests of the students.
Install a Lean 4 environment on your computer with VS Code: follow the directions
here.
Follow the instructions in Section 1.1 "Getting Started" in Mathematics in Lean to download the
"mathematics_in_lean" repository which you should be able to view in VS Code.
A major component of this course will be group projects. In teams of 2-4 students, you will choose a
mathematical statement to formalize, depending on your mathematical interests, and you will formalize it
in Lean.
Schedule:
Weeks 1-3: discussions of possible group projects
By end of week 4: Pick a group project and decide on the members of your group.
By end of week 5, submit a short proposal (1-2 pages) of your group project. This should include the
precise mathematical statements that you aim to formalize, and a roadmap of how the result will be
formalized. Include a division of labor among the group members.
Weeks 5-9: some of class time will be devoted to group work but you are also expected of course to work
together with your group outside of class.
Week 10: Each group will give a 30 minute presentation of their project and submit their project for
review (ideally using a public github repository).
Grading
Homework: 50%
Final presentation: 50%
Course policies
AI-based tools:
In this course, students are permitted to experiment with AI-based tools (such as ChatGPT and Github Copilot).
However, the Lean code for the homework assignments should be written without using AI assistants.
(The formalization problems in our homework are very likely included in the training data for most large
language models, so that these AI-based tools can simply regurgitate the correct solution.) On the other hand,
students are permitted to use AI-based tools in the group assignment.
All sources, including AI tools, must be properly cited. Use of AI in ways that are inconsistent with the
parameters above will be considered academic misconduct and subject to investigation.
Please note that AI results can be biased and inaccurate. It is your responsibility to ensure that the
information you use from AI is accurate. Additionally, pay attention to the privacy of your data. Many AI tools
will incorporate and use any content you share, so be careful not to unintentionally share copyrighted
materials, original work, or personal information.
Learning how to thoughtfully and strategically use AI-based tools may help you develop your skills, refine your
work, and prepare you for your future career. If you have any questions about citation or about what constitutes
academic integrity in this course or at the University of Washington, please feel free to contact me to discuss
your concerns.
Religious accommodation:
Washington state law requires that UW develop a policy for accommodation of student absences or significant
hardship due to reasons of faith or conscience, or for organized religious activities. The UW’s Reglious
Accommodation Policy, including more information about how to request an accommodation, is available here.
Accommodations must be requested within the first two weeks of this course using the Religious Accommodations
Request form.
Student disability resources: UW offers disability accommodations. If you have already established
accommodations with Disability Resources for Students (DRS), please communicate your approved accommodations to
me at your earliest convenience so we can discuss your needs in this course.
If you have not yet established services through DRS, but have a temporary health condition or permanent
disability that requires accommodations (conditions include but not limited to; mental health,
attention-related, learning, vision, hearing, physical or health impacts), you are welcome to contact DRS at
206-543-8924 or uwdrs@uw.edu or disability.uw.edu. DRS offers resources and coordinates reasonable
accommodations for students with disabilities and/or temporary health conditions.
Student conduct code:
The University of Washington Student Conduct Code (WAC 478-121) defines prohibited academic and behavioral
conduct and describes how the University holds students accountable as they pursue their academic goals.
Allegations of misconduct by students may be referred to the appropriate campus office for investigation and
resolution. More information can be found online here.