gnm-lean: the number of partitions of {1, ..., n} into sets of at most three elements with power-of-three sums
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-18-000004
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-18-000004/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-18-000004/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'