From 2fbc08eb16600485c4bb8713373955b3c1da00b0 Mon Sep 17 00:00:00 2001 From: Towalt Date: Thu, 12 Mar 2026 09:34:23 +0100 Subject: [PATCH 1/3] one_to_five_tonio --- .../P06_Mathlib/S01_PrimeTheorem.lean | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index ebae6b3..17635fc 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,26 +194,29 @@ 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 1 → 5 := by sorry -- Tonio + tfae_have 1 → 5 := by + intro h n + have ⟨x, y, z⟩ := h.exists_gt n + exact ⟨x, z, y⟩ -- Tonio tfae_have 1 → 3 := by sorry -- Nina 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 - tfae_have 1 → 8 := by sorry + tfae_have 1 → 8 := by sorry tfae_have 8 → 5 := by sorry From 2517954b08f11d8941970e811df4184adab6a9aa Mon Sep 17 00:00:00 2001 From: Christoph Spiegel Date: Thu, 12 Mar 2026 11:09:40 +0100 Subject: [PATCH 2/3] cleanup: remove whitespace and comment noise, keep only proof --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index 17635fc..25c3f30 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,17 +194,17 @@ 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 1 → 5 := by + tfae_have 1 → 5 := by -- Tonio intro h n have ⟨x, y, z⟩ := h.exists_gt n - exact ⟨x, z, y⟩ -- Tonio + exact ⟨x, z, y⟩ tfae_have 1 → 3 := by sorry -- Nina @@ -216,7 +216,7 @@ theorem infinitude_of_primes_tfae : [ tfae_have 7 → 3 := by sorry -- Kimia - tfae_have 1 → 8 := by sorry + tfae_have 1 → 8 := by sorry tfae_have 8 → 5 := by sorry From ac88dce439cbe4e3b373bb1f9cdd7457d52b0efd Mon Sep 17 00:00:00 2001 From: Christoph Spiegel Date: Thu, 12 Mar 2026 11:14:43 +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 25c3f30..cd3505e 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -210,9 +210,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