Tips and suggestions for teaching with Lean #

In order to help people interested in teaching with Lean, we've collected some strategies and approaches here that have worked well for people in the community. Depending on the context of your course, these approaches may or may not make sense.

Planning your course #

If you are thinking about introducing Lean into a course, or designing a course around Lean, there are some important questions you should ask yourself. Your answers to these questions can help find comparable courses that people have already taught, and can help you choose materials to use.

Organizing course projects #

It is common to use a "course project" to distribute lecture notes, examples, assignments, etc. while ensuring that students all remain on a fixed version of Lean and mathlib. Here are examples from a course at Fordham and a course at Brown. The former includes detailed notes that get compiled to HTML; the latter relies on an external textbook reference.

Without some kind of structure like this -- for example, if students receive bare .lean files -- it is hard to ensure that they all use the same version of Lean. It is also a good way to provide a "library" file or files containing basic definitions, tactics, and such that are useful for your course.

These projects are often hosted on GitHub. Students are asked to clone the project, or create a Codespace or Gitpod instance, at the start of the course. They are instructed to pull updates periodically, for instance, when new homeworks are released. If students are not expected to be proficient with git, you can provide helper scripts that attempt to do this management automatically.

Some instructors recommend that students copy homework files before beginning an assignment, working on the copied version, to avoid merge conflicts if the assignment should change.

Other instructors have used GitHub Classrooms for assignment releases. In this setup, each assignment must be its own standalone Lean project.

Lean-in-the-cloud setups #

Our resources page has pointers to setting up GitHub Codespaces and Gitpod for use with a course project. Especially for large courses aimed at students who might struggle to install Lean locally, the use of cloud resources to run Lean can greatly simplify the beginning of a course.

In both approaches, students will be able to use VSCode in a browser to edit Lean files with a Lean server running remotely. With Codespaces, a convenient VSCode plugin makes it possible to work from a local VSCode installation too. The obvious upsides are that there is a uniform environment for all students, without installation headaches, and that no student is using an underpowered machine. Downsides include that student files are saved on the cloud, and students might struggle to download and submit them; these cloud services limit the number of free hours per student per month; and internet access is required to work on the course.

Some instructors have successfully run large courses using these resources, and many offer them as an option to students. For GitHub Codespaces, it is important to remind students to sign up for GitHub's student benefits to take advantage of extra Codespaces hours.

Renaming and redefining tactics #

The Lean/mathlib names for tactics may not match how you present these topics in class. In Lean 4 it is easy to create aliases for certain tactic calls or change the behavior of existing tactics within a course project. (In the linked examples, in any course file importing Tactics.lean, the behavior of linarith will be redefined.)

Ending proofs with done #

It can sometimes be confusing to tell when a tactic proof is complete, since the error message appears at the top of the proof but not at the bottom. Some instructors have had success teaching students to begin writing a proof with the tactic done at the end.

example (x : ) : x = x := by 
  -- fill in your proof here

An alternative is to use curly braces after by:

example (x : ) : x = x := by {
  -- fill in your proof here