Email Gateway (Aug 18 2022 at 14:05): Email Gateway (Aug 18 2022 at 14:05):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi out there,
here at TUM we plan to start a student project formalizing factorial
chains, Stirling numbers, discrete summation and related stuff, which
seems yet underrepresented in the formal area, at least according to
Google and the Isabelle repositories. However, to avoid work in
parallel, I would like to ask whether somebody out there is working in
that direction or has some related stuff in the drawer.
Any feedback welcome,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:10):From: Amine Chaieb <ac638@cam.ac.uk>
For an example in my PhD I formalized Stirling numbers of the first and
second kind (more about 2nd kind) and the main theorem that transforms
normal powers as sums of falling powers with stirling numbers (2nd
kind). There is also a simple part about forward differentiation and
those operators you need for discrete summation. Basic stuff, no
hypergeometric summation and the like. Of course in the drawer... I'll
send it over.
Best wishes,
Amine.
Florian Haftmann wrote:
Last updated: Apr 19 2024 at 04:17 UTC