update progress electric boogaloo

README.md

@@ -9,3 +9,11 @@ See Index.md for a list of theorems, lemmas and corralary and the small set of p
 To learn Lean and prepare myself, I will read this month _Theorem Proving in Lean 4_.
 
 I will try to continusly update this README.md tracking my advance.
+
+#### 2026-07-30
+
+Lean4 is much more complex than what I thought. Not only I need to learn a new syntax, but also dependent type theory, formal logic and much more.
+
+I also watch a [video](https://www.youtube.com/watch?v=0QZI_m8WZ0Q) and followed step by step. I've learned better than in my few hours of reading _Theorem Proving in Lean 4_ (I switched to the video after not entierly understanding the fifth paragraph of the subchapter "What makes dependent type theory dependent" of the second chapter of the book.
+
+I am bit bored by copying examples and following books. I'm gonna try the same methode I used to learn C and Python. Set myself goals (in this case small basic proofs) and when I don't know or don't understand it google it (I won't use a LLM not because I'm against it, but because I don't want to become reliant on it).

ZeroToLean/Basic.lean

@@ -1 +0,0 @@
-def hello := "world"

ZeroToLean/TheoremProvingInLean4/Chapter01_Introduction/intro.lean

@@ -1,7 +0,0 @@
-namespace Introduction
-  theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
-   fun hpq : p ∧ q =>
-     have hp : p := And.left hpq
-     have hq : q := And.right hpq
-     show q ∧ p from And.intro hq hp
-end Introduction

ZeroToLean/TheoremProvingInLean4/Chapter02_DependentTypeTheory/simplyTypeTheory.lean

@@ -1,152 +0,0 @@
-namespace simpleTypeTheory
-
--- some are pasted from the book and some are just me testing stuff
-
-/- Define some constants. -/ 
-def m : Nat := 1 -- m is a natural number 
-def n : Nat := 0
-def b1 : Bool := true -- b1 is a Boolean 
-def b2 : Bool := false
-/- Check their types. -/ 
-#check m -- output: Nat 
-#check n 
-#check n + 0 -- Nat 
-#check m * (n + 0) -- Nat 
-#check b1 -- Bool 
-#check b1 && b2 -- "&&" is the Boolean and 
-#check b1 || b2 -- Boolean or 
-#check true -- Boolean "true" 
-/- Evaluate -/ 
-#eval 5 * 4 
-#eval m + 2 
-#eval b1 && b2 ------20 3 false
-
-
-def t : Bool := true
-def f : Bool := false
-
-#eval t ∧ f ∨ (t ∨ f)
-
-
-#check Nat → Nat
-#check Nat -> Nat
--- type the arrow as "\to" or "\r"
--- alternative ASCII notation
-#check Nat × Nat
-#check Prod Nat Nat
--- type the product as "\times"
--- alternative notation
-#check Nat → Nat → Nat
-
-#check Nat → (Nat → Nat)
- -- same type as above
-#check Nat × Nat → Nat
-#check (Nat → Nat) → Nat -- a "functional"
-#check Nat.succ
-#check (0, 1)
-#check Nat.add
--- Nat → Nat
--- Nat × Nat
--- Nat → Nat → Nat
-#check Nat.succ 2
- -- Nat
-#check Nat.add 3
- -- Nat → Nat
-#check Nat.add 5 2
- -- Nat
-#check (5, 9).1
- -- Nat
-#check (5, 9).2
- -- Nat
-#eval Nat.succ 2
- -- 3
-#eval Nat.add 5 2
- -- 7
-#eval (5, 9).1
- -- 5
-#eval (5, 9).2
- -- 9
-
-#check Nat
- -- Type
-#check Bool
- -- Type
-#check Nat → Bool
- -- Type
-#check Nat × Bool
- -- Type
-#check Nat → Nat
- -- ...
-#check Nat × Nat → Nat
-#check Nat → Nat → Nat
-#check Nat → (Nat → Nat)
-#check Nat → Nat → Bool
-#check (Nat → Nat) → Nat
-
-
-def α : Type := Nat
-def β : Type := Bool
-def F : Type → Type := List
-def G : Type → Type → Type := Prod
-#check α
- -- Type
-#check F α
- -- Type
-#check F Nat
- -- Type
-#check G α
- -- Type → Type
-#check G α β
- -- Type
-#check G α Nat
- -- Type
-
-
-def α : Type := Nat 
-#check List α -- Type 
-#check List Nat -- Type
-
-#check List
-
-end simpleTypeTheory
-
-namespace FunctionAbstractionAndEvaluation
-#check fun (x : Nat) => x + 5 -- Nat → Nat #check λ (x : Nat) => x + 5 -- λ and fun mean the same thing #check fun x => x + 5 -- Nat inferred #check λ x => x + 5 -- Nat inferred
-
-#eval (λ x : Nat => x + 5) 10 -- 15
-
-#check fun (x : Nat) => x + 5
- -- Nat → Nat
-#check λ (x : Nat) => x + 5
- -- λ and fun mean the same thing
-#check fun x => x + 5
- -- Nat inferred
-#check λ x => x + 5
- -- Nat inferred
-
-def f (n : Nat) : String := toString n
-def g (s : String) : Bool := s.length > 0
-#check fun x : Nat => x
- -- Nat → Nat
-#check fun x : Nat => true
- -- Nat → Bool
-#check fun x : Nat => g (f x)
- -- Nat → Bool
-#check fun x => g (f x)
- -- Nat → Bool
-
- #check fun (g : String → Bool) (f : Nat → String) (x : Nat) => g (f x)
--- (String → Bool) → (Nat → String) → Nat → Bool
-
-#check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x)
-
-#check (fun x : Nat => x) 1
- -- Nat
-#check (fun x : Nat => true) 1
- -- Bool
-#check (fun (α β γ : Type) (u : β → γ) (v : α → β) (x : α) => u (v x)) Nat String Bool g f 0
--- Bool
-
- -- gonna try 10p / day. stopped at 11 Definitions.
-
-end FunctionAbstractionAndEvaluation