Master Thesis Defense: Peter Urbak - A Formal Study of Moessner's Sieve

Title:
 A Formal Study of Moessner's Sieve

Abstract:

 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).