A Proof of Bala's Congruence Conjecture for A028342
Ahaan Kallat
math.CO
Jul 17, 2026 · v1
TL;DR
Theorem 1.1 and all supporting propositions and lemmas about congruences for OEIS sequence A028342 were formally verified in Lean 4 with Mathlib.
Abstract
Let $a(n)$ be the sequence A028342 in the On-Line Encyclopedia of Integer Sequences (OEIS), defined by the exponential generating function $\sum_{n\ge0} a(n)x^n/n! = \prod_{i\ge1}(1-x^i)^{-1/i}$. Equivalently, $a(n)$ counts permutations of an $n$-element labeled set in which every cycle is assigned one divisor of its length, where a cycle of length $m$ has $d(m)$ choices, $d(m)$ being the number of positive divisors of $m$. We prove a family of congruences for $a$, conjectured by Peter Bala. They state that $k \mid a(n+k)+a(n)$ for odd $k$, that $k \mid a(n+k)-a(n)$ for $k\equiv 0,2,6 \pmod 8$, and that $k \mid 2(a(n+k)-a(n))$ for $k\equiv 4\pmod 8$. The proof first establishes a product congruence $a(n+k)\equiv a(n)a(k)\pmod k$, and then computes $a(p^r)\bmod p^r$ for each prime power by counting the colored permutations fixed by a subgroup of order $p$.
Problem
Peter Bala conjectured a family of congruences for OEIS sequence A028342, defined via an exponential generating function counting colored permutations, but these congruences were left unproved.
Approach
A product congruence a(n+k) ≡ a(n)a(k) (mod k) is established using a cyclic group action on colored permutations and the orbit–stabilizer theorem. The problem is reduced to prime powers via the Chinese remainder theorem, and prime-power residues a(p^r) mod p^r are computed by counting objects fixed by an order-p subgroup. The final congruences are assembled by case analysis on k. The entire argument, including Theorem 1.1 and its lemmas, was formalized in Lean 4 using Mathlib.
Results
The conjectured congruences are proven: k divides a(n+k)+a(n) for odd k, k divides a(n+k)-a(n) for k≡0,2,6 mod 8, and k divides 2(a(n+k)-a(n)) for k≡4 mod 8. The proofs are machine-checked in Lean.
