import data.nat

Stream: mathlib4

[Nathaniel Collins]

I'm trying to follow this tutorial (https://www.youtube.com/watch?v=b59fpAJ8Mfs) about the infinitude of primes in lean 4 and I'm getting a "processing stopped" error with the import data.nat.prime statement. https://stackoverflow.com/questions/50805696/beginner-cannot-import-in-lean This post made me think that I should install mathlib or mathlib4. I have installed both but the error has not changed. https://leanprover-community.github.io/archive/stream/270676-lean4/topic/issues.20with.20.22import.22.html This post made me think that this statement has not been ported over to lean 4 yet. Is this the case or am I missing something? Thank you!

[Kevin Buzzard]

that is a tutorial about the infinitude of primes in Lean 3.

[Kevin Buzzard]

Lean 4 has no maths library to speak of right now. If you want to do mathematics at this level then probably you want to install Lean 3 and the community tools following the instructions on the community website https://leanprover-community.github.io/get_started.html

[Nathaniel Collins]

Great! I'll get started on that now