Lean4.ai - Beginner's Guide

Step 1: Installation

The recommended way to install Lean 4 is through elan, the Lean version manager:

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

This installs elan, lean, and lake (the build tool).

Install VS Code and the Lean 4 extension. This gives you:

Use Lake to set up a new project with Mathlib:

lake init my_project math

Then run lake build to download dependencies. The first build takes a while as it fetches Mathlib's cache.

Tip: Run lake exe cache get in a Mathlib-dependent project to download precompiled oleans instead of building from source. This can save hours.

Work through these resources roughly in order:

Natural Number Game -- A browser game that teaches core tactics (rfl, rw, induction, etc.) through proving properties of natural numbers. No installation needed.
Theorem Proving in Lean 4 -- The standard textbook. Covers propositions, tactics, structures, type classes, and more.
Mathematics in Lean -- Hands-on exercises formalizing real mathematics with Mathlib. Great for building practical skills.
Functional Programming in Lean -- If you want to use Lean for programming (not just proofs), this book covers IO, monads, and practical programming patterns.

One of the biggest challenges in Lean is finding the right lemma or theorem. Here are the tools:

Lean Search -- Describe what you need in plain English (e.g., "sum of two even numbers is even") and it finds matching theorems.
Loogle -- Search by type signature. If you know the shape of the theorem you need, this is fast and precise.
exact? -- A tactic that searches Mathlib for a lemma that closes your current goal. Use it liberally.
apply? -- Like exact? but also suggests lemmas that partially match.
rw? -- Suggests rewrite lemmas that apply to your goal.

Tip: In VS Code, you can also use #check to inspect a term's type and #print to see a definition. Example: #check Nat.add_comm

AI tools can significantly speed up your workflow in Lean 4:

llmstep -- Suggests next proof steps directly in VS Code. Lightweight and fast.
Lean Copilot -- Runs LLMs natively inside Lean 4 to suggest tactics, search for proofs, and translate informal proofs to formal ones.
Claude / ChatGPT -- Modern LLMs can write Lean 4 code. Paste your goal state and ask for help. Claude Sonnet is a good balance of speed and quality for this.
LeanDojo -- If you're building your own AI prover, this provides the infrastructure to interact with Lean programmatically.

Tip: When using an LLM for Lean code, always paste the full goal state from the Infoview. The more context you give, the better the suggestions.

Read the Infoview constantly. The goal state shown in VS Code's Lean Infoview panel is your primary guide. Place your cursor after each tactic to see what changed.
Use sorry as a placeholder. It lets you skip a proof temporarily so you can work on the overall structure first, then fill in details.
Ask on Zulip. The Lean community is exceptionally welcoming. Post in the "new members" stream. Include your code and goal state.
Start small. Prove simple things about natural numbers and lists before tackling topology or algebra. Build up your tactic vocabulary gradually.
Use have and suffices to break proofs into smaller steps. This makes proofs easier to write and debug.
Learn the key tactics first: intro, apply, exact, rw, simp, ring, omega, norm_num, constructor, cases, induction. These cover a surprising amount of ground.

Once you're comfortable with the basics: