unknown package 'data'

Stream: lean4

[Judy Zhu]

Hi! I am following the Lean tutorial and in the first line 'import data.real.basic' I got an error saying 'unknown package 'data'.' I disabled Lean4 extension on VScode while only enabled Lean3 but the same error still exists. What should I do? Thank you!

[James Gallicchio]

Could you link the tutorial you are following? At this point I think the recommendation is to learn Lean4, but many of the resources/tutorials haven't been updated to Lean4 yet...

[Judy Zhu]

The tutorial I'm following is from the official web: https://github.com/leanprover-community/tutorials. I think this one is for Lean3. Is there any recommendation on how to learn Lean4? Thanks.

[Alex J. Best]

What is your background and what are you interested in learning lean for? The advice of which resources to look at depends a bit on that. But you could look up "mathematics in lean 4" or "theorem proving in lean 4" as a good start