A bijective proof of a partition theorem of Berkovich and Uncu

Michal Mogielnicki, Ken Ono, Niels Voss, Jujian Zhang

math.CO Aug 5, 2026 · v1

Read PDF arXiv abstract Code

TL;DR

AxiomProver autonomously formalized and machine-verified the main bijective partition theorem in Lean 4.31.0, with problem and solution files.

Abstract

In 2016, Berkovich and Uncu proved that, for all nonnegative integers $i$, $j$, and $n$, the number of strict partitions of $n$ with $i$ odd-indexed odd parts and $j$ even-indexed odd parts equals the number of strict partitions of $n$ with $i$ parts congruent to $1$ modulo $4$ and $j$ parts congruent to $3$ modulo $4$. Their proof used generating functions, and they asked for a combinatorial proof. We answer their question with an explicit bijection, assembled from three classical ingredients: $2$-modular diagrams, an insertion algorithm of Chen, Gao, Ji, and Li, and Glaisher's bijection. AxiomProver autonomously formalized and verified the proof of the main theorem in Lean.

Problem

Berkovich and Uncu proved in 2016 that the number of strict partitions of n with i odd-indexed odd parts and j even-indexed odd parts equals the number with i parts congruent to 1 mod 4 and j parts congruent to 3 mod 4, using generating functions. They asked for a combinatorial proof.

Approach

An explicit bijection is constructed as a composition of four classical maps: 2-modular diagrams, an insertion algorithm of Chen–Gao–Ji–Li, and Glaisher's bijection, passing through intermediate partition classes. The bijection is computable in both directions and its statistic bookkeeping is verified on worked examples. The mathematical argument was developed by the human authors and then formalized in Lean.

Results

The bijection answers the Berkovich–Uncu question. AxiomProver autonomously translated the problem into Lean and produced a machine-checked formal proof of the main theorem using Lean 4.31.0.

Papers With

A bijective proof of a partition theorem of Berkovich and Uncu