A bijective proof of a partition theorem of Berkovich and Uncu

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

Input files

• input/task.md: problem statement
• input/main-5.tex: source of the paper

Output files

• BerkovichUncu/problem.lean: translation of the problem statement into Lean 4.31.0
• BerkovichUncu/solution.lean: solution in Lean 4.31.0

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

cd $DIRECTORY
axle verify-proof --environment lean-4.31.0 problem.lean solution.lean | jq ".okay"

Formalization notes

That each of the four maps outputs a partition of n in the stated class, and is a bijection, is assumed rather than proved: these are the sixteen fields of BUData n, which mainEquiv and main_cardinality take as a hypothesis.

Lean version

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

License

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

Repository maintainers

• Evan Chen
• Kenny Lau
• Michal Mogielnicki
• Ken Ono