Active participation is essential for success in this course. Students are expected to attend all classes, contribute to discussions, and engage in collaborative activities. This includes asking questions, sharing insights, and working effectively during in-class exercises or group work.
Constructive engagement allows students to deepen their understanding of the material, learn from their peers, and build essential problem-solving and communication skills that will be valuable in future coursework and careers.
Homework assignments are a critical component of the course. They are designed to reinforce the concepts covered in lectures and provide hands-on experience using Lean. Assignments will include a mix of logical proofs, programming tasks, and conceptual exercises. Solutions must be submitted on time and will be graded for clarity and correctness. Collaboration is encouraged, but each student must submit their own work.
Projects are a significant component of the course, giving students the opportunity to apply their knowledge to formalize and verify mathematical or computational concepts in Lean. These projects will build problem-solving skills, encourage creativity, and allow students to explore the potential of interactive theorem proving. Both the midterm and final projects will be evaluated based on technical accuracy, clarity of exposition, creativity, and teamwork.
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.
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.
Quizzes will be administered periodically to assess understanding of key concepts and ensure students are keeping up with the material. These will be short, focused assessments designed to reinforce learning and identify areas for improvement. Quizzes may include logical proofs, questions about Lean syntax, or problem-solving tasks. They are an opportunity to practice applying course concepts and receive feedback on your progress.