gn-lean: the Gurvich–Naumova partition conjecture
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.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-07-000013
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-07-000013/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-07-000013/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'