new: Initial commit

.gitignore

@@ -0,0 +1,2 @@
+/.lake
+.directory

Lean Talk SP24.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `«Lean Talk SP24»` library.
+-- Import modules here that should be built as part of the library.
+import «Lean Talk SP24».basics

Lean Talk SP24/basics.lean

@@ -0,0 +1,59 @@
+import Mathlib.Data.Nat.Basic
+import Mathlib.Data.Nat.Parity
+import Mathlib.Tactic
+
+open Nat
+
+-- Obligatory Hello World
+#eval "Hello world!"
+
+-- These are pieces of data.
+#check 2 + 2
+
+def f (x : ℕ) :=
+  x + 3
+
+#check f
+
+-- These are propositions, of type `Prop`.
+#check 2 + 2 = 4
+
+def FermatLastTheorem :=
+  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n
+
+#check FermatLastTheorem
+
+-- These are proofs of propositions.
+theorem easy : 2 + 2 = 4 :=
+  rfl
+
+#check easy
+
+theorem hard : FermatLastTheorem :=
+  sorry
+
+#check hard
+
+-- Here are some proofs.
+example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k + k)⟩ =>
+  have hmn : m * n = m * k + m * k := by rw [hk, mul_add]
+  show ∃ l, m * n = l + l from ⟨_, hmn⟩
+
+example : ∀ m n : Nat, Even n → Even (m * n) :=
+fun m n ⟨k, hk⟩ => ⟨m * k, by rw [hk, mul_add]⟩
+
+example : ∀ m n : Nat, Even n → Even (m * n) := by
+  -- say m and n are natural numbers, and assume n=2*k
+  rintro m n ⟨k, hk⟩
+  -- We need to prove m*n is twice a natural number. Let's show it's twice m*k.
+  use m * k
+  -- substitute in for n
+  rw [hk]
+  -- and now it's obvious
+  ring
+
+example : ∀ m n : Nat, Even n → Even (m * n) := by
+  rintro m n ⟨k, hk⟩; use m * k; rw [hk]; ring
+
+example : ∀ m n : Nat, Even n → Even (m * n) := by
+  intros; simp [*, parity_simps]

lake-manifest.json

@@ -0,0 +1,68 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "276953b13323ca151939eafaaec9129bf7970306",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "rev": "6beed82dcfbb7731d173cd517675df27d62ad0f4",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "rev": "af1e86cf7a37389632a02f4a111e6b501b2b818f",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.27",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "328b7ecbc986507635abf725bbed4da70e418298",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "«Lean Talk SP24»",
+ "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,17 @@
+import Lake
+open Lake DSL
+
+package «Lean Talk SP24» where
+  -- Settings applied to both builds and interactive editing
+  leanOptions := #[
+    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
+    ⟨`pp.proofs.withType, false⟩
+  ]
+  -- add any additional package configuration options here
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"
+
+@[default_target]
+lean_lib «Lean Talk SP24» where
+  -- add any library configuration options here

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.6.0-rc1