The q-TSPP theorem | Lean AI formalization leaderboard

Problem statement

Notes: The orbit-counting formula for totally symmetric plane partitions, stated as an identity of integer polynomials after clearing denominators. Coordinates start at zero, and orbits are counted by their unique representatives with weakly increasing coordinates.

Source: Koutschan, Kauers, and Zeilberger (2011), Theorem 1. DOI: 10.1073/pnas.1019186108

Informal solution: Unavailable.

theorem declaration uses `sorry`q_tspp (n : ℕ) :
    QTSPP.generatingPolynomial n *
      (∏ c ∈ QTSPP.sortedTriples n,
        (1 - q ^ (QTSPP.coordinateSum c + 1))) =
    ∏ c ∈ QTSPP.sortedTriples n,
      (1 - q ^ (QTSPP.coordinateSum c + 2)) := byn:ℕ⊢ generatingPolynomial n * ∏ c ∈ sortedTriples n, (1 - Polynomial.X ^ (coordinateSum c + 1)) =
  ∏ c ∈ sortedTriples n, (1 - Polynomial.X ^ (coordinateSum c + 2))
  sorryAll goals completed! 🐙