diff --git a/README.md b/README.md index 6a62093..8d34705 100644 --- a/README.md +++ b/README.md @@ -85,25 +85,38 @@ run any other file inside `src/example/` following its command inside `Makefile` #### my notes - [basics](docs/basic_concepts.md) +- [formal veification](docs/formal_verification.md)
-#### learning lean +#### learning lean and theorem proving -- โœ… [learn Lean from lean-lang.org](https://lean-lang.org/documentation/0) +- โœ… [learn Lean from lean-lang.org](https://lean-lang.org/documentation/) +- โœ… [Lean prover community](https://leanprover-community.github.io/) - ๐ŸŸก [Lean 4 documentation](https://leanprover.github.io/lean4/doc/) - ๐ŸŸก [mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html) - ๐ŸŸก [theorem proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4/) +- ๐ŸŸก [the matrix cookbook](https://www.math.uwaterloo.ca/~hwolkowi/matrixcookbook.pdf) with [code](https://github.com/eric-wieser/lean-matrix-cookbook) +- ๐ŸŸก [the Lean 4 theorem prover and programming language](https://lean-lang.org/papers/lean4.pdf) +- ๐ŸŸก [an extensible theorem proving frontend](https://lean-lang.org/papers/thesis-sebastian.pdf) +- ๐ŸŸก [a metaprogramming framework for formal verification](https://lean-lang.org/papers/tactic.pdf)
#### useful - [vscode/cursor plugin](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4) +- [mathlib algebra methods ref](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Defs.html#Group) +- [zulip Lean channel](https://leanprover.zulipchat.com/) +- [moogle.ai (find theorems)](https://www.moogle.ai/)
#### applied examples +- [Lean prover community's blog](https://leanprover-community.github.io/blog/) and [projects](https://leanprover-community.github.io/lean_projects.html) +- [social choice theory in Lean (code)](https://github.com/asouther4/lean-social-choice?tab=readme-ov-file) +- [the deep link equating math proofs and computer programs](https://www.quantamagazine.org/the-deep-link-equating-math-proofs-and-computer-programs-20231011/) + - *"types are fundamentally equivalent to logical propositions"* - [AI safety via debate, by g. irving et al (2018)](https://arxiv.org/pdf/1805.00899) - *"in the debate game, it is harder to lie than to refute a lie."* \ No newline at end of file diff --git a/docs/basic_concepts.md b/docs/basic_concepts.md index f600ae2..808199e 100644 --- a/docs/basic_concepts.md +++ b/docs/basic_concepts.md @@ -369,6 +369,10 @@ def twice (f : Nat โ†’ Nat) (a : Nat) := f (f a)
+* for instance, `(ยท + 2)` is syntax sugar for `(fun x => x + 2)` + +
+ --- ## namespaces diff --git a/docs/formal_verification.md b/docs/formal_verification.md new file mode 100644 index 0000000..ef0c552 --- /dev/null +++ b/docs/formal_verification.md @@ -0,0 +1,46 @@ +# formal verification + +
+ +## tl; dr + +
+ +* formal methods are a set of techniques and specialized tools used to specify, design, and verify +complex systems with mathematical rigor + - 1. specify: describe a system's desired behavior precisely + - 2. design: develop system components with assurance they'll work as intended + - 3. verify: prove or provide evidence that a system meets its specification + +
+ +--- + +## proof assistant + +
+ +* a piece of software that provides a language for defining objects, specifying properties of these objects, and proving that these specifications hold (i.e., the system checks that these proofs are correct down to their logical foundation) +* in a formalization, all definitions are precisely specified and all proofs are virtually guaranteed to be correct. + +
+ +

+ +

