Module 2 · Level 5

Logic Gates

Learn the difference between booleans and propositions, and how Lean treats logic as part of its type system.

Bool vs Prop

Bool is a value you compute. Prop is a statement you prove. Lean keeps them distinct, but you can move between them.

lean

1#check true           -- Bool
2#check (2 + 2 = 4)    -- Prop
3
4def isEven (n : Nat) : Bool := n % 2 = 0
5#eval isEven 4

Many theorems state properties about booleans. You can turn a boolean check into a proposition with decide or by writing a predicate.

lean

1def IsEven (n : Nat) : Prop := n % 2 = 0
2
3#check IsEven 4

Exercise: Simple Predicate

Define a predicate IsPositive for integers and test it with#check.

lean

1def IsPositive (n : Int) : Prop := n > 0
2#check IsPositive 3

ℹ

Propositions are not booleans. You cannot #eval a proposition without deciding it.

Key Takeaway

Bool is computed. Prop is proven. Lean keeps the distinction clear to avoid logical mistakes.