Four-digit Kaprekar dynamics in odd bases
Evan Chen, Ken Ono, Richard E. Schwartz, Dinesh S. Thakur
math.NT
Jun 18, 2026 · v3
math.CO
TL;DR
AxiomProver autonomously produced Lean 4/Mathlib formalizations of the paper's main theorems on Kaprekar dynamics from the statements alone; files are in a public repository.
Abstract
Start with four digits, arrange them in both descending and ascending order, subtract, and repeat. This simple process is known as the Kaprekar routine, famous in base ten for sending every nonconstant four-digit string to $6174$. We show that in every odd base $B>3$, the four-digit Kaprekar map has an unexpectedly rigid structure. After at most three iterations, every nonconstant orbit enters an explicit triangular region $\mathcal{T}_B$, and on this region the map is conjugate to projective doubling: \[ \{[r],[s]\}\longmapsto \{[2r],[2s]\}. \] This gives a complete finite description of all nonconstant terminal cycles, including an explicit formula for their lengths and counts. In particular, the longest terminal cycle has length at most $(B-1)/2$, and equality can occur only when $B$ is prime. For primes $p>5$, equality occurs precisely when the least positive $m$ with $2^m\equiv\pm1\pmod p$ is $m=(p-1)/2$. The results proved here were first formulated by Schwartz and Thakur. As a test case for AI-assisted formal mathematics, AxiomProver produced Lean/mathlib formalizations of these results.
Problem
The four-digit Kaprekar routine in odd bases B>3 can have several terminal cycles, and nobody had a complete description of them. Schwartz and Thakur had formulated conjectured results on the structure and lengths of these cycles.
Approach
The digit map is reduced to a map on difference coordinates (d1,d2). After at most three iterations every nonconstant orbit enters a triangular region, where half-sum/half-difference coordinates conjugate the map to projective doubling on unordered pairs of classes in ((Z/BZ){0})/{±1}. Cycle lengths are then analyzed via the projective order of 2 modulo B. AxiomProver was given only the theorem statements and generated Lean 4.28.0 formal statements and complete proofs.
Results
All nonconstant terminal cycles are described, with explicit formulas for their lengths and counts. The longest cycle has length at most (B-1)/2, and equality can occur only for prime B. For primes p>5, equality holds exactly when the projective order of 2 is (p-1)/2. The main theorems are fully formalized in Lean (github.com/AxiomMath/kaprekar4).