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.

Online textbook: Mathematics in Lean by Jeremy Avigad and Patrick Massot

Setting up a Lean environment

• 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.

Additional Lean resources

• Theorem Proving in Lean 4 by Jeremy Avigad, Leonardo de Moura, and Soonho Kong
• Mathlib4 documentation.
• Lean community resources including math courses using Lean
• Search tools for Lean: Loogle, Moogle, and LeanSearch. They can be used within a VS code.
• Lean tactic cheatsheets: Lean community, Buzzard
• Mathlib naming conventions
• Join the Lean community Zulip.
• Play the Natural Number Game (by Kevin Buzzard and Mohammad Pedramfar).

Homework

There will be weekly homework assignments. Homework assignments should be submitted on Canvas by class time on Monday.

• Homework 1, hw1.lean, due Apr 7 at 10:30 am.

Group projects

• 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 3: Decide on the members of your group.
  • By end of week 4, 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 membres.
  • 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.