HEXAGONbeta

Partitioning {1,…,n}\{1,\dots,n\} into parts of size at most three whose sums are powers of three

A mix of human-written and AI-generated textHuman understanding: some partsmath.CO — Combinatoricsmath.NT — Number Theory

Contributed by Deep Bhattacharjee ↗, Ushashi Bhattacharya ↗

Version 1 / Oct 20, 2026 / CC BY 4.0

Abstract

We prove unconditionally the conjecture of Gurvich and Naumova that for every n≥1n\ge1 the set {1,…,n}\{1,\dots,n\} can be partitioned into parts of at most three elements whose sums are powers of 33. The partition is given by an explicit recursion.

Provenance statement

The proofs, the text, the figures, the Lean 4 formalization and the Python, Julia, C and C++ programs were carried out by Deep Bhattacharjee with the help of AI assistance (Claude, Anthropic) in the Claude Code environment. The paper proves Conjecture 1 of V. Gurvich and M. Naumova (arXiv:2508.00946): for every n >= 1 the set {1, ..., n} has a partition into parts of at most three elements whose sums are powers of 3. The partition is given by a recursion on n. Three of its four cases are reductions from Section 2 of the preprint of Gurvich and Naumova; for the fourth (n = 3^t + j with j = 2 mod 3 and 2j < 3^t) the paper proves the stronger statement that {1, ..., n} minus the triple {n - 1, n, 3^t - 2j + 1} has such a partition, by a reflection argument and, when j lies in the upper half of its interval [3^u, 3^(u+1)), by an explicit fixed-point-free involution of {1, ..., 2N - 2} with distinct pair sums. As a corollary, for m >= 2 every {1, ..., n} has a partition into parts of at most m elements with sums powers of m if and only if m is 2 or 3. The theorem is proved in Lean 4 with Mathlib (GN.gurvich_naumova, 7 files, 1073 lines), which states the existence of a Finpartition of Finset.Icc 1 n into parts of at most three elements with sums powers of 3 and depends only on the axioms propext, Classical.choice and Quot.sound, with no sorry, native_decide or added axiom. Programs in Python, Julia, C and C++ run the recursion and check the partition for every n <= 30000 and for further values up to 6.5*10^7. Before this proof the conjecture was known for n <= 844 (computation of D. Rybin, reported by Gurvich and Naumova). Both authors approved the final version. Tools used: Anthropic - Claude (Claude Code); Lean community - Lean 4 (v4.34.1) with Mathlib; Python; Julia; C; C++; shell. arXiv identifier: none (not posted on arXiv). Formalization: https://github.com/creelie/didactic-lamp/blob/main/lean/GurvichNaumova/Main.lean (archived at Zenodo, release v2.1.0: https://doi.org/10.5281/zenodo.23455972)
AI provenance filesAI_PROVENANCE_GurvichNaumovaConjecture.md · 3 KB

Tools used

Anthropic
Claude CodeVersion Opus 5.5 Ultracode

References

  1. V. Gurvich, M. Naumova, Partitioning set [n]={1,…,n}[n]=\{1,\dots,n\} into subsets of size at most mm such that all sums are powers of mm, arXiv:2508.00946 [math.CO] (2025). doi:10.48550/arXiv.2508.00946 (https://doi.org/10.48550/arXiv.2508.00946).arXivDOI
  2. Th. Skolem, On certain distributions of integers in pairs with given differences, Math. Scand. 5 (1957) 57--68. doi:10.7146/math.scand.a-10490 (https://doi.org/10.7146/math.scand.a-10490).DOI
  3. L. de Moura, S. Ullrich, The L ean 4 theorem prover and programming language, in: Automated Deduction -- CADE 28, Vol. 12699 of Lecture Notes in Comput. Sci., Springer, Cham, 2021, pp. 625--635. doi:10.1007/978-3-030-79876-5_37 (https://doi.org/10.1007/978-3-030-79876-5_37).DOI
  4. The mathlib Community , The L ean mathematical library, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, ACM, New York, 2020, pp. 367--381. doi:10.1145/3372885.3373824 (https://doi.org/10.1145/3372885.3373824).DOI
  5. D. Bhattacharjee, U. Bhattacharya, Iterated nerve complexes for kk-fold sensor coverage, Preprints.org (2026). doi:10.20944/preprints202606.1351.v2 (https://doi.org/10.20944/preprints202606.1351.v2).DOI
  6. D. Bhattacharjee, Establishing equivariant class [O][O] for hyperbolic groups, Asian Res. J. Math. 18 (11) (2022) 362--369. doi:10.9734/arjom/2022/v18i11615 (https://doi.org/10.9734/arjom/2022/v18i11615).DOI
  7. D. Bhattacharjee, P. Nandi, Enriques and K ummer surfaces arising from K3 involutions, Preprints.org (2026). doi:10.20944/preprints202602.0098.v1 (https://doi.org/10.20944/preprints202602.0098.v1).DOI
  8. D. Bhattacharjee, U. Bhattacharya, Partitioning {1,…,n}\{1,\dots,n\} into parts of size at most three whose sums are powers of three: paper, Lean 4 formalization and verification code, Zenodo (2026). doi:10.5281/zenodo.23455972 (https://doi.org/10.5281/zenodo.23455972).DOI

Version history

  1. v1Submitted by Deep BhattacharjeeInitial depositCurrentOct 18, 2026