A Formal Study of Moessner's Sieve

In this dissertation, we present a new characterization of Moessner's sieve that brings a range of new results with it. As such, we present a dual to Moessner's sieve that generates a sequence of so-called Moessner triangles, instead of a traditional sequence of successive powers, where each triangle is generated column by column, instead of row by row. Furthermore, we present a new characteristic function of Moessner's sieve that calculates the entries of the Moessner triangles generated by Moessner's sieve, without having to calculate the prefix of the sequence.
We prove Moessner's theorem adapted to our new dual sieve, called Moessner's idealized theorem, where we generalize the initial configuration from a sequence of natural numbers to a seed tuple containing just one non-zero entry. We discover a new property of Moessner's sieve that connects Moessner triangles of different rank, thus acting as a dual to the existing relation between Moessner triangles of different index, thereby suggesting the presence of a 2-dimensional grid of triangles, rather than the traditional 1-dimensional sequence of values.
We adapt Long's theorem to the dual sieve and obtain a simplified initial configuration of Long's theorem, consisting of a seed tuple of two non-zero entries. We conjecture a new generalization of Long's theorem that has a seed tuple of arbitrary entries for its initial configuration and connects Moessner's sieve with polynomial evaluation. Lastly, we approach the connection between Moessner's sieve and polynomial evaluation from an alternative perspective and prove an equivalence relation between the triangle creation procedures of Moessner's sieve and the repeated application of Horner's method for polynomial division.
All results presented in this dissertation have been formalized in the Coq proof assistant and proved using a minimal subset of the constructs and tactics available in the Coq language. As such, we demonstrate the potential of proof assistants to inspire new results while lowering the gap between programs (in computer science) and proofs (in mathematics).