{"id":"palomar/PALOMAR-2026-10-29-000035","url":"https://github.com/sthubbar/goldbach-lean/tree/66ec03d5fb4e945966f9828e72b198029974de4b/entries/dudek2017","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-29-000035-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11P32","msc:11N36","msc:11N13","msc:11Y16"],"score":0,"title":"On the sum of a prime and a square-free number","trust":"high","domain":"math.NT","source":"palomar","authors":["Steve Hubbard"],"reviews":0,"subject":"math.NT","summary":"Conditional on one explicit hypothesis, AP12Lower 0.21, taken as a hypothesis of the theorem and never as an axiom: for every integer x >= 10^9, each reduced residue class mod 12 holds more than 0.21 x / log x primes p 2 is the sum of a prime and a square-free number. AP12Lower 0.21 is implied by Corollary 1.6 of M. A. Bennett, G. Martin, K. O'Bryant and A. Rechnitzer, Explicit bounds for primes in arithmetic progressions, Illinois J. Math. 62, 2018, which gives 1/4 in place of 0.21; the entry proves that implication in Lean, with the corollary itself stated as a hypothesis. The even case,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-29","reactions":{},"formalized":true,"formalizes":[{"title":"On the sum of a prime and a square-free number","identifier":"doi:10.1007/s11139-015-9736-2","relationship":"formalizes"}]}