A Lean 4 formalization, generated by AxiomProver, of the dynamics of Kaprekar's routine for four-digit numbers in odd bases B > 3, proving the map is conjugate to a doubling map on projective residues and deriving terminal-cycle bounds.
Want to contribute? Help formally verify Four-digit Kaprekar Dynamics in Odd Bases. Click on the button to view remaining issues on GitHub.
This table shows the verification status of all functions in the project. Click on a function to see more details.
