Four-digit Kaprekar Dynamics in Odd Bases

This repository contains artifacts generated by AxiomProver related to the paper arXiv:TODO.

Input files

• input/kaprekar-input.tex: problem statement as TeX
• input/task.md: task specification (referring to TeX statement)
• input/.environment: specifies Lean version to use

Output files

• Kaprekar4/problem.lean: translation of the problem statement into Lean 4.28.0
• Kaprekar4/solution.lean solution in Lean 4.28.0

One can verify that the problem.lean and solution.lean are compatible using the axle verify-proof command:

cd Kaprekar4
axle verify-proof --environment lean-4.28.0 problem.lean solution.lean | jq ".okay"

Lean version

The formal proofs provided in this work were developed and verified using Lean 4.28.0. Compatibility with earlier or later versions is not guaranteed due to the evolving nature of the Lean 4 compiler and its core libraries.

Verifying with Comparator

This repository can be verified against the formal problem statement with the Lean comparator on a Linux machine. First, follow the instructions in https://github.com/leanprover/comparator to install comparator. Then, run the following command:

lake env comparator comparator.json

License

This repository uses the MIT License. See LICENSE for details.

Repository maintainers

• Evan Chen
• Kenny Lau
• Ken Ono
• Jujian Zhang