Four-digit Kaprekar dynamics in odd bases
Evan Chen, Ken Ono, Richard E. Schwartz, Dinesh S. Thakur
math.NT
Jun 18, 2026 · v1
math.CO
TL;DR
Formalizes its odd-base four-digit Kaprekar dynamics theorems in Lean 4 with Mathlib, generated autonomously by the AxiomProver system from statements alone.
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 famously sends every nonconstant base-ten string to 6174, but in other bases the terminal behavior splits into several cycles whose lengths depend on the base. The paper determines this structure completely for every odd base.
Approach
Using difference coordinates, the authors show that after at most three iterations every nonconstant orbit enters an explicit triangular region on which the Kaprekar map is conjugate to projective doubling [r],[s] -> [2r],[2s]. This yields explicit formulas for terminal cycle lengths and counts. As a test of AI-assisted formal mathematics, AxiomProver was given only the statements of the main theorems and autonomously produced Lean 4.28.0 formalizations: a problem statement (problem.lean) and a complete machine-checked proof (solution.lean).
Results
In every odd base B>3 the map has a rigid finite structure; the longest terminal cycle has length at most (B-1)/2, with equality possible only for prime B, and for primes p>5 equality holds exactly when the least m with 2^m = +-1 mod p is (p-1)/2. The Lean/Mathlib proofs were verified by the Lean 4 type-checker.