+ +
+ +--- + +## proving methods + +
+ +### rfl + +
+ +* reflexivity of equality: anything is equal to itself +* `rfl` stands for reflexivity, a fundamental concept and a very common tactic used in proofs +* in Lean's type theory, equality is an inductive type, and `Eq.refl` a is the constructor for proving` a = a` diff --git a/docs/images/proof_assistant.png b/docs/images/proof_assistant.png new file mode 100644 index 0000000..5a38ddd Binary files /dev/null and b/docs/images/proof_assistant.png differ diff --git a/src/proofs/DefiningEvenNumber.lean b/src/proofs/DefiningEvenNumber.lean new file mode 100644 index 0000000..d07cd28 --- /dev/null +++ b/src/proofs/DefiningEvenNumber.lean @@ -0,0 +1,128 @@ +import Mathlib.Data.Nat.Basic + +/- +## +## I. defining what an "even" number is +## +-/ + +-- we define a new `inductive` type called `Even` +-- an inductive type allows us to define a data type by specifying its constructors +-- here, we say that a number `n` is `Even` if: +-- 1. `Even.zero` : 0 is even +-- 2. `Even.add_two` : if `k` is even, then `k + 2` is also even +inductive Even : Nat โ†’ Prop + | zero : Even 0 + | add_two {k : Nat} (hk : Even k) : Even (k + 2) + + +/- +## +## II. proving a simple property about even numbers +## +-/ + +-- our goal is to prove the following theorem: +-- if a number `n` is even, then `n + 2` is also even +theorem even_add_two_is_even {n : Nat} (hn : Even n) : Even (n + 2) := by + -- we have `hn : Even n` in our context + -- our goal is `Even (n + 2)` + -- since `Even` is an inductive type, we can use `induction` on `hn`. + -- this means we'll prove the statement for each constructor of `Even` + induction hn with + | zero => + -- case 1: `n` is `0`. + -- our goal is now `Even (0 + 2)`, which simplifies to `Even 2` + -- we can prove this directly using the `Even.add_two` constructor + -- we need to show that `Even 0` holds, which is true by `Even.zero` + apply Even.add_two + apply Even.zero + | add_two k hk ih => + -- case 2: `n` is of the form `k + 2`, where `hk : Even k` + -- and `ih` is our inductive hypothesis: `Even (k + 2)` implies `Even ((k + 2) + 2)` + -- the inductive hypothesis `ih` is actually `Even (k + 2)` implies `Even (k + 2 + 2)` + -- `ih` will be a proof of our goal for `k` so `ih : Even (k + 2)` + -- our goal is `Even ((k + 2) + 2)` + -- we can use `Even.add_two` again + -- to apply `Even.add_two`, we need a proof that `Even (k + 2)` holds (our inductive hypothesis `ih`) + apply Even.add_two + assumption -- this tactic tries to find a proof of the current goal among the hypotheses + -- in this case, `ih` is exactly `Even (k + 2)` + + +/- +## +## III. using the theorem +## +-/ + +example : Even 4 := by + -- we know 0 is even + have h0 : Even 0 := Even.zero + -- then 2 is even (0 + 2) + have h2 : Even 2 := Even.add_two h0 + -- then 4 is even (2 + 2) + exact Even.add_two h2 + + +-- another way to prove `Even 4` using our theorem `even_add_two_is_even` +example : Even 4 := by + -- we know `Even 0`. + have h0 : Even 0 := Even.zero + -- apply `even_add_two_is_even` to `h0` to get `Even (0 + 2)`, i.e., `Even 2` + have h2 : Even 2 := even_add_two_is_even h0 + -- apply `even_add_two_is_even` to `h2` to get `Even (2 + 2)`, i.e., `Even 4` + exact even_add_two_is_even h2 + + +/- +## +## IV. a slightly more complex definition and proof +## +-/ + +-- let's define addition for natural numbers +-- let's assume `add_zero` and `add_succ` are axioms for now +-- let's define what it means for a number to be "odd": +-- a number `n` is `Odd` if `n = k + 1` for some even `k` +def Odd (n : Nat) : Prop := โˆƒ k, Even k โˆง n = k + 1 + +-- prove that if `n` is odd, then `n + 2` is also odd +theorem odd_add_two_is_odd {n : Nat} (hn : Odd n) : Odd (n + 2) := by + -- our hypothesis `hn` is `Odd n`, which means `โˆƒ k, wven k โˆง n = k + 1` + -- we can `rcases` this hypothesis to get `k` and its properties + rcases hn with โŸจk, hk_even, hk_nโŸฉ + -- `k : Nat` + -- `hk_even : Even k` + -- `hk_n : n = k + 1` + + -- our goal is `Odd (n + 2)` + -- by definition, this means `โˆƒ m, Even m โˆง (n + 2) = m + 1` + + -- let's substitute `n = k + 1` into the goal + -- the goal becomes `Odd ((k + 1) + 2)`, which simplifies to `Odd (k + 3)` + -- we need to find an `m` such that `Even m` and `k + 3 = m + 1` + -- if we choose `m = k + 2`, then `k + 3 = (k + 2) + 1` is true + -- so we need to show `Even (k + 2)` + + -- we know `hk_even : Even k` + -- we can use our previously proven theorem `even_add_two_is_even` to show `Even (k + 2)` + have hk_plus_2_even : Even (k + 2) := even_add_two_is_even hk_even + + -- now we have `hk_plus_2_even : Even (k + 2)` + -- we want to show `โˆƒ m, Even m โˆง (n + 2) = m + 1` + -- let `m := k + 2` + -- we use `exists.intro` to provide the witness `k + 2` + exists (k + 2) + -- now our goal is `Even (k + 2) โˆง (n + 2) = (k + 2) + 1` + -- we can `split` the goal into two subgoals + constructor + -- subgoal 1: `Even (k + 2)` + exact hk_plus_2_even + -- subgoal 2: `(n + 2) = (k + 2) + 1` + -- we know `n = k + 1`, lets rewrite: + rw [hk_n] + -- goal becomes `(k + 1) + 2 = (k + 2) + 1` + -- this is true by associativity and commutativity of addition + -- lean's simplifier `simp` can usually handle such arithmetic equalities + simp diff --git a/src/proofs/FermatLastTheorem.lean b/src/proofs/FermatLastTheorem.lean index 9edd28d..f85300e 100644 --- a/src/proofs/FermatLastTheorem.lean +++ b/src/proofs/FermatLastTheorem.lean @@ -1,6 +1,9 @@ /- ## ## for the lolz +## https://leanprover-community.github.io/blog/posts/FLT-announcement/ +## https://github.com/leanprover-community/flt-regular +## https://leanprover-community.github.io/flt-regular/blueprint/ ## -/