Assistance for importing libraries in vs code

Stream: new members

[Sushrut Jog]

Hey! I am pretty new to Lean; till now, I have been using it from the web UI, but now I am trying to install it on my system - macOS 14.4.1 - using VS Code.

I keep getting errors when I try to import stuff, as I have seen people do online. When I try doing import data.nat.prime as the guy does in https://www.youtube.com/watch?v=b59fpAJ8Mfs&t=237s, I get the error unknown package 'data'.

I also cannot execute the following code and get the error unknown identifier 'begin':
example (p q r : Prop) : ((p ∧ q) → r) ↔ ((p → r) ∧ (q → r)) :=
begin
split,
{ sorry, },
{ sorry, },
end

I can run all these things on the web UI, however. I suspect I have not correctly installed Mathlib dependencies?? Any help is appreciated. Thanks.

[Eric Wieser]

It sounds like you have installed Lean 4 but are following tutorials on Lean 3

[Eric Wieser]

Scott Morrison, should we edit all the old video titles to make this clear?

[Sushrut Jog]

Ah, okay, thanks! Is there any way I can find the equivalent syntax in Lean 4 for these online tutorials? Almost everywhere on the internet (including GPT and Gemini) I am finding this same syntax.

[Johan Commelin]

@Sushrut Jog These resources are all about learning Lean 4: https://leanprover-community.github.io/learn.html