Help with Lean coding

Stream: new members

[Kajani Kaunda]

Hello,

1. Theorem prime_form_6n_plus_1_or_6n_minus_1 proves that all primes p > 3 can be expressed in the form (6y ± 1).
2. How can I use prime_form_6n_plus_1_or_6n_minus_1 to prove/state that there are infinitely many n such that (6n ± 1) is prime.

theorem prime_form_6n_plus_1_or_6n_minus_1 (p : ℕ) (hprime : Nat.Prime p) (hp : 3 < p) :
    ∃ n, (p = 6 * n + 1 ∨ p = 6 * n - 1) := by
  suffices p % 6 = 1 ∨ p % 6 = 5 by
    obtain hp | hp := this
    · use p / 6
      left
      omega
    · use (p / 6 + 1)
      right
      omega
  have : p % 6 < 6 := Nat.mod_lt _ (by norm_num)
  have : p ≠ 2 := by linarith
  have : p ≠ 3 := by linarith
  have : p ≠ 6 := by rintro rfl; norm_num at hprime
  interval_cases hr : p % 6 <;> first | omega | (exfalso; revert hr)
  · rw [← Nat.dvd_iff_mod_eq_zero, Nat.dvd_prime hprime]
    aesop
  · refine ne_of_apply_ne (· % 2) ?_
    dsimp
    rw [Nat.mod_mod_of_dvd _ (by norm_num), ← Nat.dvd_iff_mod_eq_zero, Nat.dvd_prime hprime]
    aesop
  · refine ne_of_apply_ne (· % 3) ?_
    dsimp
    rw [Nat.mod_mod_of_dvd _ (by norm_num), ← Nat.dvd_iff_mod_eq_zero, Nat.dvd_prime hprime]
    aesop
  · refine ne_of_apply_ne (· % 2) ?_
    dsimp
    rw [Nat.mod_mod_of_dvd _ (by norm_num), ← Nat.dvd_iff_mod_eq_zero, Nat.dvd_prime hprime]
    aesop

theorem infinitely_many_y_such_that_6y_pm_1_is_prime :
  ∃ᶠ (y : ℕ) in atTop, Nat.Prime (6 * y + 1) ∨ Nat.Prime (6 * y - 1) :=
  sorry

[Aaron Liu]

For this you also need some form of "infinitely many primes", or rather, "arbitrarily large primes", since what you have written is an "arbitrarily large" statement. Once you have that, combine it with the fact that all sufficiently large primes are 6n ± 1 which you have proved. You will also probably need a lower bound on y such that p = 6y ± 1 is possible (p / 6 - 2 should work).

[Kajani Kaunda]

Okay.
Lower bound : we can define y as y > 0 or ∈(0,+∞). or inroduce it as a hypothesis like this: (hy : y > 0). would that work?

[Kajani Kaunda]

On the other hand, perhaps y implicitly starts at 1 with the atTop syntax. No?

[Riccardo Brasca]

Do you have a math proof? We have Dirichlet theorem in mathlib, so it is immediate if you can use it.

[Kajani Kaunda]

Riccardo Brasca said:

Do you have a math proof? We have Dirichlet theorem in mathlib, so it is immediate if you can use it.

A "Math proof". how do you mean Sir?

[Riccardo Brasca]

A pen and paper proof.

[Kajani Kaunda]

Yes I do.

[Riccardo Brasca]

Ok, good. The easiest way of formulating this in Lean is to prove that for all k there is n >k such that 6*n+1 is prime (and similarly for -1).

[Riccardo Brasca]

Without bothering with filters/infinite sets.

[Kajani Kaunda]

All primes > 3 can be expressed in the form 6n + 1 or 6n - 1. So this implies that there are infinitely many n such that 6n + 1 or 6n - 1 are prime. QED. No?

[Kajani Kaunda]

Riccardo Brasca said:

Ok, good. The easiest way of formulating this in Lean is to prove that for all k there is n >k such that 6*n+1 is prime (and similarly for -1).

So how do I do that? Remember, I am not so good with Lean! :smile:

[Riccardo Brasca]

Kajani Kaunda said:

All primes > 3 can be expressed in the form 6n + 1 or 6n - 1. So this implies that there are infinitely many n such that 6n + 1 or 6n - 1 are prime. QED. No?

No, it implies that at least one of the two set is infinite, not that both are.

[Riccardo Brasca]

Ah sorry, you want the statement with or, so then yes, it's a direct consequence of the fact that there are infinitely many primes.

[Kajani Kaunda]

So can we use the already formalized theorem on that to prove our case?

[Ruben Van de Velde]

So you've got a set you know to be infinite (the primes >3), a set you'd like to prove is also infinite (the n s.t. ...) and a function from the primes to the corresponding n (somewhat implicitly given). The missing part is that this function is injective

[Kajani Kaunda]

Ruben Van de Velde said:

So you've got a set you know to be infinite (the primes >3), a set you'd like to prove is also infinite (the n s.t. ...) and a function from the primes to the corresponding n (somewhat implicitly given). The missing part is that this function is injective

Yes Sir. The injective part...

[Kajani Kaunda]

Is this a good start?

theorem infinitely_many_n_6n_plus_minus_1_primes :
    Infinite { n | Nat.Prime (6 * n + 1) ∨ Nat.Prime (6 * n - 1) } := by sorry

[Ruben Van de Velde]

Probably Set.Infinite is going to be easier

[Ruben Van de Velde]

I found a gap in my proof though - the function I hand-waved isn't injective (f 5 = f 7)

[Kajani Kaunda]

Ruben Van de Velde said:

Probably Set.Infinite is going to be easier

Great! The frustrating thing is that thoerem prime_form_6n_plus_1_or_6n_minus_1 implies it, so how do we state that in Lean?

Ruben Van de Velde said:

I found a gap in my proof though - the function I hand-waved isn't injective (f 5 = f 7)

Oh ....

[Ruben Van de Velde]

Probably you could prove that at least one of { n | Nat.Prime (6 * n + 1) } and { n | Nat.Prime (6 * n - 1) } is infinite as Riccardo suggested, and then your statement follows because you've got at least one infinite subset. No time to work it out in detail right now, though

[Ruben Van de Velde]

(There may be easier strategies)

[Kajani Kaunda]

Ruben Van de Velde said:

(There may be easier strategies)

I appreciate your suggestions. Thank you. I will try them out.