diff --git a/_posts/.2026-06-28-lean.md.swp b/_posts/.2026-06-28-lean.md.swp new file mode 100644 index 0000000..23eba83 Binary files /dev/null and b/_posts/.2026-06-28-lean.md.swp differ diff --git a/_posts/2026-06-28-lean.md b/_posts/2026-06-28-lean.md new file mode 100644 index 0000000..0a10cd1 --- /dev/null +++ b/_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) + + + diff --git a/_posts/2026-06-28-todo.md b/_posts/2026-06-28-todo.md new file mode 100644 index 0000000..8f632d9 --- /dev/null +++ b/_posts/2026-06-28-todo.md @@ -0,0 +1,343 @@ +--- +title: "Mathematics but not handwavey" +date: 2026-06-28 +description: "TODO" +tags: ["theoretical mathematics", "first principles"] +math: true +--- + +alternate titles: + +* Functional Programming Meets Rigoporous Mathematics +* Mathematics but cut the bullshit +* Mathematics but done right +* Dipping my toes into rigorous mathematics +* Mathematics but without gaps +* Let's PROVE IT! + +/-- If $x$ and $y$ are numbers, then either $x \leq y$ or $y \leq x$. -/ + +```lean +Statement le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by + sorry +``` + + +Explicitly use ≤ instead of <= +Use Latex where possible + +## scraps + +Underwood Dudley +"In mathematics problems can be solved, using reason, and the solutions can be checked and shown to be correct." + ++ Recently completed the natrual numbers game as an intro to LEAN and i think i really like it +https://adam.math.hhu.de/#/g/leanprover-community/nng4 + + +First principles (like [my 8bit CPU](projects/8bit-cpu/)) + +ETH Discrete Mathematik Chapter 6 + +> Definition 6.1. A proof system is a quadruple Π = (S,P,τ,φ), as above. + + +Excerpt + +from ETH Zürich +Departement Informatik +Diskrete +Mathematik +Ueli Maurer +Herbstsemester 2024 + +> **6.2.4 Proof Systems in Theoretical Computer Science**\* +> +> An important extension of the concept of proof systems are so-called interactive proofs. $^{16}$ In such a system, the proof is not a bit-string, but it consists of an interaction (a protocol) between the prover and the verifier, where one tolerates an immensely small (e.g. exponentially small) probability that a verifier accepts a “proof” for a false state- ment. The reason for considering such interactive proofs are: +> +> * Such interactive proofs can exist for statements for which a classical (non-interactive) proof does not exist. For example, there exists an interactive proof system for the non-Hamiltonicity of graphs. +> * Such interactive proofs can have a special property, called *zero-knowledge*, which means that the verifier learns absolutely nothing (in a well-defined sense) during the protocol, except that the statement is true. In particular, the verifier cannot prove the statement to somebody else. +> * Zero-knowledge proofs (especially non-interactive versions, so-called NIZK’s) are of crucial importance in a large number of applications, for example in sophisticated block-chain systems. + +## INTRO + +![Path from Axioms to QED](/assets/blog/lean_graph.svg) + + + assumptiosn: reader is familiar with discrete mathematic[118;1:3us + +### MOTIVATION + I don't like assumptions + I don't like bullshit + How do we know if a given stastement is real? + Why just "hope it works" + First principles + Start with Axioms and build our way up + + **Some definitions first:** + Axiom := most fundamental assumptions + Proof := + Theorem := + Statement := + Proposition := + + + How do I verify that a given proof is correct? + How do I verify that I didn't bullshit my way to QED. + + + Some semesters back I have completed the discrete mathematics (https://eventoweb.zhaw.ch/Evt_Pages/Brn_ModulDetailAZ.aspx?node=2901247e-aa27-4f84-a5d6-d6b33b234dbd&IDAnlass=1456265&IdLanguage=133&clearcache=true) course at ZHAW. Now i am here to re-visit it with a different lense upon learning about proof asistants. + + + My main struggle with discrete mathematics is the lack of feedback to my work. Analogy: checking if code compiles and runs correclty when only on paper is difficult. same with proofs. one misstep. GOAL: reduce human error + + I feel like my understanding of mathematics is too fuzzy. I want to be less hand wavey and want to see my gaps explicitly. + + explicitly out of scope: (type system of Lean, how lean works, RCOQ, full 99 variations of a proof review) + explicitly mention: NO AI has been used to aid with LEAN + NO AI has been used in this article except for language / phrasing + +### 99 VARIATIONS OF A PROOF + + 99 variations of a proofs proposes the idea that proofs are but mere logical arguments. + + we start with theorem: +$$ + (x : \mathbb{N})) - x^3-6x^2+11x-6=2x-2 \implies x=1 \lor x=4 +$$ + +Twoliner (Proof by factorization (Proof 1 - Oneline)): +$$ +x^3-6x^2+9x-4=0 \\ +(x-1)^2(x-4)=0 +\Box +$$ + +// thanks Josua for gifting me the book + + and proove it in 98 other ways + (find 99 logical reasonings) + my favourite is : Proof #6 - axiomatic -> first principles. first we define notation, then definitions and then solve find proor by means of applying axioms + + +// 20 - defintiional is quite similar to 6 +// - no hiddewn assumptions, everything clearly defined + +// some other proofs that spark joy to me are: +// 9 - monosyllabic - sma words +// 10 - wordless by showing pricutres of cube +// 27 - algorithmic + + +// fun ones: +// 11 - exam +// 15 - matrix +// 25 - open collaborative +// 28 - flowchart +// 29 - model + +// 26 - auditory + +// hate: +// 19 - jargon (reminds of LinkedIn) +/ [insert tier list] + +full book review and +tier list comes later.. + + // Most logical arguments are difficult to systematically veirfy. + // I love machines - they do exactly what they have been told to do. - not always what i want them to but at least they are deterministic. WHY can't we use them for mathematics? WE CAN + + // statement -> irrefutable proof + + +made me realize LEAN exists: +- https://arxiv.org/abs/2605.22763 + +## LEAN + +``` +ℕ +├── add_zero ───────┬── zero_add ──────┬── zero_le ───────┐ +│ │ ├── add_comm │ +│ │ └── add_assoc ─────┤ +├── add_succ ───────┼── succ_add ──────┬── add_comm ├── le_total +│ │ └── add_assoc ─────┤ +└── one_eq_succ_zero┴── succ_eq_add_one┬── le_succ_self ──┘ + └──────────────────┘ +``` + + // LEAN -> proof asistant + // > quote LEAN + // TOPIC: today we will prove that ℕ are totally orderred + // [image of a number line] + + // assumptions: ℕ has been defined as either 0 or succ + // a <= b has been defined as ∃ c : b = a + c (numberline example svg) + + + + +| | $a = False$ | $b = True$ | +| --- | --- | --- | +| $b = False$ | $False \lor False \implies False$ | $a \lor b \implies True$ | +| $b = True$ | $a \lor b \implies True$ | $a \lor b \implies True$ | + + +// our assumption: + +$$ +\fbox{ + $(x, y \in \mathbb{N}) : x <= y ∨ y <= x$ +} + +\Box +$$ + + + + // reads as: given two natural numbers, one of them is greater or equal than the other. Intuitively makes sense. example: 6,7. so here (6≤7) ∨ (7≤6) -> True ∨ False -> True. + Or given same numbers: (1≤1) ∨ (1≤1) -> True ∨ True -> True + // It is easy to show that the statement holds for two _specific_ numbers but we need to prove that it holds for _all_ numbers. We focus on ℕ for simplicity. + + + my version of the x <= y ∨ y <= x proof has inspired by Kevin Buzzard. + + + x <= y ∨ y <= x + + // here we can apply induction on y for example. + // we can split this into two cases. + // ind y with d hd + + hd: (x <= y ∨ y <= x) + + induction y = 0 + x <= 0 ∨ 0 <= x // right one has been proven + 0 <= x // exactly zero_le + induction y = succ(d) + x <= succ(d) ∨ succ(d) <= x + + // let's focus on our hypothesis from earlier (hd) + // let's break it up into parts + + (x <= y) ∨ (y <= x) + | | + | right: hr := (y <= x) + left: hl := (x <= y) + + + // here we can apply cases as per definition + + // > If h : P ∨ Q is a hypothesis, then cases h with hp hq will turn one goal into two goals, one with a hypothesis hp : P and the other with a hypothesis hq : Q. + +.. + + + +## Final Proof + +Axioms +```lean + +/- BEGIN PROVE: x ≤ y ∨ y ≤ x -/ +induction y with +| zero => + right /- 0 ≤ x -/ + exact zero_le x +| succ d hd => + /- ind y=0 -/ + /- BEGIN PROVE: x ≤ 0 ∨ 0 ≤ x -/ + + /- END PROVE: x ≤ 0 ∨ 0 ≤ x -/ + + /- ind y=d -/ + cases hd with hl hr /- hd = hl ∨ hr + | hr := d ≤ x + hl := x ≤ d + -/ + cases hl with c hc /- hc := d = x + c -/ + left /- x ≤ succ d -/ + rw[hc] + use c + 1 + rw[succ_eq_add_one] + rw[← add_assoc] + rfl + + /- trial and error -/ + cases hr with e he /- + hr : d ≤ x + he : x = d + e + -/ + cases e with a /- e -> {0, succ(a)} -/ + /- e=0 ; he : x = d + 0 -/ + rw[add_zero] at he /- he : x = d -/ + left + rw[he] + exact le_succ_self d /- le_succ_self x - x ≤ succ x-/ + /- he : x = d + succ a -/ +``` + +Prereqs / Assumptions + +```lean +Statement succ_eq_add_one n : succ n = n + 1 := by + rw [one_eq_succ_zero] + rw [add_succ] + rw [add_zero] + rfl + +Statement zero_le (x : ℕ) : 0 ≤ x := by + use x + rw [zero_add] + rfl +``` + +Now MY proof: + +```lean +Statement 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 + rw[hc] + left + rw[succ_eq_add_one] + use c + 1 + rw[← add_assoc] + rfl + | inr hr => + cases hr with c hc + cases c with + | zero => + rw[zero_eq_0] at hc + rw[add_zero d] at hc + left + rw[hc] + exact le_succ_self d + | succ => + rw[add_succ] at hc + right + rw[hc] + use a + rw[succ_add] + rfl +``` + + + - https://adam.math.hhu.de/#/ + - + - https://github.com/julian/lean.nvim + - https://leanprover-community.github.io/1000.html diff --git a/assets/blog/dependency_graph.svg b/assets/blog/dependency_graph.svg new file mode 100644 index 0000000..9efe3e4 --- /dev/null +++ b/assets/blog/dependency_graph.svg @@ -0,0 +1,2 @@ + +ℕa + succ(d) = succ(a + d)a + 0 = a1 = succ(0)succ(n) = n + 10 + n = nsucc(a) + b = succ(a + b)a + b = b + aa + b + c = a + (b + c)0 ≤ xx ≤ succ(x)x ≤ y ∨ y ≤ x \ No newline at end of file diff --git a/assets/blog/lean_graph.png b/assets/blog/lean_graph.png new file mode 100644 index 0000000..966ee83 Binary files /dev/null and b/assets/blog/lean_graph.png differ diff --git a/assets/blog/lean_graph.svg b/assets/blog/lean_graph.svg new file mode 100644 index 0000000..6845608 --- /dev/null +++ b/assets/blog/lean_graph.svg @@ -0,0 +1,272 @@ + + + +NatDeps + + +cluster_order + +Order + + +cluster_basic + +Basic rewrites + + +cluster_axioms + +Axioms + + +cluster_algebra + +Algebra + + + +N + +ℕ + + + +add_zero + +add_zero +(a : ℕ) : a + 0 = a + + + +N->add_zero + + + + + +add_succ + +add_succ +(a d : ℕ) : a + succ d = succ (a + d) + + + +N->add_succ + + + + + +one_eq_succ_zero + +one_eq_succ_zero +1 = succ 0 + + + +N->one_eq_succ_zero + + + + + +succ_eq_add_one + +succ_eq_add_one +(n : ℕ) : succ n = n + 1 + + + +add_zero->succ_eq_add_one + + + + + +zero_add + +zero_add +(n : ℕ) : 0 + n = n + + + +add_zero->zero_add + + + + + +succ_add + +succ_add +(a b : ℕ) : succ a + b = succ (a + b) + + + +add_zero->succ_add + + + + + +add_comm + +add_comm +(a b : ℕ) : a + b = b + a + + + +add_zero->add_comm + + + + + +add_assoc + +add_assoc +(a b c : ℕ) : a + b + c = a + (b + c) + + + +add_zero->add_assoc + + + + + +le_total + +le_total +(x y : ℕ) : x ≤ y ∨ y ≤ x + + + +add_zero->le_total + + + + + +add_succ->succ_eq_add_one + + + + + +add_succ->zero_add + + + + + +add_succ->succ_add + + + + + +add_succ->add_comm + + + + + +add_succ->add_assoc + + + + + +add_succ->le_total + + + + + +one_eq_succ_zero->succ_eq_add_one + + + + + +le_succ_self + +le_succ_self +(x : ℕ) : x ≤ succ x + + + +succ_eq_add_one->le_succ_self + + + + + +succ_eq_add_one->le_total + + + + + +zero_add->add_comm + + + + + +zero_add->add_assoc + + + + + +zero_le + +zero_le +(x : ℕ) : 0 ≤ x + + + +zero_add->zero_le + + + + + +succ_add->add_comm + + + + + +succ_add->add_assoc + + + + + +succ_add->le_total + + + + + +add_assoc->le_total + + + + + +zero_le->le_total + + + + + +le_succ_self->le_total + + + + + \ No newline at end of file diff --git a/assets/blog/lean_thing.png b/assets/blog/lean_thing.png new file mode 100644 index 0000000..b38be45 Binary files /dev/null and b/assets/blog/lean_thing.png differ diff --git a/assets/blog/numberline.png b/assets/blog/numberline.png new file mode 100644 index 0000000..f6ffb89 Binary files /dev/null and b/assets/blog/numberline.png differ diff --git a/proof.dot b/proof.dot new file mode 100644 index 0000000..df3560c --- /dev/null +++ b/proof.dot @@ -0,0 +1,109 @@ +digraph proof { + compound=true; + rankdir=TB; + node [shape=box, style="rounded,filled", fillcolor="#f0f0f0", + fontname="Helvetica", fontsize=11]; + edge [fontname="Helvetica", fontsize=10]; + + // ── pseudo-states ── + start_top [shape=circle, width=.2, style=filled, fillcolor=black, label=""]; + end_top [shape=doublecircle, width=.15, style=filled, fillcolor=black, label=""]; + + // ── top level ── + G0 [label="x ≤ y ∨ y ≤ x"]; + Z0 [label="x ≤ 0 ∨ 0 ≤ x"]; + Z1 [label="0 ≤ x"]; + + start_top -> G0; + G0 -> Z0 [label="induction y (0)"]; + G0 -> start_succ [label="induction y (succ d, hd)", lhead=cluster_succ]; + Z0 -> Z1 [label="right"]; + Z1 -> end_top [label="exact zero_le x"]; + + // ── succ branch ── + subgraph cluster_succ { + label="succ d (hd : x≤d ∨ d≤x)"; + style=rounded; fontname="Helvetica"; + start_succ [shape=circle, width=.2, style=filled, fillcolor=black, label=""]; + end_succ [shape=doublecircle, width=.15, style=filled, fillcolor=black, label=""]; + + S0 [label="x ≤ succ d ∨ succ d ≤ x"]; + + start_succ -> S0; + S0 -> start_inl [label="cases hd (inl hl)", lhead=cluster_inl]; + S0 -> start_inr [label="cases hd (inr hr)", lhead=cluster_inr]; + + // inl sub-scope + subgraph cluster_inl { + label="inl"; + style=rounded; fontname="Helvetica"; + start_inl [shape=circle, width=.2, style=filled, fillcolor=black, label=""]; + end_inl [shape=doublecircle, width=.15, style=filled, fillcolor=black, label=""]; + + IL0 [label="…∨…\n(hl : x≤d)"]; + IL1 [label="…∨…\n(hc : d = x+c)"]; + IL2 [label="x ≤ succ(x+c) ∨ succ(x+c) ≤ x"]; + IL3 [label="x ≤ succ(x+c)"]; + IL4 [label="x ≤ (x+c)+1"]; + IL5 [label="(x+c)+1 = x+(c+1)"]; + IL6 [label="(x+c)+1 = (x+c)+1"]; + + start_inl -> IL0; + IL0 -> IL1 [label="cases' hl with c hc"]; + IL1 -> IL2 [label="rewrite[hc]"]; + IL2 -> IL3 [label="left"]; + IL3 -> IL4 [label="rewrite[succ_eq_add_one]"]; + IL4 -> IL5 [label="use c+1"]; + IL5 -> IL6 [label="rewrite[← add_assoc]"]; + IL6 -> end_inl [label="rfl"]; + } + + end_inl -> end_succ [ltail=cluster_inl]; + + // inr sub-scope + subgraph cluster_inr { + label="inr"; + style=rounded; fontname="Helvetica"; + start_inr [shape=circle, width=.2, style=filled, fillcolor=black, label=""]; + end_inr [shape=doublecircle, width=.15, style=filled, fillcolor=black, label=""]; + + IR0 [label="…∨…\n(hr : d≤x)"]; + IR1 [label="…∨…\n(hc : x = d+c)"]; + + // c = 0 + RZ0 [label="…∨…\n(hc : x = d+0)"]; + RZ2 [label="…∨…\n(hc : x = d)"]; + RZ3 [label="x ≤ succ d"]; + RZ4 [label="d ≤ succ d"]; + + // c = succ a + RS0 [label="…∨…\n(hc : x = d + succ a)"]; + RS1 [label="…∨…\n(hc : x = succ(d+a))"]; + RS2 [label="succ d ≤ x"]; + RS3 [label="succ d ≤ succ(d+a)"]; + RS4 [label="succ(d+a) = succ d + a"]; + RS5 [label="succ(d+a) = succ(d+a)"]; + + start_inr -> IR0; + IR0 -> IR1 [label="cases' hr with c hc"]; + IR1 -> RZ0 [label="cases c (0)"]; + IR1 -> RS0 [label="cases c (succ a)"]; + + RZ0 -> RZ2 [label="rewrite[add_zero d] at hc"]; + RZ2 -> RZ3 [label="left"]; + RZ3 -> RZ4 [label="rewrite[hc]"]; + RZ4 -> end_inr [label="exact le_succ_self d"]; + + RS0 -> RS1 [label="rewrite[add_succ] at hc"]; + RS1 -> RS2 [label="right"]; + RS2 -> RS3 [label="rewrite[hc]"]; + RS3 -> RS4 [label="use a"]; + RS4 -> RS5 [label="rewrite[succ_add]"]; + RS5 -> end_inr [label="rfl"]; + } + + end_inr -> end_succ [ltail=cluster_inr]; + } + + end_succ -> end_top [ltail=cluster_succ]; +}