15 hours ago
- In Lean, logical statements like `2+2=4` are of type `Prop`, not Boolean.
- Propositions in Lean are also types; a proof is a value of that type.
- Proving a proposition is equivalent to constructing a value of its type.
- Multiple proofs of the same proposition are considered equal (proof irrelevance).
- Lean allows expressing constraints like 'x is between 0 and 1' as type-level proofs, enabling typed truthfulness.
- Proofs can be composed using existing theorems from Mathlib.
- The `Eq` type is defined with only one constructor `refl`, making it impossible to prove false equalities.
- This bridges mathematics and programming by computing logic, not just numbers.