Syllabus Math 587 – 001 – Spring 2025

Students will work in small groups to formalize a specific problem or proof in Lean. The midterm project will focus on a foundational topic, with structured guidance provided to ensure students develop proficiency in key skills.

Graduate students will take responsibility for guiding a group through each stage of the process. This includes helping the team evaluate the provided problems, select one to work on, and translate it intro Lean code. Graduate students will organize the development of the proof, ensuring all necessary definitions, lemmas, and arguments are included. They will provide technical guidance, troubleshoot challenges, and ensure that all group members contribute equitably. Additionally, they are responsible for managing milestones and ensuring the submission of a polished, well-documented Lean file.

Graduate students are responsible for researching and proposing a final project topic, which must involve advanced applications of interactive theorem proving. The proposal should outline a relevant, feasible, and impactful project topic, incorporating instructor feedback to refine ideas.

The final project will allow students to choose from a list of complex problems that align with their interests and demonstrates their mastery of course material. Projects will require students to design and implement creative solutions, formalize their work in Lean, and present their work to the class.

Graduate students will be responsible for assembling a team to executing the project, ensuring collaboration and effective contributions from all members. Team leaders are responsible for ensuring completion of a comprehensive Lean formalization, and a detailed write-up and presentation explaining the problem, approach, and broader implications of the work.