{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T16:41:38Z","timestamp":1777480898808,"version":"3.51.4"},"reference-count":11,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,9,1]]},"abstract":"Summary<\/jats:title>\n \n Surreal numbers, a fascinating mathematical concept introduced by John Conway, have attracted considerable interest due to their unique properties. In this article, we formalize the basic concept of surreal numbers close to the original Conway\u2019s convention in the field of combinatorial game theory. We define surreal numbers with the pre-order in the Mizar system which satisfy the following condition:\n x<\/jats:italic>\n \u2a7d\n y<\/jats:italic>\n iff\n \n L\n x<\/jats:sub>\n <\/jats:italic>\n \u226a {\n y<\/jats:italic>\n }\n \u039b<\/jats:italic>\n {\n x<\/jats:italic>\n } \u226a\n \n R\n y<\/jats:sub>\n <\/jats:italic>\n .\n <\/jats:p>","DOI":"10.2478\/forma-2023-0018","type":"journal-article","created":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T13:42:33Z","timestamp":1704116553000},"page":"193-203","source":"Crossref","is-referenced-by-count":6,"title":["Conway Numbers \u2013 Formal Introduction"],"prefix":"10.2478","volume":"31","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"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2023,12,31]]},"reference":[{"key":"2026042801415298237_j_forma-2023-0018_ref_001","unstructured":"John Horton Conway. On Numbers and Games. A K Peters Ltd., Natick, MA, second edition, 2001. ISBN 1-56881-127-6."},{"key":"2026042801415298237_j_forma-2023-0018_ref_002","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":"2026042801415298237_j_forma-2023-0018_ref_003","doi-asserted-by":"crossref","unstructured":"Philip Ehrlich. Conway names, the simplicity hierarchy and the surreal number tree. Journal of Logic and Analysis, 3(1):1\u201326, 2011. doi:10.4115\/jla.2011.3.1.","DOI":"10.4115\/jla.2011.3.1"},{"key":"2026042801415298237_j_forma-2023-0018_ref_004","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":"2026042801415298237_j_forma-2023-0018_ref_005","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":"2026042801415298237_j_forma-2023-0018_ref_006","unstructured":"Adam Grabowski, Artur Korni\u0142owicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153\u2013245, 2010."},{"key":"2026042801415298237_j_forma-2023-0018_ref_007","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":"2026042801415298237_j_forma-2023-0018_ref_008","doi-asserted-by":"crossref","unstructured":"Robin Nittka. Conway\u2019s games and some of their basic properties. Formalized Mathematics, 19(2):73\u201381, 2011. doi:10.2478\/v10037-011-0013-6.","DOI":"10.2478\/v10037-011-0013-6"},{"key":"2026042801415298237_j_forma-2023-0018_ref_009","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":"2026042801415298237_j_forma-2023-0018_ref_010","doi-asserted-by":"crossref","unstructured":"Karol P\u0105k. Prime representing polynomial. Formalized Mathematics, 29(4):221\u2013228, 2021. doi:10.2478\/forma-2021-0020.","DOI":"10.2478\/forma-2021-0020"},{"key":"2026042801415298237_j_forma-2023-0018_ref_011","doi-asserted-by":"crossref","unstructured":"Karol P\u0105k. Prime representing polynomial with 10 unknowns. Formalized Mathematics, 30(4):255\u2013279, 2022. doi:10.2478\/forma-2022-0021.","DOI":"10.2478\/forma-2022-0021"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2023-0018","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T14:10:52Z","timestamp":1777385452000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2023-0018"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,1]]},"references-count":11,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2023,12,31]]},"published-print":{"date-parts":[[2023,9,1]]}},"alternative-id":["10.2478\/forma-2023-0018"],"URL":"https:\/\/doi.org\/10.2478\/forma-2023-0018","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,1]]}}}