A Proof of Bala's Congruence Conjectures for A158690
Ahaan Kallat
math.NT
Sep 7, 2026 · v1
math.CO
TL;DR
Both of Bala's congruence conjectures for OEIS sequence A158690 were formally verified in Lean 4 using Mathlib.
Abstract
Let $a(n)$ be the sequence A158690 in the On-Line Encyclopedia of Integer Sequences (OEIS), defined by the exponential generating function $\sum_{n\ge0} a(n)t^n/n! = 1+\sum_{m\ge1}\prod_{j=1}^m(1-e^{-(2j-1)t})$. We prove two congruence conjectures of Peter Bala. The first states that, for every integer $k\ge1$, the sequence $a(n)$ modulo $k$ is eventually periodic with period dividing $\varphi(k)$. We prove the stronger statement that the Carmichael function $λ(k)$ is an eventual period. The second conjecture asserts the shifted Gauss congruences $a(np^r+i)\equiv a(np^{r-1}+i)\pmod{p^r}$ for every $i\ge0$, every prime $p$, and all $n,r\ge1$. Both results follow from a general theorem for exponential generating functions of the form $G(e^t-1)$ with $G\in\mathbb Z[[y]]$, together with the standard power-sum formula for Stirling numbers of the second kind.
Problem
Peter Bala conjectured two congruence properties for the OEIS integer sequence A158690: eventual periodicity modulo k with period dividing φ(k), and shifted Gauss congruences a(np^r+i) ≡ a(np^{r-1}+i) (mod p^r).
Approach
A general theorem is proved for exponential generating functions of the form G(e^t−1) with G in Z[[y]], expressing coefficients as integral linear combinations of m!·Stirling(n,m). Power-sum expansions of Stirling numbers reduce both conjectures to elementary congruences for integer powers, using the Carmichael function for periodicity. The sequence A158690 is shown to fit this form. Bala's original conjectures were additionally formally verified in Lean 4 with Mathlib.
Results
Both conjectures are proven, with the periodicity strengthened to eventual period λ(k) (the Carmichael function). The Lean development verifies the original φ(k) statement via top-level theorems A158690.bala_conjecture_one and A158690.bala_conjecture_two.
