Skip to content

Latest commit

 

History

History
42 lines (28 loc) · 2.08 KB

setup.md

File metadata and controls

42 lines (28 loc) · 2.08 KB
title layout nav_order
Setup
default
2

Getting Started

To participate in this course, you will need:

  1. A computer with elan and vscode installed; you must also install the Lean4 package for vscode.
  2. A github account, preferably with an ssh key set up.

The natural number game

To start off, please look at the natural number game, and complete as much as you can. Try to finish the first few worlds at least. This game is an excellent beginner-friendly introduction to the mechanics of interactive theorem proving in Lean4.

Note: Proving theorems is just a part of this course. Arguably another interesting aspect of formal mathematics is writing definitions. This course will cover both.

Resources

Here is a short list of resources which may be useful.

  1. The Lean community webpage.
  2. The lean zulip channel.
  3. Theorem proving in Lean4.
  4. Mathematics in Lean.
  5. The official Lean4 documentation.
  6. The Hitchhiker’s Guide to Logical Verification

Course Specific Resources

  1. This webpage.
  2. The course repository

Other Useful Links

Please let me know if you would like for me to add any additional links in this section.

  1. A list of unicode shortcuts in VSCode