{"id":"palomar/PALOMAR-2026-09-07-000013","url":"https://github.com/JD-Jones-ASES/gn-lean/tree/73bb87b16da8c053fd07e0d4dc43732b74335a3b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-07-000013-v1.json","repo":"https://github.com/JD-Jones-ASES/gn-lean","tags":["math.CO","math.NT","msc:05A17","msc:11B75","combinatorics","number-theory","lean","partitions"],"score":0,"title":"gn-lean: the Gurvich–Naumova partition conjecture","trust":"high","domain":"math.CO","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 proof that for every nonnegative integer n, the distinct integers 1,...,n can be partitioned into nonempty sets of at most three elements, each having sum equal to a nonnegative integer power of three. This proves Conjecture 1 of Gurvich and Naumova, arXiv:2508.00946v3. The development constructs permutations with all prescribed nonzero displacements, derives signed zero-sum triple partitions, proves a contraction and complement-pair extension, and completes strong induction on n. All required finite certificates and unbounded sequence constructions are proved in Lean.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-07","reactions":{},"formalized":true,"formalizes":[{"title":"Partitioning set [n]={1,...,n} into subsets of size at most m such that all sums are powers of m","identifier":"arXiv:2508.00946v3","relationship":"adapts"},{"title":"Hooked extended Langford sequences of small and large defects","identifier":"doi:10.2478/s12175-014-0242-6","relationship":"adapts"}]}