Module 1 · Level 1

Your First Lean File

Create a Lean file, run a few commands, and see Lean respond. This is where the feedback loop starts to feel natural.

Create Hello.lean

In your project, create Hello.lean and add the following:

lean|Hello.lean

1#eval "Hello, Lean!"
2#check Nat
3#check String → Bool
4
5def greeting : String := "Welcome to Lean 4"

Exercise: Extend Your File

Add a new definition named farewell that returns a string. Then evaluate it with #eval.

lean

1def farewell : String := "See you soon"
2#eval farewell

💡

Keep your file small. Lean works best when you iterate in tiny steps and rely on the Infoview after every change.

Key Takeaway

Lean files are just code. Start simple, evaluate often, and read the Infoview.