Zulip Chat Archive

Stream: general

Topic: Problems Mac Instalation

Regivan Hugo Nunes Santiago (Nov 19 2020 at 19:29):

Hi! I am trying to install Lean 3 in Mac OS. I have followed the "Getting Started" homepage and introduced the command:

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh)" && source ~/.profile

in order to install Lean and Mathlib. However, the following code in Visualcode:

import data.nat.basic
open nat

constant prime : ℕ → Prop
constant even : ℕ → Prop
constant odd : ℕ → Prop

#check ∀ x, (even x ∨ odd x) ∧ ¬ (even x ∧ odd x)
#check ∀ x, even x ↔ 2 ∣ x
#check ∀ x, even x → even (x^2)
#check ∀ x, even x ↔ odd (x + 1)
#check ∀ x, prime x ∧ x > 2 → odd x
#check ∀ x y z, x ∣ y → y ∣ z → x ∣ z

returns the following error:

-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

  • invalid import: data.nat.basic
    could not resolve import: data.nat.basic

When I type: lean --path, I get:

"is_user_leanpkg_path": true,
"leanpkg_path_file": "/Users/lean02/.lean/leanpkg.path",
"path": [

However, the path: /Users/lean02/.lean/leanpkg.path, does not exists.

Can anyone help me? I think that if a change the path variable to point to mathlib I can solve this problem, however I do not know where is mathlib and where to put the right path to point to it.

Thank you in advance.


Bryan Gin-ge Chen (Nov 19 2020 at 19:31):

Did you read the projects page which is linked at the bottom of the macOS install page? You shouldn't need to play around with paths; the leanproject utility should be handling all of this for you.

Regivan Hugo Nunes Santiago (Nov 19 2020 at 20:08):

Dear Bryan, thank you very much. You have solved my problem.

Bryan Gin-ge Chen (Nov 19 2020 at 20:14):

Great, glad you got things working! Feel free to ask here if you have any other issues.

Last updated: Aug 03 2023 at 10:10 UTC