43. Every number has a prime factor
Prove that every k ≥ 2 has a prime factor, using the definition of Prime above the editor. Like every problem here it is Mathlib-free: only Lean’s core library is available.
Ordinary induction does not work: the factor of k comes from a divisor of k, not from k - 1. You need strong induction, where the hypothesis covers every smaller number.
This is the key lemma of problem 42, “Infinitely many primes”.
Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.
1def Prime (p : Nat) : Prop := 2 ≤ p ∧ ∀ m, m ∣ p → m = 1 ∨ m = p
2theorem solution (k : Nat) (hk : 2 ≤ k) : ∃ p, Prime p ∧ p ∣ k := by
givenLoading editor…
Type
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
k:Nat
hk:2 ≤ k
⊢∃ p, Prime p ∧ p ∣ k
ReadyLn 1, Col 1Lean 4
Draft saved in this browser