Installing relevant packages for Lean's math lib

Question

I'm using the Lean computer proof assistant on my Mac.

I tried to import data.nat.basic from lean's documentation, just like this:

import data.nat.basic

I get this:

could not resolve import: data.nat.basic
All Messages (2)
Topologic.lean:1:0
file 'data/nat/basic' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more
Topologic.lean:6:1
invalid import: data.nat.basic
could not resolve import: data.nat.basic

Evidently I missed the memo on one of the relevant installations and it means I can't use math lib. Basically I want to be able to use hash maps and lists from lean's math lib.

Can anyone direct me towards a tutorial for installing the relevant files for lists and hash sets? I am going to guess this involves installing math lib packages.

I've never actually worked with GitHub before so I would be grateful if someone had a link to a complete set of instructions.

Further, it seems like the instructions for Mathlib installation don't work- I get an error message printed in the comments below.

Answer 1

(Here are some general instructions for installing Lean 3 and setting up a project with mathlib, but for your specific problem, you may need to get help on the Lean zulip chat.)

Installing Lean 3 and other stuff

As Mario said, the installation instructions for Lean 3 can be found at Getting Started with Lean. Since you mention you are on an M1 mac, the directions are here: M1 Macs / Apple Silicon. Unfortunately, setting of Lean (and many other software tools) on M1 macs can be error prone, so feel free to stop by the Lean Zulip for more one-on-one support.

Setting up a lean project to use mathlib

Once Lean is installed you will want to make a Lean project which will allow you not only to use the base lean library, but also Lean's main mathematical library mathlib (which is where data.nat.basic comes from). Those instructions can be found in Lean projects, but let me give you some guidance.

(And for future readers, this is for Lean 3. Setting up projects for Lean 4 is different.)

When you want to start a new Lean project, in a terminal, go to the directory you want to create your project in, e.g.

cd ~/Documents/lean_projects

Then enter the following to make a new project titled my_awesome_project:

leanproject new my_awesome_project

To start VS code in your project, either start VS Code up manually, select "Open..." and navigate to my_awesome_project, or if you installed VS Code from homebrew you can also do:

code my_awesome_project

By making a Lean 3 project you will have added a number of files and directories:

• .gitignore (and other git stuff): This is a git project which will let your save progress and upload your project to github
• src: This is where you Lean files go.
• _target: This is where the mathlib files are stored along with their compiled .olean files. Don't touch this.
• leanpkg.path and leanpkg.toml: These are lean configuration files. Usually you don't need to touch them, especially if you use leanproject to do all of your upgrading, etc.

If things are set up correctly, then you can make a new my_awesome_file.lean file in src and start to type in valid lean.