Last active
March 24, 2021 15:14
-
-
Save kbuzzard/27e5e3d522bc34a20df61933d2e58b3d to your computer and use it in GitHub Desktop.
some Lean maths puzzles
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import tactic | |
import data.real.basic | |
/- | |
# Some puzzles. | |
1) (easy logic). If `P`, `Q` and `R` are true-false statements, then show | |
that `(P → (Q → R)) → ((P → Q) → (P → R))` (where `→` means "implies") | |
2) (group theory) If `G` is a group such that `∀ g, g^2 = 1` | |
then `G` is abelian. | |
3) (analysis) A set of reals has at most one least upper bound. | |
4) (linear orders) If `(a, b]` denotes the set of reals `x` with `a < x ≤ b` then | |
prove `[a,b) ∪ [b,c) ∪ [c,a) = [b,a) ∪ [c,b) ∪ [a,c)` | |
5) (group theory) If `G` is a group and `g : G`, and if `g^a = g^b = 1` with `a` | |
and `b` integers, then `g^(gcd a b) = 1` | |
6) (number theory) Prove there's a nontrivial solution to `a^2-94b^2=1` in integers. | |
7) (analysis) : If `aₙ → l` and `cₙ → l` and `aₙ ≤ bₙ ≤ cₙ` then `bₙ → l` | |
-/ | |
section Q1 | |
variables (P Q R : Prop) | |
example : (P → (Q → R)) → ((P → Q) → (P → R)) := | |
begin | |
sorry | |
end | |
end Q1 | |
section Q2 | |
variables (G : Type) [group G] | |
example : (∀ (g : G), g^2 = 1) → (∀ g h : G, g * h = h * g) := | |
begin | |
sorry | |
end | |
end Q2 | |
section Q3 | |
/- | |
def upper_bounds (S : set ℝ) : set ℝ := { b | ∀s ∈ S, s ≤ b } | |
def lower_bounds (S : set ℝ) : set ℝ := { b | ∀s ∈ S, b ≤ s } | |
def is_least (S : set ℝ) (l : ℝ) : Prop := l ∈ S ∧ l ∈ lower_bounds S | |
def is_lub (S : set ℝ) (l : ℝ) : Prop := is_least (upper_bounds S) l | |
-/ | |
/-- A set has at most one least upper bound -/ | |
example (S : set ℝ) (a b : ℝ) (ha : is_lub S a) (hb : is_lub S b) : a = b := | |
begin | |
sorry | |
end | |
end Q3 | |
section Q4 | |
variables (a b c : ℝ) | |
open set | |
example : Ico a b ∪ Ico b c ∪ Ico c a = Ico b a ∪ Ico c b ∪ Ico a c := | |
begin | |
sorry | |
end | |
end Q4 | |
section Q5 | |
variables (G : Type) [group G] (a b : ℤ) (g : G) | |
open int | |
example : g^a = 1 ∧ g^b = 1 → g^(gcd a b) = 1 := | |
begin | |
sorry | |
end | |
end Q5 | |
section Q6 | |
example : ∃ a b : ℤ, b ≠ 0 ∧ a^2 - 94*b^2 = 1 := | |
begin | |
sorry | |
end | |
end Q6 | |
section Q7 | |
-- l is the limit of aₙ if ∀ ε>0 ∃ N, n ≥ N → |aₙ - l| < ε | |
def is_limit (a : ℕ → ℝ) (l : ℝ) := | |
∀ ε > 0, ∃ N, ∀ n, N ≤ n → abs (a n - l) < ε | |
example (a b c : ℕ → ℝ) (h : ∀ n, a n ≤ b n ∧ b n ≤ c n) (l : ℝ) | |
(ha : is_limit a l) (hc : is_limit c l) : is_limit b l := | |
begin | |
sorry | |
end | |
end Q7 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment