During the semester, I will post homework related to the lecture's topics. Completing these exercises is a great way to get exposure on the different notions you can choose to formalize in your projects.
At the end of the lecture phase, you are expected to submit the homework that you have completed. This is worth 15% of your final grade. I will take the average of your 15 best solutions that you submitted. (Note: Most exercises will be graded in a binary fashion.) Generally speaking, you should get your point if:
- Lean accepts your proof
- You didn't change the imports or the statement of the exercise
- You followed the exercise's specific instructions (if there are any)
If you have any question about the exercises, please ask on Zulip. If you put your solutions to the homework online (for example on Github), I kindly ask you to make these repositories private. Beware of plagiarism. Copying the proofs from the internet is not tolerated. You can consult each other for hints if you are stuck but the code should not be an exact copy.
There are further exercises available in the ressources of the course. You are encouraged to try them out!
The deadline for the homework is 05.12.2025 at 23:59.
To submit the homework, please do a private Github repository and invite me before the deadline.