You can download the assignments here. Also check out each assignment page for any additional info.


Assignments will be submitted on gradescope. Make sure to setup your Gradescope correctly by following the instructions.

Each assignment will correspond to a single lean file. You only need to submit this single file on gradescope.The “autograder” on gradescope simply type checks the file and reports back the result. If the autograder runs without error, you likely will receive full points, but all submissions will still be manually graded. Talk to Rob if you find the idea of complete grading automation intriguing.

Regrade Policy

Students may request a regrade on an assignment up to one week after that grade has been released. This should be done directly in Gradescope.

Late Policy

Students may submit assignments one or two days late, up to a total of six late days over the semester. For example, you could be one day late on six different assignments; two days late on three different assignments; or any combination in between. If longer extensions are needed in exceptional circumstances, please contact the instructor directly.

Collaboration Policy

Students are strongly encouraged to work together on the exercise problems and to discuss the homework assignments. Written homework submissions should be your own work. We advocate the “erased whiteboard” policy: talk through your solutions with a classmate, but do not reference any written notes from that conversation when you implement your solutions. A good rule of thumb is that your discussions should remain at the conceptual level. Ask “what is the syntax for a proof by induction,” instead of asking whether your proof by induction is correct. Above all, students should adhere to Brown’s academic code.