Setting up Lean project

Stream: new members

[Vic]

Hi all! I am setting up LEAN using VScode and finished all the procedures. When I tried to create a new project on VScode on mathlib, it got stuck on the step of updating dependecies: mathlib4: lean-toolchain. If I create a standalone project, it can be created successfully very easily. Do you know how to address this? Thanks!

[Notification Bot]

A message was moved here from #mathlib4 > Siegel's Lemma by Kyle Miller.

[Kevin Buzzard]

What do you mean by "create a new project on VScode on mathlib"?

lake new RiemannHypothesisProof math

should make a new project which has mathlib as a dependency (which is what you want to do if you want to make a project where you're working on the proof of a mathematical theorem).

[Kevin Buzzard]

(@Vic your message has been moved to here by the way)