{"id":"palomar/PALOMAR-2026-09-03-000006","url":"https://github.com/jidodat/erdos684-lean/tree/4543ff7764f9e8f1b2732a8464d5c19c945bfc52","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-03-000006-v1.json","repo":"https://github.com/jidodat/erdos684-lean","tags":["math.NT","math.CO","msc:11B65","msc:11N05","msc:11A51","number-theory","erdos-problems","lean-formalization"],"score":0,"title":"Erdős Problem 684: f(n)/log n is unbounded — a Lean 4 formalization of arXiv:2604.23784","trust":"high","domain":"math.NT","source":"palomar","authors":["Ji Ho Bae"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 formalization, against Mathlib, of the main theorem of J. H. Bae, \"Unbounded logarithmic limsup in Erdős Problem 684 via shifted carry scheduling\" (arXiv:2604.23784, v3). For 0 ≤ k ≤ n write C(n,k) = u·v with u supported on the primes ≤ k and v on the primes in (k,n], and let f(n) be the least k with u > n²; Erdős asked for bounds on f(n) (Problem 684 in Bloom's database). The compared theorems state that for every ε > 0 there are infinitely many n with f(n) > (1/2 − ε)·log n·log log n / log log log n, equivalently limsup f(n)·log log log n /(log n·log log n) ≥ 1/2 (stated in the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-03","reactions":{},"formalized":true,"formalizes":[{"title":"Unbounded logarithmic limsup in Erdős Problem 684 via shifted carry scheduling","identifier":"https://arxiv.org/abs/2604.23784","relationship":"formalizes"}]}