Main text: https://leanprover-community.github.io/mathematics_in_lean/ written by Jeremy Avigad and Patrick Massot.
Additional texts:
Logic and Proof
written by Jeremy Avigad, Joseph Hua, Robert Y. Lewis, and Floris van Doorn.
The Mechanics of Proof written by Heather Macbeth.
Lean Game Server
"This server has been developed as part of the project ADAM: Anticipating the Digital Age of Mathematics at Heinrich Heine University Düsseldorf."
Lean Documentation:
https://docs.lean-lang.org/lean4/doc/
Quickstart: https://docs.lean-lang.org/lean4/doc/quickstart.html
These instructions will walk you through setting up Lean 4 together with VS Code as an editor for Lean 4.