2026-08-01T06:59:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20757 2024-09-02T10:03:24Z ddc:004 open_access

Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers Pąk, Karol Kaliszyk, Cezary Surreal numbers Conway normal form Mizar The proper class of Conway’s surreal numbers forms a rich totally ordered algebraically closed field with many arithmetic and algebraic properties close to those of real numbers, the ordinals, and infinitesimal numbers. In this paper, we formalize the construction of Conway’s numbers in Mizar using two approaches and propose a bridge between them, aiming to combine their advantages for efficient formalization. By replacing transfinite induction-recursion with transfinite induction, we streamline their construction. Additionally, we introduce a method to merge proofs from both approaches using global choice, facilitating formal proof. We demonstrate that surreal numbers form a field, including the square root, and that they encompass subsets such as reals, ordinals, and powers of ω. We combined Conway’s work with Ehrlich’s generalization to formally prove Conway’s Normal Form, paving the way for many formal developments in surreal number theory. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Karol Pąk and Cezary Kaliszyk 2024 Is Part Of LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2024.29 urn:nbn:de:0030-drops-207573 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.29 eng https://creativecommons.org/licenses/by/4.0/legalcode