Formalizing Moessner's theorem and generalizations in Nuprl

Moessner's theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers 1n, 2n, 3n, … . Several generalizations of Moessner's theorem exist. Recently, Kozen and Silva gave an algebraic proof of a general theorem that su...

Full description

Saved in:
Bibliographic Details
Published in:Journal of logical and algebraic methods in programming 2022-01, Vol.124, p.100713, Article 100713
Main Authors: Bickford, Mark, Kozen, Dexter, Silva, Alexandra
Format: Article
Language:English
Subjects:
Formalization
Moessner's theorem
Nuprl
Pascal triangle
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Moessner's theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers 1n, 2n, 3n, … . Several generalizations of Moessner's theorem exist. Recently, Kozen and Silva gave an algebraic proof of a general theorem that subsumes Moessner's original theorem and its known generalizations. In this note, we describe the formalization of this theorem that the first author did in Nuprl. On the one hand, the formalization remains remarkably close to the original proof. On the other hand, it leads to new insights in the proof, pointing to small gaps and ambiguities that would never raise any objections in pen and pencil proofs, but which must be resolved in machine formalization.
ISSN:2352-2208
DOI:10.1016/j.jlamp.2021.100713