Updated: 18 October 2025
Create a new project depending on mathlib4. After running these commands, put Lean code inside .lean files inside my_project/MyProject/ or subfolders. See Creating a Lean project
lake +leanprover/lean4:nightly-2024-04-24 new my_project math
cd my_project
lake update