From 791f82c480be9667b42634c393b66be2e719ff43 Mon Sep 17 00:00:00 2001 From: Alex Date: Thu, 12 Mar 2026 10:02:30 +0100 Subject: [PATCH 1/3] added proof that 6 implies 1 --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index ebae6b3..8a87eb2 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) @@ -194,10 +194,12 @@ 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 6 → 1 := by -- Alexander + rintro ⟨P, hP, hprime⟩ + exact Set.infinite_of_injective_forall_mem hP (fun x => hprime x) tfae_have 4 → 1 := by sorry -- Cara @@ -222,4 +224,3 @@ theorem infinitude_of_primes_tfae : [ tfae_have 9 → 2 := by sorry tfae_finish - From c177a26dbb57b341a8cd8516ae187642234d8324 Mon Sep 17 00:00:00 2001 From: Christoph Spiegel Date: Thu, 12 Mar 2026 11:08:58 +0100 Subject: [PATCH 2/3] cleanup: remove whitespace noise, keep only proof --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index 8a87eb2..35a2d33 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) @@ -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 -- Alexander @@ -209,9 +209,9 @@ theorem infinitude_of_primes_tfae : [ 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 @@ -224,3 +224,4 @@ theorem infinitude_of_primes_tfae : [ tfae_have 9 → 2 := by sorry tfae_finish + From bdf74601c81c620081f27c3dfb70af96200a438e Mon Sep 17 00:00:00 2001 From: Christoph Spiegel Date: Thu, 12 Mar 2026 11:15:00 +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 35a2d33..d610a01 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -209,9 +209,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