From 82503617f8b01eb7df56366c8939ed5bc3c6b366 Mon Sep 17 00:00:00 2001 From: Onat Tevfik Bilgili Date: Wed, 11 Mar 2026 16:31:45 +0100 Subject: [PATCH 1/3] finished proof 1 to 2 --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index ebae6b3..90ca7d7 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) @@ -185,7 +185,10 @@ theorem infinitude_of_primes_tfae : [ tfae_have 2 → 3 := by sorry -- Arthur - tfae_have 1 → 2 := by sorry -- Onat + tfae_have 1 → 2 := by + intro h + exact { not_finite := h } + -- Onat tfae_have 1 → 6 := by sorry -- Bohdan @@ -194,7 +197,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 @@ -222,4 +225,3 @@ theorem infinitude_of_primes_tfae : [ tfae_have 9 → 2 := by sorry tfae_finish - From 4d3d63123f5585997924ce1a6ca1c957832009e0 Mon Sep 17 00:00:00 2001 From: Christoph Spiegel Date: Thu, 12 Mar 2026 11:09:20 +0100 Subject: [PATCH 2/3] cleanup: remove whitespace noise, keep only proof --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index 90ca7d7..4febfd8 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) @@ -185,10 +185,9 @@ theorem infinitude_of_primes_tfae : [ tfae_have 2 → 3 := by sorry -- Arthur - tfae_have 1 → 2 := by + tfae_have 1 → 2 := by -- Onat intro h exact { not_finite := h } - -- Onat tfae_have 1 → 6 := by sorry -- Bohdan @@ -197,7 +196,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 @@ -210,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 @@ -225,3 +224,4 @@ theorem infinitude_of_primes_tfae : [ tfae_have 9 → 2 := by sorry tfae_finish + From e161a88c63bede16e58f44ffa81df37461f81e75 Mon Sep 17 00:00:00 2001 From: Christoph Spiegel Date: Thu, 12 Mar 2026 11:14:27 +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 4febfd8..c762a2e 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