odd_add_oddtheoremProved here from basic factspropext
odd_add_oddLean 4Proved here from basic factsFormally verified
/-- **Direct proof.** The sum of two odd integers is even: if `m = 2a + 1` and `n = 2b + 1`, then`m + n = 2(a + b + 1)`. (Mathlib's `Even k` means `k = r + r` for some `r`.) -/theorem odd_add_odd {m n : ℤ} (hm : Odd m) (hn : Odd n) : Even (m + n) := by obtain ⟨a, rfl⟩ := hm obtain ⟨b, rfl⟩ := hn exact ⟨a + b + 1, by ring⟩
dvd_transtheoremProved here from basic factspropext
dvd_transLean 4Proved here from basic factsFormally verified
/-- **Direct proof.** Divisibility is transitive: if `b = a·k` and `c = b·l` then `c = a·(k·l)`. -/theorem dvd_trans {a b c : ℤ} (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c := by obtain ⟨k, rfl⟩ := hab obtain ⟨l, rfl⟩ := hbc exact ⟨k * l, by ring⟩
even_of_even_sqtheoremProved here from basic factspropext, Classical.choice, Quot.sound
even_of_even_sqLean 4Proved here from basic factsFormally verified
/-- **Proof by contrapositive.** If `n²` is even, then `n` is even. We prove the contrapositiveinstead: if `n` is not even, it is odd, so `n²` is odd (`odd_sq_of_odd`), hence not even. -/theorem even_of_even_sq (n : ℤ) (h : Even (n ^ 2)) : Even n := by by_contra hn have hodd : Odd (n ^ 2) := odd_sq_of_odd (Int.not_even_iff_odd.mp hn) exact (Int.not_even_iff_odd.mpr hodd) h
even_of_even_sq_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
even_of_even_sq_libraryLean 4Applies a library theoremFormally verified
/-- The same theorem from Mathlib's `Int.even_pow : Even (m ^ n) ↔ Even m ∧ n ≠ 0`. -/theorem even_of_even_sq_library (n : ℤ) (h : Even (n ^ 2)) : Even n := (Int.even_pow.mp h).1
exists_prime_not_memtheoremProved here from basic factspropext, Classical.choice, Quot.sound
exists_prime_not_memLean 4Proved here from basic factsFormally verified
/-- **Euclid's theorem.** Every finite set `S` of primes misses some prime.Let `N = (∏ p ∈ S, p) + 1` and let `q` be the smallest factor of `N` that is bigger than `1`(it is prime). If `q` were in `S`, it would divide both the product and `N`, hence theirdifference `1` — a contradiction. Note that `N` itself need not be prime. -/theorem exists_prime_not_mem (S : Finset ℕ) (hS : ∀ p ∈ S, p.Prime) : ∃ q, q.Prime ∧ q ∉ S := by have hpos : 0 < ∏ p ∈ S, p := Finset.prod_pos fun p hp => (hS p hp).pos have hN : (∏ p ∈ S, p) + 1 ≠ 1 := by omega refine ⟨Nat.minFac ((∏ p ∈ S, p) + 1), Nat.minFac_prime hN, fun hmem => ?_⟩ have hdvd_prod : Nat.minFac ((∏ p ∈ S, p) + 1) ∣ ∏ p ∈ S, p := Finset.dvd_prod_of_mem _ hmem have hdvd_N := Nat.minFac_dvd ((∏ p ∈ S, p) + 1) have hdvd_one : Nat.minFac ((∏ p ∈ S, p) + 1) ∣ 1 := (Nat.dvd_add_right hdvd_prod).mp hdvd_N exact (Nat.minFac_prime hN).one_lt.ne' (Nat.dvd_one.mp hdvd_one)
exists_infinite_primestheoremApplies a library theorempropext, Classical.choice, Quot.sound
exists_infinite_primesLean 4Applies a library theoremFormally verified
/-- There are primes as large as we like: Mathlib's `Nat.exists_infinite_primes`, proved withthe smallest prime factor of `n! + 1`. -/theorem exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ p.Prime := Nat.exists_infinite_primes n
sq_eq_two_mul_sqtheoremProved here from basic factspropext, Classical.choice, Quot.sound
sq_eq_two_mul_sqLean 4Proved here from basic factsFormally verified
/-- **√2 is irrational**, in the form: if `a² = 2b²` for natural numbers `a, b`, then `b = 0`.Proof by *infinite descent* (strong induction on `b`): `a²` is even, so `a = 2c`; then `b² = 2c²`,so `b = 2d`; then `c² = 2d²` is a smaller solution, and by the induction hypothesis `d = 0`, so`b = 0`. (Evenness of a square is Mathlib's `Nat.even_pow`; the lesson proves it as Theorem 4.) -/theorem sq_eq_two_mul_sq (a b : ℕ) (h : a ^ 2 = 2 * b ^ 2) : b = 0 := by induction b using Nat.strong_induction_on generalizing a with | _ b ih => have ha : Even a := (Nat.even_pow.mp ⟨b ^ 2, by rw [h]; ring⟩).1 obtain ⟨c, rfl⟩ := ha have hb2 : b ^ 2 = 2 * c ^ 2 := by nlinarith have hb : Even b := (Nat.even_pow.mp ⟨c ^ 2, by rw [hb2]; ring⟩).1 obtain ⟨d, rfl⟩ := hb have hc : c ^ 2 = 2 * d ^ 2 := by nlinarith by_contra hne have hd : d = 0 := ih d (by omega) c hc omega
gauss_sum_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
gauss_sum_libraryLean 4Applies a library theoremFormally verified
/-- Mathlib's version, `Finset.sum_range_id_mul_two : (∑ i ∈ range n, i) * 2 = n * (n - 1)`. -/theorem gauss_sum_library (n : ℕ) : (∑ i ∈ range n, i) * 2 = n * (n - 1) := sum_range_id_mul_two n
sum_oddtheoremProved here from basic factspropext, Classical.choice, Quot.sound
sum_oddLean 4Proved here from basic factsFormally verified
/-- **The odd numbers add up to squares:** `1 + 3 + ⋯ + (2n − 1) = n²`, by induction.The inductive step is `n² + (2n + 1) = (n + 1)²`. -/theorem sum_odd (n : ℕ) : ∑ i ∈ range n, (2 * i + 1) = n ^ 2 := by induction n with | zero => rfl | succ n ih => rw [sum_range_succ, ih]; ring
stampstheoremProved here from basic factspropext, Quot.sound
stampsLean 4Proved here from basic factsFormally verified
/-- **Strong induction.** Every whole number `n ≥ 8` is a sum of 3s and 5s.The cases `8 = 3 + 5`, `9 = 3 + 3 + 3` and `10 = 5 + 5` start things off; for `n ≥ 11` thenumber `n − 3 ≥ 8` is smaller, so (strong induction hypothesis) it is `3a + 5b`, and then`n = 3(a + 1) + 5b`. The step reaches back *three* places, which ordinary induction cannot dodirectly. -/theorem stamps (n : ℕ) (hn : 8 ≤ n) : ∃ a b : ℕ, n = 3 * a + 5 * b := by induction n using Nat.strong_induction_on with | _ n ih => rcases (show n = 8 ∨ n = 9 ∨ n = 10 ∨ 11 ≤ n by omega) with h | h | h | h · exact ⟨1, 1, by omega⟩ · exact ⟨3, 0, by omega⟩ · exact ⟨0, 2, by omega⟩ · obtain ⟨a, b, hab⟩ := ih (n - 3) (by omega) (by omega) exact ⟨a + 1, b, by omega⟩
false_step_holdstheoremProved here from basic factspropext
false_step_holdsLean 4Proved here from basic factsFormally verified
/-- A **fake induction**: *if* `n² + n + 1` were even, *then* `(n + 1)² + (n + 1) + 1` would beeven too, because the second number is the first plus `2(n + 1)`. The inductive step is fine… -/theorem false_step_holds (n : ℕ) (h : Even (n ^ 2 + n + 1)) : Even ((n + 1) ^ 2 + (n + 1) + 1) := by have e : (n + 1) ^ 2 + (n + 1) + 1 = (n ^ 2 + n + 1) + 2 * (n + 1) := by ring rw [e] exact h.add (even_two_mul (n + 1))
never_eventheoremProved here from basic factspropext, Classical.choice, Quot.sound
never_evenLean 4Proved here from basic factsFormally verified
/-- …but the base case fails, and in fact the claim is false for **every** `n`: `n² + n = n(n + 1)`is even (it is a product of consecutive numbers), so `n² + n + 1` is odd. -/theorem never_even (n : ℕ) : ¬ Even (n ^ 2 + n + 1) := by have h : Even (n * (n + 1)) := Nat.even_mul_succ_self n have e : n ^ 2 + n + 1 = n * (n + 1) + 1 := by ring rw [e, Nat.even_add_one] exact not_not.mpr h
/-- The principle of **ordinary induction** for `ℕ`, stated as a proposition. -/def OrdinaryInduction : Prop := ∀ P : ℕ → Prop, P 0 → (∀ n, P n → P (n + 1)) → ∀ n, P n
/-- The principle of **strong induction**: if `P n` follows whenever `P k` holds for all `k < n`,then `P n` holds for every `n`. (No separate base case: for `n = 0` there are no `k < 0`.) -/def StrongInduction : Prop := ∀ P : ℕ → Prop, (∀ n, (∀ k < n, P k) → P n) → ∀ n, P n
/-- The **well-ordering principle**: every non-empty set of natural numbers has a least element. -/def WellOrdering : Prop := ∀ S : Set ℕ, S.Nonempty → ∃ m ∈ S, ∀ k ∈ S, m ≤ k
ordinaryInduction_holdstheoremApplies a library theoremNo axioms
ordinaryInduction_holdsLean 4Applies a library theoremFormally verified
/-- Ordinary induction holds: it is the recursor `Nat.rec` that comes with the definition of `ℕ`. -/theorem ordinaryInduction_holds : OrdinaryInduction := fun _ h0 hs n => Nat.rec h0 hs n
strong_of_ordinarytheoremProved here from basic factsNo axioms
strong_of_ordinaryLean 4Proved here from basic factsFormally verified
/-- **Ordinary ⇒ strong induction.** Apply ordinary induction to the stronger statement`Q n := ∀ k < n, P k`. `Q 0` is vacuous; and if `Q n` holds then `P n` holds by the hypothesis,so `Q (n + 1)` holds. Finally `P n` follows from `Q (n + 1)`.(All three principles are theorems about `ℕ` in Lean; what these proofs show is that each one canbe *derived* from the previous one, using only basic arithmetic facts.) -/theorem strong_of_ordinary (ind : OrdinaryInduction) : StrongInduction := by intro P h n have hQ : ∀ m, ∀ k < m, P k := by refine ind (fun m => ∀ k < m, P k) (fun k hk => absurd hk (Nat.not_lt_zero k)) ?_ intro m hm k hk rcases Nat.lt_succ_iff_lt_or_eq.mp hk with hlt | heq · exact hm k hlt · rw [heq]; exact h m hm exact hQ (n + 1) n (Nat.lt_succ_self n)
wellOrdering_of_strongtheoremProved here from basic factspropext, Classical.choice, Quot.sound
wellOrdering_of_strongLean 4Proved here from basic factsFormally verified
/-- **Strong induction ⇒ well-ordering.** Suppose `S` had no least element. By strong induction,no `n` is in `S`: if all `k < n` are outside `S` and `n ∈ S`, then `n` would be the least element.So `S` is empty, contradicting the hypothesis. -/theorem wellOrdering_of_strong (sind : StrongInduction) : WellOrdering := by intro S hne by_contra hno push Not at hno have hout : ∀ n, n ∉ S := by refine sind (fun n => n ∉ S) ?_ intro n ih hn obtain ⟨k, hkS, hkn⟩ := hno n hn exact ih k hkn hkS obtain ⟨x, hx⟩ := hne exact hout x hx
ordinary_of_wellOrderingtheoremProved here from basic factspropext, Classical.choice, Quot.sound
ordinary_of_wellOrderingLean 4Proved here from basic factsFormally verified
/-- **Well-ordering ⇒ ordinary induction.** If `P 0` and `P n → P (n + 1)`, but `P` failedsomewhere, let `m` be the *least* failure. `m ≠ 0` because `P 0` holds, so `m = j + 1`; and `j < m`means `P j` holds, hence `P (j + 1) = P m` holds — a contradiction. -/theorem ordinary_of_wellOrdering (wo : WellOrdering) : OrdinaryInduction := by intro P h0 hs n by_contra hn obtain ⟨m, hm, hmin⟩ := wo {k | ¬ P k} ⟨n, hn⟩ cases m with | zero => exact hm h0 | succ j => have hj : P j := by by_contra hj have := hmin j hj omega exact hm (hs j hj)
/-- A direct proof: the sum of two odd integers is even.Hint: `obtain ⟨a, rfl⟩ := hm` unpacks `m = 2 * a + 1`; then give the witness for `Even`(`Even k` means `k = r + r`) and finish with `ring`. -/theorem odd_add_odd {m n : ℤ} (hm : Odd m) (hn : Odd n) : Even (m + n) := by sorry
Show the compiled solution
odd_add_oddLean 4Proved here from basic factsFormally verified
/-- **Direct proof.** The sum of two odd integers is even: if `m = 2a + 1` and `n = 2b + 1`, then`m + n = 2(a + b + 1)`. (Mathlib's `Even k` means `k = r + r` for some `r`.) -/theorem odd_add_odd {m n : ℤ} (hm : Odd m) (hn : Odd n) : Even (m + n) := by obtain ⟨a, rfl⟩ := hm obtain ⟨b, rfl⟩ := hn exact ⟨a + b + 1, by ring⟩
/-- Induction: the first `n` odd numbers add up to `n²`.Hint: `induction n with | zero => rfl | succ n ih => ?_`, then `rw [sum_range_succ, ih]` and`ring`. -/theorem sum_odd (n : ℕ) : ∑ i ∈ range n, (2 * i + 1) = n ^ 2 := by sorry
Show the compiled solution
sum_oddLean 4Proved here from basic factsFormally verified
/-- **The odd numbers add up to squares:** `1 + 3 + ⋯ + (2n − 1) = n²`, by induction.The inductive step is `n² + (2n + 1) = (n + 1)²`. -/theorem sum_odd (n : ℕ) : ∑ i ∈ range n, (2 * i + 1) = n ^ 2 := by induction n with | zero => rfl | succ n ih => rw [sum_range_succ, ih]; ring