What are the differences between theorem, example, def, etc?

Question

What are all the differences between these keywords that allow for defining top level variables?

What I have noticed so far is that theorems can't be anonymous — you can write example : A := B but not theorem : A := B.

Answer 1

An outline of the differences in Lean 4, which you mentioned is the version you are interested in:

• A def is the primary way to define a named function / value in Lean. Unless its result type is Prop or it is marked noncomputable, a def will be compiled into Lean's intermediate representation (IR) in preparation for execution by Lean's interpreter and/or for further compilation into C code.

def add (x y : Nat) : Nat := x + y -- a simple computation
def one_plus_one_eq_two : 1 + 1 = 2 := rfl -- theorems can be defs too!

• A theorem is essentially a noncomputable def. This means that values defined by a theorem cannot be used in ordinary computation as they will not (and maybe cannot) be compiled down into executable code. Note that Lean erases types (eg., T : Type u, Prop : Type), propositions (e.g., 1 = 1 : Prop) and proofs (e.g., rfl : 1 = 1) -- all of which are technically noncomputable -- before attempting compilation, which is why they are still safe to use in computable code. Such values are termed irrelevant by the Lean compiler IR.

theorem foo : Nat := 5
def addFoo (x : Nat) := x + foo 
/-
error: 
failed to compile definition, consider marking it as 'noncomputable' 
because it depends on 'foo', and it does not have executable code
-/
#eval foo -- same error
theorem addFoo' (x : Nat) : Nat := x + foo -- ok

• An example creates an anonymous def that is type checked for correctness and then immediately discarded by Lean. Thus, an example has no lasting effect on the environment and cannot be referred to by later declarations. Note that while Lean will end up discarding the code it generates from an example, it does still, by default, generate code. Thus, you must mark an example noncomputable if it uses a noncomputable definition for a (i.e., to define a value that is not erased).

example : 1 + 1 = 2 := rfl
example (x y : Nat) : Nat := x + y
example (x : Nat) : Nat := x + foo -- same error as above
noncomputable example (x : Nat) : Nat := x + foo -- ok

Note that there are other keywords for defining functions / values (e.g., axiom, opaque, abbrev, etc.) which I have not discussed here as you did not ask about them. Furthermore, given your choice of keywords to compare, it seemed best to focus on the named/anonymous, computable/noncomputable distinctions that separate def, theorem, and example.