• 1 Kauers–Schneider verification ▶
    • 1 Section 2: classical Stirling identity
    • 2 Section 3, Id. 1: \(q\)-Stirling of the second kind
    • 3 Section 3, Id. 2: \(q\)-Stirling of the first kind (corrected)
    • 4 Section 3, Id. 3: printed statement (classical \(S_1\)), proved; plus corrected generic-\(q\) analogs
    • 5 Section 3, Id. 4: fully deformed variant (Carlitz-weighted resolution)
    • 6 Section 3, companion report: the signed array form
    • 7 Section 3, Item 5: \(q\)-Worpitzky identity
  • Dependency graph

OreAlgebraLean verification blueprint

OreAlgebraLean contributors

  • 1 Kauers–Schneider verification
    • 1 Section 2: classical Stirling identity
    • 2 Section 3, Id. 1: \(q\)-Stirling of the second kind
    • 3 Section 3, Id. 2: \(q\)-Stirling of the first kind (corrected)
    • 4 Section 3, Id. 3: printed statement (classical \(S_1\)), proved; plus corrected generic-\(q\) analogs
    • 5 Section 3, Id. 4: fully deformed variant (Carlitz-weighted resolution)
    • 6 Section 3, companion report: the signed array form
    • 7 Section 3, Item 5: \(q\)-Worpitzky identity