PartitionPolynomial

Reciprocals of Partition Polynomials

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

Input files

For conjecture i where i ∈ {2,5,7,8,9,10}, the input files are:

the statement of the conjecture in Conjecture{i}_Statement.tex
task.md that reads

Please read `Conj{i}_Statement.tex` and formalize Conjecture~\ref{conj:conj{i}}.

.environment that reads lean-4.28.0 (omitted from the current repo)

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-Conjecture2.json
lake env comparator comparator-Conjecture5.json
lake env comparator comparator-Conjecture7.json
lake env comparator comparator-Conjecture8.json
lake env comparator comparator-Conjecture9.json
lake env comparator comparator-Conjecture10.json

License

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

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.