I'd like to propose a formalization project to be included in the Lean-Pool:
Repository: https://github.com/viazovska/PentagonalNumberTheorem
Apache-2.0 · leanprover/lean4:v4.30.0-rc1 · Mathlib tracked at master
The repository contains two independent proofs of Euler's pentagonal number theorem. They share
no lemmas, so each confirms the result on its own.
The Franklin route is the primary development and the focus of our work. It is the sign-reversing
involution on partitions into distinct parts, giving p_e(n) - p_o(n) = (-1)^|k| when n is the
generalized pentagonal number k(3k-1)/2 and 0 otherwise, together with the identification of that
signed count with the coefficient of X^n in the truncated product over ℤ⟦X⟧. It builds on
Mathlib's Nat.Partition.genFun, whose module docstring lists "generating function for the
partition function p(n) (TODO: prove this)" — which coeff_pGenFun_eq_p_count here effectively
does.
The q-series route develops q-Pochhammer symbols, the Gaussian binomial coefficient, Euler's two
identities and the Cauchy identity, proves the Jacobi triple product both as a formal power
series identity over an arbitrary commutative ring and analytically over ℂ for ‖q‖ < 1, and
reaches the same theorem for the infinite product by specialization. We include it because it is
much the more reusable half: that machinery is general-purpose, whereas the Franklin route is
specific to this theorem. We note that q-series identities including the Jacobi triple product
have been formalized in Lean before [see arXiv:2607.01544]; we claim no priority.
On provenance, which we would record as AI: the Lean proofs in both routes were largely
generated by Aristotle (Harmonic). The two differ in how much human direction and checking went
in. The Franklin route (1264 lines) follows a blueprint we wrote ourselves, lemma by lemma, and
carries substantially more manual intervention and review. The q-series route (3318 lines, 72% of
the project) is machine-generated blueprint and all; our contribution was restructuring the
library, renaming its API to be mathlib-ready and reviewing statements. Claude assisted with proof
development, the blueprint and CI. If you read that split as mix rather than AI we would not
object, but AI seems the more accurate of the two.
The gates, as far as we can check them: 4582 lines of our own Lean across 19 files; no sorry;
axioms limited to propext, Classical.choice and Quot.sound; no unsafe or partial; Apache-2.0;
a file header on all 19 files; largest file 716 lines; lake build --wfail green, with Mathlib's
standard linter set enabled in lakefile.toml and enforced in CI.
Every formalized declaration is tied to a blueprint entry with a prose statement and proof sketch,
and leanblueprint checkdecls enforces in CI that every \lean{} annotation names a declaration
that exists. All 220 public declarations carry docstrings. Blueprint, dependency graph and
doc-gen4 API documentation are at https://viazovska.github.io/PentagonalNumberTheorem/.
PentagonalNumberTheorem.lean imports both halves, if a single entry module helps.
We can also open a content PR under LeanPool/ instead if you would prefer; a project card is
drafted and ready.
I'd like to propose a formalization project to be included in the Lean-Pool:
Repository: https://github.com/viazovska/PentagonalNumberTheorem
Apache-2.0 ·
leanprover/lean4:v4.30.0-rc1· Mathlib tracked atmasterThe repository contains two independent proofs of Euler's pentagonal number theorem. They share
no lemmas, so each confirms the result on its own.
The Franklin route is the primary development and the focus of our work. It is the sign-reversing
involution on partitions into distinct parts, giving p_e(n) - p_o(n) = (-1)^|k| when n is the
generalized pentagonal number k(3k-1)/2 and 0 otherwise, together with the identification of that
signed count with the coefficient of X^n in the truncated product over ℤ⟦X⟧. It builds on
Mathlib's
Nat.Partition.genFun, whose module docstring lists "generating function for thepartition function p(n) (TODO: prove this)" — which
coeff_pGenFun_eq_p_counthere effectivelydoes.
The q-series route develops q-Pochhammer symbols, the Gaussian binomial coefficient, Euler's two
identities and the Cauchy identity, proves the Jacobi triple product both as a formal power
series identity over an arbitrary commutative ring and analytically over ℂ for ‖q‖ < 1, and
reaches the same theorem for the infinite product by specialization. We include it because it is
much the more reusable half: that machinery is general-purpose, whereas the Franklin route is
specific to this theorem. We note that q-series identities including the Jacobi triple product
have been formalized in Lean before [see arXiv:2607.01544]; we claim no priority.
On provenance, which we would record as
AI: the Lean proofs in both routes were largelygenerated by Aristotle (Harmonic). The two differ in how much human direction and checking went
in. The Franklin route (1264 lines) follows a blueprint we wrote ourselves, lemma by lemma, and
carries substantially more manual intervention and review. The q-series route (3318 lines, 72% of
the project) is machine-generated blueprint and all; our contribution was restructuring the
library, renaming its API to be mathlib-ready and reviewing statements. Claude assisted with proof
development, the blueprint and CI. If you read that split as
mixrather thanAIwe would notobject, but
AIseems the more accurate of the two.The gates, as far as we can check them: 4582 lines of our own Lean across 19 files; no
sorry;axioms limited to propext, Classical.choice and Quot.sound; no
unsafeorpartial; Apache-2.0;a file header on all 19 files; largest file 716 lines;
lake build --wfailgreen, with Mathlib'sstandard linter set enabled in
lakefile.tomland enforced in CI.Every formalized declaration is tied to a blueprint entry with a prose statement and proof sketch,
and
leanblueprint checkdeclsenforces in CI that every\lean{}annotation names a declarationthat exists. All 220 public declarations carry docstrings. Blueprint, dependency graph and
doc-gen4 API documentation are at https://viazovska.github.io/PentagonalNumberTheorem/.
PentagonalNumberTheorem.leanimports both halves, if a single entry module helps.We can also open a content PR under
LeanPool/instead if you would prefer; a project card isdrafted and ready.