From a98ec03ed8243d06331f30aec81308addac927a7 Mon Sep 17 00:00:00 2001 From: Cara Bennett Date: Thu, 12 Mar 2026 11:01:18 +0100 Subject: [PATCH 1/4] showed_4_to_1 --- .../P06_Mathlib/S01_PrimeTheorem.lean | 69 ++++++++++++------- 1 file changed, 45 insertions(+), 24 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index a423dff..87b7bd5 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -39,7 +39,7 @@ To do this, you should: (III) Use `exact?` or `simp?` whenever you think you have a nuclear expression that *should* be in mathlib to try and find it. Often it is advisable to extract the statement into - separate `example` for this. You can also manually search the files, guess the + separate `example` for this. You can also manually search the files, guess the expected theorem name based on the [mathlib naming convention](https://leanprover-community.github.io/contribute/naming.html), use [leansearch.net](https://leansearch.net) or [Loogle](https://loogle.lean-lang.org), talk to people on [Is there code for X? on zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Complexity.20theory/with/578655619) @@ -82,12 +82,54 @@ theorem infinitude_of_primes_tfae : [ tfae_have 3 → 4 := by sorry -- Alexandra tfae_have 5 → 4 := by sorry -- Sammy - + tfae_have 6 → 3 := by sorry -- Anna tfae_have 6 → 1 := by sorry -- Alexander - tfae_have 4 → 1 := by sorry -- Cara + tfae_have 4 → 1 := by -- Cara + /- + We are proving that : + Given: + (4) For any finite set *of prime numbers* we can find a prime number outside of it, i.e. + `(∀ (S : Finset ℕ) (_ : ∀ s ∈ S, Nat.Prime s), (∃ p ∉ S, p.Prime))`. + Then: + (1) The set of primes is infinite, i.e. `{ p : ℕ | p.Prime }.Infinite`. + -/ + + -- First, we clear the unused variables to make the InfoView more readable. + clear tfae_5_to_6 tfae_2_to_3 tfae_1_to_2 tfae_1_to_6 tfae_3_to_2 + tfae_3_to_4 tfae_5_to_4 tfae_6_to_3 tfae_6_to_1 + + -- Introduce our assumption (4) + intro h + + --- Assume by way of contradiction that the set of primes is finite. + by_contra P_finite + push_neg at P_finite + + -- We also define P, the set of primes, to use later in the proof. + let P := {p | Nat.Prime p} + + -- Now, we show that all numbers in our set are prime, using the theorem `Set.mem_toFinset` + -- See: (https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Set.mem_toFinset#doc) + -- This is necessary, since our hypothesis is only for sets of prime numbers. + obtain (n_in_P_n_prime : (∀ n ∈ P_finite.toFinset, Nat.Prime n)) := + fun _ => (@Set.Finite.mem_toFinset ℕ P _ P_finite).mp + + -- We apply our hypothesis, so we get that there exists a + -- prime not in our finite set of primes + have _ := h P_finite.toFinset n_in_P_n_prime + + -- Finally, we show that the opposite statement is also true, and we get a contradiction. + -- See: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Set.notMem_setOf_iff#doc + -- For the description of `notMem_setOf_iff` + obtain (_ : ¬(∃ p ∉ P_finite.toFinset, Nat.Prime p)) := by + push_neg + intro p p_not_in_P_finset + have p_not_in_S := (@Set.Finite.mem_toFinset ℕ P p P_finite).mpr.mt p_not_in_P_finset + exact Set.notMem_setOf_iff.mp p_not_in_S + contradiction tfae_have 1 → 5 := by sorry -- Tonio @@ -96,24 +138,3 @@ theorem infinitude_of_primes_tfae : [ tfae_have 3 → 5 := by sorry -- Daniel tfae_finish - - - - - - - - - - - - - - - - - - - - - From 9777226793d52ad6fd4b3e7c5d0d33ce0069dc86 Mon Sep 17 00:00:00 2001 From: Cara Bennett Date: Thu, 12 Mar 2026 11:14:14 +0100 Subject: [PATCH 2/4] remamed variable --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index 87b7bd5..cb6a14d 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -127,8 +127,8 @@ theorem infinitude_of_primes_tfae : [ obtain (_ : ¬(∃ p ∉ P_finite.toFinset, Nat.Prime p)) := by push_neg intro p p_not_in_P_finset - have p_not_in_S := (@Set.Finite.mem_toFinset ℕ P p P_finite).mpr.mt p_not_in_P_finset - exact Set.notMem_setOf_iff.mp p_not_in_S + have p_not_in_P := (@Set.Finite.mem_toFinset ℕ P p P_finite).mpr.mt p_not_in_P_finset + exact Set.notMem_setOf_iff.mp p_not_in_P contradiction tfae_have 1 → 5 := by sorry -- Tonio From ff417eca3c8eec4980cdfc447a08b9f817d68c6a Mon Sep 17 00:00:00 2001 From: carabennett <71158040+carabennett@users.noreply.github.com> Date: Thu, 12 Mar 2026 11:19:59 +0100 Subject: [PATCH 3/4] whitespace --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index bd1a7eb..d245127 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -42,7 +42,7 @@ To do this, you should: (III) Use `exact?` or `simp?` whenever you think you have a nuclear expression that *should* be in mathlib to try and find it. Often it is advisable to extract the statement into - separate `example` for this. You can also manually search the files, guess the + separate `example` for this. You can also manually search the files, guess the expected theorem name based on the [mathlib naming convention](https://leanprover-community.github.io/contribute/naming.html), use [leansearch.net](https://leansearch.net) or [Loogle](https://loogle.lean-lang.org), talk to people on [Is there code for X? on zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Complexity.20theory/with/578655619) From ae7c3eed5ae3379e5b01dc1542b4a9041e4ca8d9 Mon Sep 17 00:00:00 2001 From: carabennett <71158040+carabennett@users.noreply.github.com> Date: Thu, 12 Mar 2026 11:20:28 +0100 Subject: [PATCH 4/4] whitespace --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index d245127..2636517 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -194,7 +194,7 @@ theorem infinitude_of_primes_tfae : [ tfae_have 3 → 4 := by sorry -- Alexandra tfae_have 5 → 4 := by sorry -- Sammy - + tfae_have 6 → 3 := by sorry -- Anna tfae_have 6 → 1 := by sorry -- Alexander