Zulip Chat Archive

Stream: mathlib4

Topic: Pentagonal number theorem: statement & plan

Beibei Xiong (Dec 15 2025 at 13:20):

I’d like to align on the statement and upstream plan for the formalization of the pentagonal number theorem.

Related PR: #31362
Related repo (wwylele @Weiyi Wang ): https://github.com/wwylele/PentagonalNumberTheorem

Points I’d like to confirm:

  1. For the first Mathlib PR, can we take the main statement to be the PowerSeries expansion over ℤ, together with a finite cut-off product, to avoid convergence/topology issues, and derive the “summed over ℕ / ℂ” formulations later as corollaries?

  2. Is there any preference on namespace or file placement to avoid clashes (e.g. something like Nat.Partition.Pentagonal)?

  3. Should error_term_e be postponed for now, or should we require a well-definedness lemma (or alternatively switch to the quadratic-solve approach)?

I’m happy to adapt to other suggestions as well.

Aaron Liu (Dec 15 2025 at 13:24):

looks like you have a lot of good results in here but I don't see the identity of formal power series

Weiyi Wang (Dec 15 2025 at 15:56):

For the first point, I believe mathlib has already handled all topology problems for you, and what's left to prove is mostly algebraic. My repo has demonstrated this. For upstreaming to Mathlib, I don't think we should repeat the machinery about going from finite to infinite. Of course, you should feel free to do so for your own practice

Nick Adfor (Dec 17 2025 at 06:49):

Where does the new work on the pentagonal number theorem published?

Weiyi Wang (Dec 20 2025 at 22:28):

Since you mentioned that I should feel free to continue upstreaming my project, I opened #33143 for the version I had

Weiyi Wang (Dec 21 2025 at 14:07):

... and I coded it up to the relation between even/odd partitions and pentagonal numbers in #33157

Violeta Hernández (Dec 21 2025 at 21:56):

I'd like to mention #33031, which gives a combinatorial proof for a theorem which already has a power series proof. Is this really something we want?

Nick Adfor (Dec 22 2025 at 10:40):

I don't know what she (@Beibei Xiong ) want, but I'm now trying to read some more article about this pentagonal number theorem.

Weiyi Wang (Dec 22 2025 at 13:57):

Nick_adfor said:

Where does the new work on the pentagonal number theorem published?

I don't think there is "new work" on this unless I missed something. This is about formalizing an old proof, right?

Nick Adfor (Dec 22 2025 at 14:12):

Right

Last updated: Feb 28 2026 at 14:05 UTC