在Lean中，类似2 + 2 = 4的值类型为Prop。同时，2 + 2 = 4本身也是一个类型。要证明一个命题，等价于构造出类型为这个命题的值。如下所示：
def claim1 : Prop := 2 + 2 = 4
def proof : claim1 := by ref若想证明一个命题为假，如2 + 2 = 5，我们可以构造一个类型为Not(2 + 2 = 5)的值。
每个命题最多只有一个独特的证明，也即，命题的多个证明是等价的，无法区分的。
在Lean中，类似2 + 2 = 4的值类型为Prop。同时，2 + 2 = 4本身也是一个类型。要证明一个命题，等价于构造出类型为这个命题的值。如下所示：
def claim1 : Prop := 2 + 2 = 4
def proof : claim1 := by ref若想证明一个命题为假，如2 + 2 = 5，我们可以构造一个类型为Not(2 + 2 = 5)的值。
每个命题最多只有一个独特的证明，也即，命题的多个证明是等价的，无法区分的。