Blog/lean

_posts/2026-06-28-lean.md

@@ -0,0 +1,184 @@
+---
+title: "Mathematics but not handwavey (real)"
+date: 2026-06-28
+description: "First steps in formal mathematics with Lean"
+tags: ["theoretical mathematics", "first principles"]
+math: true
+---
+
+## Intro
+
+### Discrete Mathematics
+### ZHAW Background -> different approach to mathematics
+### Vocabulary
+
+
+
+∃: there exists
+≤: less than or equal to
+
+Today we will be proving the total order of natural numbers.
+
+$$
+\Huge \forall x,y \in \mathbb{N} : x \le y \lor y \le x
+$$
+
+
+$$
+\boxed{\displaystyle \quad \forall x,y \in \mathbb{N} : x \le y \lor y \le x \quad}
+$$
+
+$$
+\boxed{\forall x,y \in \mathbb{N} : x \le y \lor y \le x}
+$$
+
+$$
+\fbox{\(\displaystyle \quad \forall x,y \in \mathbb{N} : x \le y \lor y \le x \quad\)}
+$$
+
+$$
+\colorbox{#fff3cd}{$\displaystyle \forall x,y \in \mathbb{N} : x \le y \lor y \le x$}
+$$
+
+
+$$
+\fbox{
+  $\forall (x,y : ℕ) : x ≤ y ∨ y ≤ x$
+}
+$$
+
+
+![graph](/assets/blog/dependency_graph.svg)
+
+
+
+Before we do that we need to get some definitions out of the way.
+
+## Definitions
+
+### Natural Number?
+
+First:
+
+What even is a Natural number?
+Natural numbers are defined to be all "positive" "whole" numbers.
+
+$$
+\mathbb{N} = \{0,1,2,3,4,5, \ldots \}
+$$
+
+But this isn't yet a concrete definiton.
+Natural numbers can be seen as a sequeence. The sequence starts at 0.
+Each number is either 0 or a successor.
+
+$$
+\mathbb{N} 
+ \stackrel{\mathrm{def}}{=} \begin{cases}
+  0 &\text{Base case} \\ 
+  \mathrm{succ} &\text{Else} \\ 
+\end{cases}
+$$
+
+### Addition?
+
+Now we can define addition. (Using axioms)
+
+It isn't enough to define addition for speicfic numbers, like let's say `6 + 1 = 7`.
+We need to define addition for ALL numbers. We do this using induction.
+
+Here we fix the variable $a$ and check the our definition of natrual numbers from before.
+
+B is either zero, or a successor of a natural number.
+
+$$
+\underline{\Large{\forall a,b \in \mathbb{N} : a + b = \text{?}}}
+$$
+
+$$
+\forall a,b \in \mathbb{N} : a + b \stackrel{\mathrm{def}}{=}
+\begin{cases}
+a & b = \text{0} \\ 
+succ(a + d) & b = \operatorname{succ}(d) \\ 
+\end{cases}
+$$
+
+$$
+\text{Example: } \underline{1 + 2 = 3}
+$$
+
+
+
+$$
+\begin{array}{rl}
+              & \textbf{Axioms} \\
+\mathrm{i.}   & 1 \stackrel{\mathrm{def}}{=} succ(0) \\
+\mathrm{ii.}  & 2 \stackrel{\mathrm{def}}{=} succ(1) \\
+\mathrm{iii.} & 3 \stackrel{\mathrm{def}}{=} succ(2) \\
+\mathrm{iv.}  & a + 0 \stackrel{\mathrm{def}}{=} a \\
+\mathrm{v.}   & a + \operatorname{succ}(b) \stackrel{\mathrm{def}}{=} \operatorname{succ}(a+b) \\
+\end{array}
+  \begin{array}{l|l}
+\textbf{Statements} & \textbf{Reasons} \\
+\hline
+  1 + 2                                               & \text{Given}   \\
+  1 + \operatorname{succ}(1)                          & \mathrm{ii.}   \\
+  \operatorname{succ}(1 + 1)                          & \mathrm{v.}    \\
+  \operatorname{succ}(1 + \operatorname{succ}(0))     & \mathrm{i.}    \\
+  \operatorname{succ}(\operatorname{succ}(1 + 0))     & \mathrm{v.}    \\
+  \operatorname{succ}(\operatorname{succ}(1))         & \mathrm{iv.}   \\
+  \operatorname{succ}(2)                              & \mathrm{ii.'}  \\
+  3                                                   & \mathrm{iii.'} \\
+  \end{array}
+$$
+
+
+$$
+\underline{\Large{\forall a,b \in \mathbb{N} : a \le b \text{ ?}}}
+$$
+
+$$
+\forall a, b \in \mathbb{N} : a \le b \stackrel{\mathrm{def}}{\iff} ∃ (c : ℕ), b = a + c
+$$
+
+![graph](/assets/blog/numberline.png)
+
+## Prooving
+
+```lean
+theorem le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by
+  induction y with
+  | zero =>
+    right
+    exact zero_le x
+  | succ d hd =>
+    cases hd with
+    | inl hl =>
+      cases' hl with c hc
+      rewrite[hc]
+      left
+      rewrite[succ_eq_add_one]
+      use c + 1
+      rewrite[← add_assoc]
+      rfl
+    | inr hr =>
+      cases' hr with c hc
+      cases c with
+      | zero =>
+        rewrite[zero_eq_0] at hc
+        rewrite[add_zero d] at hc
+        left
+        rewrite[hc]
+        exact le_succ_self d
+      | succ a =>
+        rewrite[add_succ] at hc
+        right
+        rewrite[hc]
+        use a
+        rewrite[succ_add]
+        rfl
+```
+
+![graph](/assets/blog/lean_thing.png)
+
+<https://tinyurl.com/4tr5uc7c>
+