Category Archives: Technical assistance

How to install mathlib and keep it up to date

Overview I’m going to explain how to install the current (bleeding edge) version of lean and mathlib, and set up a project directory on your (unix or windows or mac) computer where you can write lean files which use the … Continue reading

Posted in Technical assistance | 5 Comments

Installing Lean (and VSCode) on Windows from scratch

Here are some notes, but honestly I am no expert. This just worked for me though. Some hints for Mac users are in the comments below. Step 1: Install Lean. Go to https://github.com/leanprover/lean/releases/tag/v3.3.0 and scroll to the very bottom. Download … Continue reading

Posted in Technical assistance | 5 Comments