Number theory proof

Stream: new members

[Alex Gu]

I'm learning how to write Number Theory proofs in Lean, and was stuck with this example:

theorem not_exists_prime_8_pow_plus_47 : ¬∃ n : ℕ, (8^n + 47).Prime := by sorry

Here is the proof in natural language: we do a proof by contradiction.

• If n = 0 (mod 2), then taking (mod 3) gives 8^n+47 = (-1)^n+(-1) = 0 (mod 3)
• If n = 1 (mod 4), then taking (mod 5) gives 8^n+47 = (-2)^(4k+1)+2 = -2 * (16^k) + 2 = 0 (mod 5)
• If n = 3 (mod 4), then taking (mod 13) gives 8^n+47 = 8^(4k+3)+8 = 4096^k*512+8=5 + 8 = 0 (mod 13)

Could anyone help me with how one might express this in Lean? Pointers to some examples of number theory proofs (I read through the ones in MIL) would also be super appreciated. Thanks!

[Ruben Van de Velde]

Maybe this is a start:

import Mathlib
theorem not_exists_prime_8_pow_plus_47 : ¬∃ n : ℕ, (8^n + 47).Prime := by
  rintro ⟨n, hn⟩
  have : n % 4 < 4 := Nat.mod_lt n (by norm_num)
  interval_cases h : n % 4

  all_goals sorry

but you might need to convert the hypothesis h to another formulation for the smoothest proof

[Alex Gu]

I'm getting stuck at some steps like proving 4096 ^ k ≡ 1 [ZMOD 3], is there some simple tactic for this?

[Edward van de Meent]

i thiink you'd want to use (8:ZMod 3) ^ n + -1 = 0

[Edward van de Meent]

i think that will have better reasoning about exponentiation n stuff.

[Alex Gu]

I'm trying like this, starting from where @Ruben Van de Velde left off:

  · have h (k : ℕ): (8:ZMod 3)^(4*k) + 47 = 0 := by
      rw [pow_mul]
      norm_num

The state is ⊢ 4096 ^ k + 47 = 0, how do I do this?

[Daniel Weber]

Does reduce_mod_char work?

[Alex Gu]

How can I express that if n % 4 = 1, then there exists k such that n = 4*k+1?

[Daniel Weber]

docs#Nat.div_add_mod

[Alex Gu]

I got here so far but not sure how to finish this case, any advice? :sweat_smile:

theorem not_exists_prime_8_pow_plus_47 : ¬∃ n : ℕ, (8^n + 47).Prime := by
  rintro ⟨n, hn⟩
  have : n % 4 < 4 := Nat.mod_lt n (by norm_num)
  interval_cases h : n % 4
  · have h0 : n = 4 * (n / 4) := by
      nth_rewrite 1 [← Nat.div_add_mod n 4]
      rw [h]
      ring

    have h1 (k : ℕ): (8:ZMod 3)^(4*k) + 47 = 0 := by
      rw [pow_mul]
      norm_num
      reduce_mod_char
      rw [one_pow]
      reduce_mod_char

[Kevin Buzzard]

Here's how I'd do the first one:

import Mathlib

-- helper lemma
lemma aux {n : ℕ} (hn : 2 ∣ n) : 3 ∣ 8^n + 47 := by
  rw [dvd_iff_exists_eq_mul_right] at hn
  obtain ⟨m, rfl⟩ := hn
  rw [← Fin.natCast_eq_zero, pow_mul]
  push_cast
  rw [one_pow]
  norm_num
  simp

theorem not_exists_prime_8_pow_plus_47 : ¬∃ n : ℕ, (8^n + 47).Prime := by
  rintro ⟨n, hn⟩
  have : n % 4 < 4 := Nat.mod_lt n (by norm_num)
  interval_cases h : n % 4
  · have h0 : n = 4 * (n / 4) := by
      nth_rewrite 1 [← Nat.div_add_mod n 4]
      rw [h]
      ring
    have h1 : 2 ∣ n := ⟨2 * (n / 4), by linear_combination h0⟩
    exact Nat.not_prime_of_dvd_of_lt (aux h1) (by norm_num) (by norm_num) hn
  · sorry
  · sorry
  · sorry

[Alex Gu]

I was able to solve most of the proof, but got stuck at this last step. Any wisdom here?

lemma aux2 {n : ℕ} (hn : 4 ∣ (n - 3)) : 13 ∣ 8^n + 47 := by
  rw [dvd_iff_exists_eq_mul_right] at hn
  obtain ⟨m, p⟩ := hn
  have h : n = 4 * m + 3 := by sorry
  rw [h]
  rw [← Fin.natCast_eq_zero]
  rw [pow_add]
  rw [pow_mul]
  push_cast
  rw [one_pow]
  norm_num
  simp

[Heather Macbeth]

Have you considered taking a modular arithmetic approach? This seems more natural to me:

import Mathlib.Data.ZMod.Basic

example {n : ℕ} (hn : n % 4 = 3) : 8^n ≡ -47 [ZMOD 13] := by
  calc (8:ℤ) ^ n = 8 ^ (4 * (n / 4) + (n % 4)) := by rw [Nat.div_add_mod]
    _ = (8 ^ 4) ^ (n / 4) * 8 ^ 3 := by rw [pow_add, pow_mul, hn]
    _ ≡ 1 ^ (n/4) * (-47) [ZMOD 13] := by gcongr <;> decide
    _ = -47 := by ring

[Heather Macbeth]

By the way, your previous statement is incorrect. Natural number subtraction is unpredictable! :)

example : ¬ ∀ {n : ℕ} (hn : 4 ∣ (n - 3)), 13 ∣ 8^n + 47 := by
  push_neg
  use 0
  decide

[Alex Gu]

Sorry to ask so many questions, but how could I connect this with what I have so far? Specifically, how can I reconcile **hn** : Nat.Prime (8 ^ n + 47) with lemma aux1 {n : ℕ} (hn : n % 4 = 1) : 8^n ≡ -47 [ZMOD 5]?

And also, is there anywhere I could get a deeper dive on how to use Zmod? I couldn't find it in TPIL or MIL :sweat_smile:

[Ruben Van de Velde]

I think the next steps are:

1. 8^n + 47 ≡ 0 [ZMOD 5]
2. 5 ∣ 8^n + 47
3. 8^n + 47 ≠ 5
4. If a prime divides another prime, they must be equal
5. ... but they're not, so you're done

I suggest you try to solve each of those individually