{"id":"palomar/PALOMAR-2026-09-04-000003","url":"https://github.com/ibrahimmian36/palomar-decanus/tree/776a5817bffcd9c30dd96259ccb7cfc822ec8ec4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-04-000003-v1.json","repo":"https://github.com/ibrahimmian36/palomar-decanus","tags":["cs.LO","math.NT","msc:11N56","msc:68V20","number-theory","divisor-function","erdos-problems"],"score":0,"title":"A kernel-checked exclusion certificate for Erdős Problem 647, to 10^8","trust":"high","domain":"cs.LO","source":"palomar","authors":["Ibrahim Mian","Shayaan Siddique"],"reviews":0,"subject":"cs.LO","summary":"Erdős Problem 647 asks whether there is any n > 24 with max_{m 10^8. The exclusion is certified rather than searched at check time. A witness at a cover position is an offset together with prime-power pairs dividing m, certifying tau(m) >= prod (e + 1); every prime in a pair is below 1024 and is checked prime by eleven trial divisions, so no primality certificates appear anywhere. A chain of witnesses covers the interval and each certificate chunk is discharged by a single decide against the chain checker, so the Lean kernel certifies the arithmetic and the generator that produced it is…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-09-04","reactions":{},"formalized":true,"formalizes":[{"title":"A Kernel-Checked Exclusion Certificate for Erdős Problem 647","identifier":"https://arxiv.org/abs/2608.17880","relationship":"formalizes"},{"title":"Erdős Problem 647","identifier":"https://www.erdosproblems.com/647","relationship":"formalizes"}]}