From e64aec831b1e366b55bd03c0b5072033b964844d Mon Sep 17 00:00:00 2001 From: Sidharth Hariharan Date: Mon, 17 Aug 2026 15:43:43 -0700 Subject: [PATCH 1/4] formalization.yaml: formatting errors --- formalization.yaml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/formalization.yaml b/formalization.yaml index 5a9ad58..518b3ef 100644 --- a/formalization.yaml +++ b/formalization.yaml @@ -6,7 +6,7 @@ project: name: "PrimeGapsLib" authors: [Evan Chen, Sidharth Hariharan, Kenny Lau, Bhavik Mehta, Ken Ono, Ashvin Swaminathan, Jesse Thorner, Yunzhou Xie] responsible_maintainers: [Kenny Lau, Ashvin Swaminathan] - license: "Apache 2.0" + license: "Apache-2.0" sources: - title: "Variants of the Selberg sieve" @@ -15,14 +15,14 @@ sources: type: "article" location: "Theorem 4(i)" relationship: "formalizes" - source_note: "Formalises the fact that the Bombieri-Vinogradov theorem implies it" + note: "Formalises the fact that the Bombieri-Vinogradov theorem implies it" - title: "Small gaps between primes" authors: [James Maynard] id: "https://doi.org/10.4007/annals.2015.181.1.7" type: "article" location: "Theorem 1.4, second inequality" relationship: "formalizes" - source_note: "Formalises the fact that the Bombieri-Vinogradov theorem implies it" + note: "Formalises the fact that the Bombieri-Vinogradov theorem implies it" classification: arxiv: [math.NT] From e6a0b724a1005dce4db19b1f5c7e4a9bd7340fc9 Mon Sep 17 00:00:00 2001 From: Sidharth Hariharan Date: Mon, 17 Aug 2026 15:54:34 -0700 Subject: [PATCH 2/4] add msc classifications based on sources --- formalization.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/formalization.yaml b/formalization.yaml index 518b3ef..81929d1 100644 --- a/formalization.yaml +++ b/formalization.yaml @@ -26,6 +26,7 @@ sources: classification: arxiv: [math.NT] + msc2020: [11N05, 11N35, 11N36, 11P32] # Based on the MSC classifications of the sources status: scope: "Developing a consolidated Lean library for results on gaps between primes" From 1d54603732c0d4511c03a2595bdcdde36e2143f2 Mon Sep 17 00:00:00 2001 From: Sidharth Hariharan Date: Mon, 17 Aug 2026 16:08:10 -0700 Subject: [PATCH 3/4] rm inconsistency with comparator --- formalization.yaml | 8 -------- 1 file changed, 8 deletions(-) diff --git a/formalization.yaml b/formalization.yaml index 81929d1..5cafabb 100644 --- a/formalization.yaml +++ b/formalization.yaml @@ -34,14 +34,6 @@ status: sorry_in_definitions: 0 axioms: [propext, Classical.choice, Quot.sound] main_results: - - declaration: "bombieriVinogradov_implies_frequently_prime_gap_le_246" - file: "PrimeGaps/Bounded246.lean" - sorry_count: 0 - axioms: [propext, Classical.choice, Quot.sound] - comparator_config: "Comparator/comparator.json" - literature_dependencies: - - statement: "The Bombieri-Vinogradov Theorem" - source: "Small gaps between primes (p.384)" - declaration: "bombieriVinogradov_implies_prime_gap_le_246" file: "PrimeGaps/Bounded246.lean" sorry_count: 0 From 09a6fd8a5d9194639246167b017287f596273b5c Mon Sep 17 00:00:00 2001 From: Sidharth Hariharan Date: Mon, 17 Aug 2026 16:09:40 -0700 Subject: [PATCH 4/4] flesh out scope a bit --- formalization.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/formalization.yaml b/formalization.yaml index 5cafabb..9235dd5 100644 --- a/formalization.yaml +++ b/formalization.yaml @@ -29,7 +29,7 @@ classification: msc2020: [11N05, 11N35, 11N36, 11P32] # Based on the MSC classifications of the sources status: - scope: "Developing a consolidated Lean library for results on gaps between primes" + scope: "Developing a consolidated Lean library for results on gaps between primes, the flagship result being that the Bombieri-Vinogradov theorem implies that that there are infinitely many pairs of primes separated by no more than 246." sorry_count: 0 sorry_in_definitions: 0 axioms: [propext, Classical.choice, Quot.sound]