AI 中文总结
针对Berkovich与Uncu2016年提出的分拆定理，研究者构建了由2-模图等要素组成的显式双射，还借助AxiomProver在Lean中形式化验证了该主定理的证明，解决了其提出的组合证明问题。
AI 中文摘要
2016年，Berkovich和Uncu证明：对所有非负整数i、j和n，n的严格分拆中，具有i个奇索引奇部且j个偶索引奇部的数量，等于n的严格分拆中，具有i个模4余1的部分且j个模4余3的部分的数量。他们的证明使用生成函数，并提出是否存在组合证明的问题。我们通过一个显式双射回答了该问题，该双射由三个经典要素构成：2-模图、Chen、Gao、Ji和Li的插入算法，以及Glaisher双射。AxiomProver在Lean中自主形式化并验证了主定理的证明。
英文摘要
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.
CommentsComments welcome
