A Lean Syntax Primer

Programming with proofs.

A Lean Syntax Primer

September 2, 2025

Pay what you like

This is my opinionated syntax primer for the Lean programming language. It is far from complete and may contain inaccuracies (I’m still learning Lean myself) but this is how I wish I was introduced to it, and what I wish was clarified.

Why Lean?

This post assumes you’re already eager to learn a bit of Lean. For motivation, I humbly submit to you two takes: one from me and one from its creator.

Declaring Definitions

Let’s start by writing a few definitions. These can appear at the top level of the file:

def name := "Alice"
def age := 42

(Try it in the online playground.)

Note you have to write := (assignment) rather than =. This is because Lean uses = for comparisons. This might remind you of Go or Pascal (if you’re old enough).

Although you haven’t written any types explicitly, each definition is typed. To find out their types, you can hover over name and age in the online playground or inside VS Code. You should see name : String and 42 : Nat, respectively. (Going forward, when I say “hover”, I’ll assume either of those environments.)

Here, String is obviously a string, while Nat stands for a “natural number”. In Lean, natural numbers include 0, 1, 2, and so on, going up arbitrarily large.

You could specify types explicitly by writing : SomeType before the :=:

def name : String := "Alice"
def age : Nat := 42

If you don’t, Lean will try to infer the type from what you wrote on the right side.

Specifying Types

You’ve just seen that Lean infers "Alice" to be a String and 42 to be a Nat. A Nat could be 0, 1, 2, and so on. What if you try a negative number like -140?

def temperature := -140

If you hover on temperature, you’ll see that it’s an Int. An Int, which stands for integer, is a built-in type allowing any whole number, negative or positive.

You could ask for a specific type like Int explicitly in the definition:

def roomTemperature : Int := 25

If you just wrote def roomTemperature := 25, Lean would give you a Nat, but adding : Int explicitly nudged type inference to try to produce an Int.

Another way to ask for a specific type is to wrap the expression itself:

def roomTemperature := (25 : Int)

In both cases, you’re saying you really want to get an Int. If Lean couldn’t figure out how to produce an Int from the expression, it would give you a type error.

Let’s calculate Alice’s birth year based on her age:

def name := "Alice"
def age := 42
def birthYear := 2025 - age

We need to get birthYear somewhere on the screen. If you’re following along in the online playground, you might realize that your code isn’t actually running.

This is because there are two ways to use Lean.

One way to use Lean is to run your code. Another way to use Lean is to prove some facts about your code. You can also do both—write code and proofs about it. We’re going to start by learning to run some code, and then we’ll look at writing proofs.

Running Code

If you just want to see the result of some expression, add an #eval command:

def name := "Alice"
def age := 42
def birthYear := 2025 - age

#eval birthYear

Hovering over this #eval in your editor will now say 1983. Another place where it’ll show up is the InfoView on the right side of the online playground:

[1983 shows up in InfoView]

Note 1983 in the bottom right corner. If you set up VS Code with the Lean extension locally, you can get the same InfoView displayed like this:

[Screenshot of InfoView in VS Code]

Lean InfoView is incredibly useful and I suggest to keep it open at all times.

The #eval command is handy for doing inline calculations and to verify your code is working as intended. But maybe you actually want to run a program that outputs something. You can turn a Lean file into a real program by defining main:

def name := "Alice"
def age := 42
def birthYear := 2025 - age
def main := IO.println birthYear

I intentionally did not say “a main function” because main is not a function. (You can hover over it to learn the type of the main but we won’t focus on that today.)

Let’s run our program:

lean --run Scratch.lean

Now 1983 appears in the terminal. Alternatively, you could also do this:

lean Scratch.lean -c Scratch.c

The C code generated by Lean compiler will include an instruction to print 1983:

LEAN_EXPORT lean_object* _lean_main(lean_object* x_1) {
lean_object* x_2; lean_object* x_3;
x_2 = lean_unsigned_to_nat(1983u);
x_3 = l_IO_println___at___main_spec__0(x_2, x_1);
return x_3;

Now you see that Lean can be used to write programs.

Writing Proofs

Now let’s prove that age + birthYear together add up to 2025.

Define a little theorem alongside with your program:

def name := "Alice"
def age := 42
def birthYear := 2025 - age

theorem my_theorem : age + birthYear = 2025 := by
sorry

A theorem is like a def, but aimed specifically at declaring proofs.

The declared type of a theorem is a statement that it’s supposed to prove. Your job is now to construct a proof of that type, and the Lean “tactic mode” (activated with by) provides you with an interactive and concise way to construct such proofs.

Initially, the InfoView tells you that your goal is age + birthYear = 2025:

[Goal: age + birthYear = 2025]

However, that’s not something you can be sure in directly. What’s age? Try to unfold age to replace age in the goal with whatever its definition says:

[Goal: 42 + birthYear = 2025]

Note how this made the goal in your InfoView change to 42 + birthYear = 2025. Okay, but what’s a birthYear? Let’s unfold birthYear as well:

[Goal: 42 + (2025 - age) = 2025]

You’re getting closer; the goal is now 42 + (2025 - age) = 2025. Unfolding birthYear brought back age, what’s age again? Let’s unfold age:

[Goal: 42 + (2025 - 42) = 2025]

At this point the goal is 42 + (2025 - 42) = 2025, which is a simple arithmetic expression. The built-in decide tactic can solve those with gusto:

And you’re done! You’ve now proven that age + birthYear = 2025 without actually having run any code. This is being verified during typechecking.

You can verify that editing age to another number will not invalidate your proof. However, if you edit birthYear to 2023 - age, the proof no longer typechecks:

[tactic 'decide' proved that 42 + (2023 - 42) is false]

Of course, this was all a bit verbose. Instead of doing unfold for each definition manually, you can tell the simp simplifier to do them recursively for you:

[simp [age, birthView] solves the same theorem]

This also proves the goal.

This example is contrived but I wanted to show you how it feels to step through the code step by step and transform it “outside in”. It almost makes you feel like you’re the computer, logically transforming the code towards the goal. It won’t always be so tedious, especially if you have some useful theorems prepared.

We’ll come back to proving things, but for now let’s learn some more Lean basics.

Opening Namespaces

Have another look at this main definition:

def name := "Alice"
def age := 42
def birthYear := 2025 - age
def main := IO.println birthYear

[...]

Original source