{"id":"palomar/PALOMAR-2026-08-18-000002","url":"https://github.com/AxiomMath/PrimeGapsLib/tree/1faa7b14e82ddebc2772dfb9153922f01b106477","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-18-000002-v1.json","repo":"https://github.com/AxiomMath/PrimeGapsLib","tags":["math.NT","msc:11N05","msc:11N35","msc:11N36","msc:11P32","prime-gaps","number-theory","lean-formalization"],"score":0,"title":"AxiomMath/PrimeGapsLib","trust":"high","domain":"math.NT","source":"palomar","authors":["Evan Chen","Sidharth Hariharan","Kenny Lau","Bhavik Mehta","Ken Ono","Ashvin Swaminathan","Jesse Thorner","Yunzhou Xie"],"reviews":0,"subject":"math.NT","summary":"`PrimeGapsLib` is an evolving codebase aimed at housing results about gaps in primes. The flagship result thus far is that pairs of primes are separated by at most 246 infinitely often, conditional on the Bombieri-Vinogradov theorem. The 246 proof was generated collaboratively between human formalisers at Axiom Math and AxiomProver, their in-house theorem proving system. Community feedback and contributions are welcome!","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-18","reactions":{},"formalized":true,"formalizes":[{"title":"Variants of the Selberg sieve","identifier":"https://doi.org/10.1186/s40687-014-0012-7","relationship":"formalizes"}]}