From 4888cb08f3d4dd3e8e45c1343186667594008b8a Mon Sep 17 00:00:00 2001 From: Speacky081 Date: Thu, 12 Mar 2026 10:22:49 +0100 Subject: [PATCH 1/3] finished one to three --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index ebae6b3..afc868f 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -203,7 +203,17 @@ theorem infinitude_of_primes_tfae : [ tfae_have 1 → 5 := by sorry -- Tonio - tfae_have 1 → 3 := by sorry -- Nina + tfae_have 1 → 3 := by -- Nina + intro P S + by_contra + push_neg at this + have Prime := {p | Nat.Prime p} + have p := Set.Infinite.exists_notMem_finset P S + obtain ⟨p, pP, pS⟩ := p + have not_prime := (this p) pS + have pPP : Nat.Prime p := pP + exact not_prime pPP + tfae_have 3 → 5 := by sorry -- Daniel From 8e884421a60b5e9d7ca9dff9dc6714d7fd2af407 Mon Sep 17 00:00:00 2001 From: Christoph Spiegel Date: Thu, 12 Mar 2026 11:08:34 +0100 Subject: [PATCH 2/3] cleanup: remove whitespace noise, keep only proof --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index afc868f..786c096 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -214,12 +214,11 @@ theorem infinitude_of_primes_tfae : [ have pPP : Nat.Prime p := pP exact not_prime pPP - tfae_have 3 → 5 := by sorry -- Daniel - tfae_have 7 → 1 := by sorry -- Bohdan / Kimia + tfae_have 7 → 1 := by sorry -- Bohdan - tfae_have 1 → 7 := by sorry -- Bohdan / Kimia + tfae_have 1 → 7 := by sorry -- Bohdan tfae_have 7 → 3 := by sorry -- Kimia From 9be8f1a12a38df9351dd9a442fed8f58f8f2b01b Mon Sep 17 00:00:00 2001 From: Christoph Spiegel Date: Thu, 12 Mar 2026 11:15:15 +0100 Subject: [PATCH 3/3] restore Bohdan / Kimia attribution --- 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 786c096..2280200 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -216,9 +216,9 @@ theorem infinitude_of_primes_tfae : [ tfae_have 3 → 5 := by sorry -- Daniel - tfae_have 7 → 1 := by sorry -- Bohdan + tfae_have 7 → 1 := by sorry -- Bohdan / Kimia - tfae_have 1 → 7 := by sorry -- Bohdan + tfae_have 1 → 7 := by sorry -- Bohdan / Kimia tfae_have 7 → 3 := by sorry -- Kimia