{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T11:04:48Z","timestamp":1774868688584,"version":"3.50.1"},"reference-count":22,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2025,9,1]],"date-time":"2025-09-01T00:00:00Z","timestamp":1756684800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,9,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>The concept of surreal numbers, as postulated by John Conway, represents a complex and multifaceted structure that encompasses a multitude of familiar number systems, including the real numbers, as integral components. In this study, we undertake the construction of the real numbers, commencing with the integers and dyadic rationals as preliminary steps. We proceed to contrast the resulting set of real numbers derived from our construction with the axiomatically defined set of real numbers based on Conway\u2019s axiom. Our findings reveal that both approaches culminate in the same set.<\/jats:p>","DOI":"10.2478\/forma-2025-0002","type":"journal-article","created":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T16:21:37Z","timestamp":1760372497000},"page":"11-23","source":"Crossref","is-referenced-by-count":1,"title":["Surreal Dyadic and Real Numbers: A Formal Construction"],"prefix":"10.2478","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7099-1669","authenticated-orcid":false,"given":"Karol","family":"P\u0105k","sequence":"first","affiliation":[{"name":"Faculty of Computer Science , University of Bia\u0142ystok , Poland"}]}],"member":"374","published-online":{"date-parts":[[2025,9,30]]},"reference":[{"key":"2026033010152229018_j_forma-2025-0002_ref_001","doi-asserted-by":"crossref","unstructured":"Vincent Bagayoko and Joris van der Hoeven. Surreal substructures. Fundamenta Mathematicae, 266(1):25\u201396, 2024. doi:10.4064\/fm231020-23-2.","DOI":"10.4064\/fm231020-23-2"},{"key":"2026033010152229018_j_forma-2025-0002_ref_002","unstructured":"Wolfgang Bertram. On Conway\u2019s numbers and games, the von Neumann universe, and pure set theory. ArXiv preprint arXiv:2501.04412, 2025."},{"key":"2026033010152229018_j_forma-2025-0002_ref_003","unstructured":"John Horton Conway. On Numbers and Games. A K Peters Ltd., Natick, MA, second edition, 2001. ISBN 1-56881-127-6."},{"key":"2026033010152229018_j_forma-2025-0002_ref_004","doi-asserted-by":"crossref","unstructured":"Ovidiu Costin and Philip Ehrlich. Integration on the surreals. Advances in Mathematics, 452:109823, 2024. doi:10.1016\/j.aim.2024.109823.","DOI":"10.1016\/j.aim.2024.109823"},{"key":"2026033010152229018_j_forma-2025-0002_ref_005","doi-asserted-by":"crossref","unstructured":"Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic, 65(2):525\u2013549, 2000. doi:10.2307\/2586554.","DOI":"10.2307\/2586554"},{"key":"2026033010152229018_j_forma-2025-0002_ref_006","doi-asserted-by":"crossref","unstructured":"Philip Ehrlich. The absolute arithmetic continuum and the unification of all numbers great and small. The Bulletin of Symbolic Logic, 18(1):1\u201345, 2012. doi:10.2178\/bsl\/1327328438.","DOI":"10.2178\/bsl\/1327328438"},{"key":"2026033010152229018_j_forma-2025-0002_ref_007","doi-asserted-by":"crossref","unstructured":"Philp Ehrlich. Number systems with simplicity hierarchies: A generalization of Conway\u2019s theory of surreal numbers. Journal of Symbolic Logic, 66(3):1231\u20131258, 2001. doi:10.2307\/2695104.","DOI":"10.2307\/2695104"},{"key":"2026033010152229018_j_forma-2025-0002_ref_008","doi-asserted-by":"crossref","unstructured":"Harry Gonshor. An Introduction to the Theory of Surreal Numbers. London Mathematical Society Lecture Note Series, 110. Cambridge University Press, 1986. ISBN 0521312051.","DOI":"10.1017\/CBO9780511629143"},{"key":"2026033010152229018_j_forma-2025-0002_ref_009","unstructured":"Donald E. Knuth. Surreal Numbers: How Two Ex-students Turned on to Pure Mathematics and Found Total Happiness. Addison-Wesley, 1974."},{"key":"2026033010152229018_j_forma-2025-0002_ref_010","doi-asserted-by":"crossref","unstructured":"Lionel Elie Mamane. Surreal numbers in Coq. In Jean-Christophe Filli\u00e2tre, Christine Paulin-Mohring, and Benjamin Werner, editors, Types for Proofs and Programs, TYPES 2004, volume 3839 of LNCS, pages 170\u2013185. Springer, 2004. doi:10.1007\/11617990 11.","DOI":"10.1007\/11617990_11"},{"key":"2026033010152229018_j_forma-2025-0002_ref_011","doi-asserted-by":"crossref","unstructured":"J. A. Nieto, J. A. Escalante-Javalera, C. A. Somera-Patr\u00f3n, and E. J. Villasenor-Gonz\u00e1lez. Parity of dyadic rationals and surreal numbers. Far East Journal of Mathematical Sciences (FJMS), (2):155\u2013167, May 2024. doi:10.17654\/0972087124010.","DOI":"10.17654\/0972087124010"},{"key":"2026033010152229018_j_forma-2025-0002_ref_012","doi-asserted-by":"crossref","unstructured":"Steven Obua. Partizan games in Isabelle\/HOLZF. In Kamel Barkaoui, Ana Cavalcanti, and Antonio Cerone, editors, Theoretical Aspects of Computing \u2013 ICTAC 2006, volume 4281 of LNCS, pages 272\u2013286. Springer, 2006.","DOI":"10.1007\/11921240_19"},{"key":"2026033010152229018_j_forma-2025-0002_ref_013","doi-asserted-by":"crossref","unstructured":"Karol P\u0105k. Conway numbers \u2013 formal introduction. Formalized Mathematics, 31(1): 193\u2013203, 2023. doi:10.2478\/forma-2023-0018.","DOI":"10.2478\/forma-2023-0018"},{"key":"2026033010152229018_j_forma-2025-0002_ref_014","doi-asserted-by":"crossref","unstructured":"Karol P\u0105k. Integration of game theoretic and tree theoretic approaches to Conway numbers. Formalized Mathematics, 31(1):205\u2013213, 2023. doi:10.2478\/forma-2023-0019.","DOI":"10.2478\/forma-2023-0019"},{"key":"2026033010152229018_j_forma-2025-0002_ref_015","doi-asserted-by":"crossref","unstructured":"Karol P\u0105k. The ring of Conway numbers in Mizar. Formalized Mathematics, 31(1): 215\u2013228, 2023. doi:10.2478\/forma-2023-0020.","DOI":"10.2478\/forma-2023-0020"},{"key":"2026033010152229018_j_forma-2025-0002_ref_016","unstructured":"Karol P\u0105k and Cezary Kaliszyk. Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers. In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, 15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia, volume 309 of LIPIcs, pages 29:1\u201329:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 2024. doi:10.4230\/LIPICS.ITP.2024.29."},{"key":"2026033010152229018_j_forma-2025-0002_ref_017","doi-asserted-by":"crossref","unstructured":"Matthew Roughan. Practically surreal: surreal arithmetic in Julia. SoftwareX, 9:293\u2013298, 2019. doi:10.1016\/j.softx.2019.03.005.","DOI":"10.1016\/j.softx.2019.03.005"},{"key":"2026033010152229018_j_forma-2025-0002_ref_018","doi-asserted-by":"crossref","unstructured":"Alex Ryba, Philip Ehrlich, Richard Kenyon, Jeffrey Lagarias, James Propp, and Louis Kauffman. Conway\u2019s mathematics after Conway. Notices of the American Mathematical Society, 69:1145\u20131155, 2022. doi:10.1090\/noti2513.","DOI":"10.1090\/noti2513"},{"key":"2026033010152229018_j_forma-2025-0002_ref_019","doi-asserted-by":"crossref","unstructured":"Dominik Tomaszuk, \u0141ukasz Szeremeta, and Artur Korni\u0142owicz. MMLKG: Knowledge graph for mathematical definitions, statements and proofs. Scientific Data, 10(1), 2023. doi:10.1038\/s41597-023-02681-3.","DOI":"10.1038\/s41597-023-02681-3"},{"key":"2026033010152229018_j_forma-2025-0002_ref_020","unstructured":"Claus T\u00f8ndering. Surreal numbers \u2013 an introduction. HTTP, version 1.7, December 2019."},{"key":"2026033010152229018_j_forma-2025-0002_ref_021","unstructured":"The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study, 2013."},{"key":"2026033010152229018_j_forma-2025-0002_ref_022","doi-asserted-by":"crossref","unstructured":"Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle framework. In Otmane Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar, editors, Theorem Proving in Higher Order Logics, pages 33\u201338. Springer Berlin Heidelberg, 2008.","DOI":"10.1007\/978-3-540-71067-7_7"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.sciendo.com\/pdf\/10.2478\/forma-2025-0002","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T10:15:41Z","timestamp":1774865741000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.2478\/forma-2025-0002"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,1]]},"references-count":22,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2025,9,30]]},"published-print":{"date-parts":[[2025,9,1]]}},"alternative-id":["10.2478\/forma-2025-0002"],"URL":"https:\/\/doi.org\/10.2478\/forma-2025-0002","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,1]]}}}