# AI provenance: Partitioning {1, ..., n} into parts of size at most three whose sums are powers of three

Authors: Deep Bhattacharjee (corresponding author, ORCID 0000-0003-0466-750X;
formerly EGSPL, Bhubaneswar, Odisha 751030, India, and formerly University of
Calcutta, Senate House, 87/1 College Street, Kolkata 700073, West Bengal,
India) and Ushashi Bhattacharya (ORCID 0009-0002-2254-3914; formerly National
Taiwan University, Taipei 106319, Taiwan).

- Paper: https://github.com/creelie/didactic-lamp/blob/main/preprintGurvichNaumovaConjecture/GurvichNaumovaConjecture.pdf
- Lean formalization and code: doi:10.5281/zenodo.23455972 (release v2.1.0; all versions doi:10.5281/zenodo.23316376)
- Repository: https://github.com/creelie/didactic-lamp

## Result

Conjecture 1 of V. Gurvich and M. Naumova (arXiv:2508.00946) states that for
every n ≥ 1 the set {1, ..., n} can be partitioned into parts of at most three
elements, the sum of each part being a power of 3. Before this proof it was
known for n ≤ 844. The paper proves it for every n, with the partition given
by an explicit recursion. As a corollary, for m ≥ 2 every set {1, ..., n} has
a partition into parts of at most m elements with sums that are powers of m
if and only if m is 2 or 3.

## Who did what

Deep Bhattacharjee chose the problem, directed the work, set the format and
the target journal, and ran the computations. Claude (Anthropic), used through
Claude Code under his direction, produced the following:

- the proofs (the strengthened statement for the fourth case of the recursion,
  the reflection lemma and the involutions with distinct pair sums);
- the Lean 4 formalization (7 files, 1073 lines);
- the checking programs in C, C++, Python and Julia;
- the figures;
- the LaTeX text of the paper, its footnotes and its reference list (every
  reference, the three self-citations included, was checked against the
  Crossref or arXiv record);
- this file and the submission notes.

No other AI system took part. The paper uses no unproved result from other
work.

## How the result is checked

- **Lean 4.34.1 with Mathlib.** The main theorem `GN.gurvich_naumova` states
  that for every natural number n there is a partition of {1, ..., n} into
  nonempty parts, each with at most three elements and a power of 3 as its
  sum. It depends only on the standard axioms propext, Classical.choice and
  Quot.sound. There is no `sorry`, `admit`, `native_decide` or added axiom.
- **Independent programs.** Programs in C, C++, Python and Julia build the
  partition of the recursion and check it for every n ≤ 30000 and for further
  values of n up to 6.5·10^7. They also check the invariant used in the
  induction and the two lemmas on zero-sum triples and on the involutions
  that the proof uses.
- **Release workflow.** It builds the Lean proof and runs every program before
  publishing.

## What is not claimed

The paper proves Conjecture 1 of Gurvich and Naumova and its corollary for
general m. The other questions of their preprint are not treated. The authors
checked on 15 October 2026, and again on 18 October 2026, that version 3 of
the preprint (July 2026) still lists the conjecture as open, and found no
other proof on arXiv, on GitHub or on the web.