This project provides a Lean 4 autograder that works with Gradescope.

To generate the files Gradescope needs, this project uses a repository on GitHub that must contain a template of the assignment the students will receive. This project retrieves from the template how many points each exercise is worth. Thus, the template must follow the following pattern:

@[autograded 2]
theorem th3 (h : ¬q → ¬p) : (p → q) := sorry

The autograder would award 2 points for a sorry-free proof of th3 that does not use any nonstandard axioms. Extra axioms can be allowed with the @[legalAxiom] attribute.

It is NOT necessary to edit autograder_config.json unless you want to use the helper scripts.

This project is meant to work with MathLib assignments, so for a good Gradescope performance, their container must have at least 2.0 CPU and 3.0GB RAM.

Add this project as a lake dependency to your course project. Then, set up the autograder shell for use with an assignment in that course project.

For an example, see fpv2023. The lakefile of this project imports this autograder project. To create a Gradescope assignment for HW1, I would edit the configuration file in the autograder shell to point at Homeworks/Homework1.lean in that repository, run the make_autograder.sh script, and upload the resulting zip file to Gradescope. Students would then submit only their Homework1.lean file to Gradescope.