A machine-checked formalization of recurrence and creative-telescoping certificates for Ore algebras, in Lean 4 — with an interactive blueprint linking every statement to its Lean declaration.
Ore algebras give a common language for operators such as
shift, difference, and q‑dilation acting
on sequences. Creative telescoping turns a double sum into a
one-dimensional recurrence; verifying the certificates by hand is
error-prone, so we verify them in Lean — no sorry,
Mathlib axioms aside.
The interactive blueprint breaks the argument into definitions, lemmas, and theorems, shows what each result depends on, and links each one to the corresponding Lean declaration. The coverage table maps every result of the paper to its verified declaration and status.
Classical creative-telescoping certificate, six-term recurrence, uniqueness, closed form. Fully proved.
q-analogues of the Stirling identities; the corrected convention for Id. 2 was detected and proved.
OEIS recurrence benchmarks (Fibonacci, Tribonacci, Pascal, …) and sympy cross-checks in the CI harness.
The formalization produced reusable Lean infrastructure for q-analogs and recurrence-defined special numbers, not only one-off proofs of the paper. The library guide documents what you can import and build on:
Special.QAnalogq-integers qNat, Gaussian binomials qBinom, and the q-Stirling triangles qStirling1, qStirling2, qStirling1Tilde, with their recurrence skeletons — generic over CommSemiring/CommRing.
Special.QEulerianCarlitz q-Eulerian numbers qEulerian with recurrence, support, diagonal, and first-column lemmas.
Benchmarks.OEISEight OEIS recurrence benchmarks (Fibonacci, Tribonacci, central binomial, program-derived sequences, …) proved equal to their closed forms by recurrence uniqueness.
Quick import test (values verified by lake env lean):
#eval qNat ℚ 2 5 → 31,
#eval qBinom ℚ 2 5 2 → 155,
#eval qEulerian ℚ 2 3 2 → 12.
Longer-term, generated doc-gen4 API docs will let readers
browse declarations module-by-module; for now see the curated
library guide and the
blueprint for per-declaration links.
The formalization is not just a transcription of final identities. Lean checks the algebraic infrastructure used to prove them: q-analogs, Stirling triangles, q-Eulerian numbers, recurrence operators, certificates, telescoping sums, boundary terms, uniqueness arguments, and final closed forms.
CAS scripts check printed formulas on finite exact-arithmetic grids, audit conventions, and reproduce exploratory searches. The trusted mathematical statements are the Lean declarations linked in the blueprint.
Lean is the certificate checker and proof archive; Python/CAS is the lab notebook.
| Layer | Role |
|---|---|
OreAlgebraLib/Papers/KauersSchneider/Section2.lean |
Kauers–Schneider Section 2 recurrence and closed form |
OreAlgebraLib/Papers/KauersSchneider/Section3.lean |
q-identities, corrected statements, certificates, final identities |
OreAlgebraLib/Special/QAnalog.lean |
reusable q-numbers, q-binomial, q-Stirling definitions |
OreAlgebraLib/Special/QEulerian.lean |
Carlitz q-Eulerian numbers and recurrence lemmas |
OreAlgebraLib/Benchmarks/OEIS.lean |
recurrence benchmark examples |
cas/ |
untrusted exact-rational audits and convention searches |
The coverage distinguishes Lean proofs, positive CAS checks, and historical negative controls under alternative conventions. A negative control is not a failed Lean proof, and a passing finite CAS check is not a general theorem.
Sections 2 and 3: the classical Stirling identity and its
q-analogues. The coverage table
identifies the proved declarations and the remaining formalizations.
For weighted Id. 2, Lean proves the printed recurrence, closed form,
printed certificate, and the weighted boundary and range
reconciliation layers. The Id. 4 printed certificate's pointwise
identity is also proved. The classical closing Remark's rescaled
normalization is fully proved (Section3Remark.lean):
pointwise certificate, telescoping, and — at full-grid generality
with no hypotheses — the 6-term series vanishing
remarkOpSeriesR_eq_zero_full, giving the printed
recurrence for q ≠ 0 alone; the printed-object
transport layer (bridge remarkGp_eq, certificate
g, pointwise/boundary/telescoping on the printed
normalization, incl. the k = m endpoint and the full
range Icc m n) is now also proved on the certificate
domain (q ≠ 0, q^(m+1), q^(m+2) ≠ 1).
Reproducible scripts under cas/ check the current
weighted Id. 2 and Id. 4 formulas and the classical closing Remark.
The verification harness also tracks historical negative controls.
These computations provide evidence, not Lean proofs.
Every definition, lemma, and theorem gets a label, a precise statement, and its dependencies — giving the order to formalize.
Machine-checked proofs with a proof-gap scan: no sorry, axiom, or unsafe in the library.
scripts/check_all.py gates every commit: Lean build, blueprint↔Lean links, OEIS data, and CAS reproducibility.