Beginner, cannot import in Lean

Question

I am an absolute beginner, not a programmer, trying to learn formal verification with Logic and Proof. I cannot import anything in Lean.

I extract the tar file for the binary to /tmp then do

/tmp/lean-3.4.1-linux/bin/./lean /tmp/test.lean

It works except when I am importing anything. So if my file test.lean just says

open classical
example (P : Prop) : P ∨ ¬ P := em P

there is no error. But if the same file instead says

import data.set

I get the error message

/tmp/test.lean:1:0: error: file 'data/set' not found in the LEAN_PATH  
/tmp/test.lean:1:0: error: invalid import: data.set  
could not resolve import: data.set

A similar error occurs with import data.nat.

What am I doing wrong, and what should I do? I am using Ubuntu 16.04. Please note that since I am a beginner, I have never compiled anything from source.

Answer 1

I got a solution by contacting Prof. Avigad directly.

It turns out that the book uses not only the standard library but also the Lean mathematical components library, mathlib. Installing it worked for me. I can now do import data.set without getting an error.