{"id":"palomar/PALOMAR-2026-10-28-000016","url":"https://github.com/sthubbar/goldbach-lean/tree/79f0a9c960083e7497d7217132b59ffc24f6558f/entries/bordignonstarichkova2024grh","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-28-000016-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11P32","msc:11N36","msc:11M26","msc:11Y35"],"score":0,"title":"CONDITIONAL on GRH and four cited theorems: an explicit Chen threshold exp(exp 13.375), after Bordignon and Starichkova","trust":"high","domain":"math.NT","source":"palomar","authors":["Steve Hubbard"],"reviews":0,"subject":"math.NT","summary":"CONDITIONAL. A Lean 4 proof that, under the Generalized Riemann Hypothesis, every even integer N at least exp(exp 13.375) is the sum of a prime and a square-free number greater than 1 with at most two prime factors, CONDITIONAL ON four cited results taken as explicit hypotheses of the theorem, never as axioms: Thm5J, Thm6J and Thm7J, the Lean Lab's transcriptions of Theorems 5, 6 and 7 of M. Bordignon and V. Starichkova, An explicit version of Chen's theorem assuming the Generalized Riemann Hypothesis, Ramanujan J. 64, 2024, 1213 to 1242; and LinearSieveT4 1/8349 112 114, the transcription…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-28","reactions":{},"formalized":true,"formalizes":[{"title":"An explicit version of Chen's theorem assuming the Generalized Riemann Hypothesis","identifier":"doi:10.1007/s11139-024-00866-x","relationship":"adapts"},{"title":"A lower explicit threshold for Chen's theorem under GRH","identifier":"aiXiv.online 2610.02760","relationship":"formalizes"}]}