Yes, you should expect some frustration, especially if you want to configure things your way. The least painful pipeline should be the following (only follow t

Yes, you should expect some frustration, especially if you want to configure things your way. The least painful pipeline should be the following (only follow the instructions at the pages I am listing, as otherwise things may get too confusing): 1) Install lean as a VS Code extension lean4 following : https://leanprover.github.io/lean4/doc/quickstart.html https://leanprover.github.io/lean4/doc/quickstart.html 2) Read about using the build system `lake` here : https://leanprover.github.io/lean4/doc/setup.html https://leanprover.github.io/lean4/doc/setup.html 3) Note that this does not install mathlib4; leave that for later. 4) Start playing around with basic examples in VS Code by reading the beginning sections of https://leanprover.github.io/functional_programming_in_lean/title.html https://leanprover.github.io/functional_programming_in_lean/... 5) If something does not work on break, ask in the Zulip chat; the devs are gathering pain points to improve tooling every day. If this seems too painful, indeed you may want to wait a bit for the tooling to improve.