Formalizing Moessner’s theorem and generalizations in Nuprl

Se ha publicado un artículo de razonamiento formalizado en Nuplr titulado Formalizing Moessner’s theorem and generalizations in Nuprl.

Sus autores son

• Mark Bickford (de la Univ. de Cornell),
• Dexter Kozen (de la Univ. de Cornell) y
• Alexandra Silva (de la Radboud University Nijmegen).

Su resumen es

Moessner’s theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers . 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. To the best of our knowledge, this is the first existing machine formalization. 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.