Reseña: Formalizing ordinal partition relations using Isabelle/HOL
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre combinatoria titulado Formalizing ordinal partition relations using Isabelle/HOL.
Sus autores son
- Mirna Džamonja (del IRIF (Institut de Recherche en Informatique Fondamentale) , CNRS-Université de Paris),
- Angeliki Koutsoukou-Argyraki (del Automated Reasoning Group en la Universidad de Cambridge) y
- Lawrence C. Paulson (del Automated Reasoning Group en la Universidad de Cambridge).
Su resumen es
This is an overview of a formalization project in the proof assistant Isabelle/HOL of a number of research results in infinitary combinatorics and set theory (more specifically in ordinal partition relations) by Erdős–Milner, Specker, Larson and Nash-Williams, leading to Larson’s proof of the unpublished result by E.C. Milner asserting that for all m ∈ ℕ, ω^ω → (ω^ω,m). This material has been recently formalised by Paulson and is available on the Archive of Formal Proofs; here we discuss some of the most challenging aspects of the formalization process. This project is also a demonstration of working with Zermelo–Fraenkel set theory in higher-order logic.
El trabajo se ha publicado en Experimental Mathematics.
El código de las correspondientes teorías se encuentra aquí.