Lean 4 has become significantly more accessible in 2025, with the VS Code extension now handling most installation complexity automatically. This guide provides comprehensive instructions for setting up Lean 4 and Mathematics in Lean (MIL) across all major platforms, with special attention to common issues and regional access considerations.

Prerequisites and preparation

Critical timing note: Install Lean 4 and MIL at least one week before your course begins. Courses using Lean move quickly, and you'll need working software from day one. The initial setup can take 1-3 hours depending on your system and internet connection.

Required software components

Essential prerequisites you must install first:

1. Git - Required for Lean's dependency management system
2. VS Code - The officially supported editor with the best Lean integration
3. Command line familiarity - You'll need basic terminal/command prompt skills
4. Stable internet connection - For downloading dependencies (requires ~2GB total)

Command line basics

Before starting, ensure you can:

• Open a terminal (Mac/Linux) or command prompt (Windows)
• Navigate directories using cd
• Check if commands are installed using which [command] (Mac/Linux) or where [command] (Windows)
• Understand file paths and folder structures

If you're not comfortable with command line operations, consider using the VS Code-only installation method described below, which minimizes terminal usage.

Installation procedures by operating system

macOS installation (including M1/M2 Apple Silicon)

Method 1: VS Code automated installation (Recommended for beginners)