Lean repository linked
A bijective proof of a partition theorem of Berkovich and Uncu
arXiv:2608.05142 · arXiv
Lean formalisations (1)
AxiomMath/BerkovichUncu at 03c85e361f04
Linked by the repository’s formalization.yaml.
Project review: author-verified
Audit: awaiting publication.