Skip to content

formalization.yaml: fix minor formatting errors #4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
thefundamentaltheor3m merged 4 commits into from
Aug 17, 2026
Merged

formalization.yaml: fix minor formatting errors #4

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e64aec8
formalization.yaml: formatting errors
thefundamentaltheor3m Aug 17, 2026
e6a0b72
add msc classifications based on sources
thefundamentaltheor3m Aug 17, 2026
1d54603
rm inconsistency with comparator
thefundamentaltheor3m Aug 17, 2026
09a6fd8
flesh out scope a bit
thefundamentaltheor3m Aug 17, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 5 additions & 12 deletions formalization.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -15,32 +15,25 @@ 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]
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]
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
Expand Down
Loading