Hello, Lean!

Meet Lean 4 as a practical programming language and proof assistant. You will set up your mental model, run your first commands, and understand how Lean gives feedback.

Learning Goals

• Explain what Lean 4 is and why it matters.
• Use #eval and #check to explore.
• Understand the Lean file workflow and Infoview feedback loop.

What is Lean 4?

Lean 4 is a functional programming language, a theorem prover, and a platform for formalized mathematics. As a programmer, you can treat it like a strongly typed language with a powerful compiler. As a mathematician, you can treat it like a tool for machine-checked proofs.

The unique feature of Lean is its interactive environment: every line of code is checked as you write it, and Lean tells you the exact type or the exact error. This makes learning fast and dependable.

Your First Commands

You can run code instantly with #eval and inspect types with#check.

1#eval 2 + 3
2#eval "Lean" ++ " 4"
3
4#check Nat
5#check String
6#check (Nat → Nat)

1#eval "Hello, Lean!"
2#check "Hello, Lean!"

How Lean Feels in the Editor

Lean runs inside your editor. When you move your cursor, the Infoview shows the current goal, expected types, and evaluation results. The feedback loop is immediate.