AI Proof WatchKeep up with AI contributions

Counting partitions into small blocks with power-of-three sums

Can {1,…,n} always be partitioned into nonempty blocks of at most three distinct integers, each summing to a power of three? Beyond existence, which n have exactly one, exactly two or at least three such partitions?

Why it matters and what counts as progress

Why it matters: The counting question distinguishes unique or rare decompositions from the broader existence theorem.

What counts as progress: A proof of existence for every n, followed by an exhaustive count classification; an exception to a proposed one- or two-partition family also changes the classification.

How the problem developed

  1. 31 Jul 2025 · Conjecture and partial results [1]

    Vladimir Gurvich and Mariya Naumova Conjectured that every initial interval of positive integers has a partition into parts of size at most three with power-of-three sums; constrained possible minimal counterexamples and verified cases computationally through 844.

  2. 18 Oct 2026 · Reported theorem and formalization [2]

    Deep Bhattacharjee and Ushashi Bhattacharya Reported an explicit recursive partition for every n and provided a Lean 4 formalization; this proves the m=3 existence conjecture and the stated m=2-or-3 classification.

AI contributions 2

AI-centered Lean proof classifies base-three partition counts

For partitions of {1,…,n} into nonempty blocks of at most three elements whose sums are powers of three, the count is exactly one on N_u={1,2,3,4}∪{3ᵗ+d:t≥2, d∈{−4,−2,−1,0,1,2,3,5}}; exactly two on E₂={13}∪{3ᵗ−3:t≥2}∪{3ᵗ−6:t≥3}; and at least three otherwise.

AI involvementAI-centered
ImportanceNotable
Technical verificationFormal (Lean 4/Mathlib with decide +kernel exact finite search and induction)
Human understandingFew
Reported

Read the contribution and its assessment →

Sources

  1. Gurvich and Naumova, Partitioning [n] into subsets of size at most m such that all sums are powers of m
  2. Bhattacharjee and Bhattacharya, Partitioning [n] into parts of size at most three whose sums are powers of three (paper and Lean formalization)
  3. Jones, base-three partition classification
  4. AI and human contributions to the partition proof
  5. Lean verification of partition counts
  6. Gurvich and Naumova, base-three partition paper
  7. Jones’s partition formalization
  8. Partition proof attribution
  9. Partition proof verification record
  10. Gurvich and Naumova’s conjecture and partial results
Website timeline

Publication dates and editorial changes.