{"id":"palomar/PALOMAR-2026-09-18-000004","url":"https://github.com/JD-Jones-ASES/gnm-lean/tree/c9a75e1c81e5b7231a5a720ab544dd33f6a52ca1","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-18-000004-v1.json","repo":"https://github.com/JD-Jones-ASES/gnm-lean","tags":["math.CO","math.NT","msc:05A17","msc:11B75","combinatorics","number-theory","lean","partitions"],"score":0,"title":"gnm-lean: the number of partitions of {1, ..., n} into sets of at most three elements with power-of-three sums","trust":"high","domain":"math.CO","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 classification of the number of good partitions of an initial interval, where a good partition of {1, ..., n} is a set of pairwise disjoint nonempty blocks of at most three integers covering {1, ..., n}, each block summing to a power of three, and count n is the number of them. With N_u = {1, 2, 3, 4} union {3^t - 4, 3^t - 2, 3^t - 1, 3^t, 3^t + 1, 3^t + 2, 3^t + 3, 3^t + 5 : t >= 2} and E_2 = {13} union {3^t - 3 : t >= 2} union {3^t - 6 : t >= 3}, the four compared theorems say that for n >= 1 the count is 1 exactly on N_u, is 2 exactly on E_2, and is at least 3 elsewhere, and that…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-18","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"}]}