Skip to main content

Conway’s Normal Form in the Mizar System Cover

.blurhash-client-img { display: none !important; }

Conway’s Normal Form in the Mizar System

Formalized Mathematics

Volume 33 (2025): Issue 1 (September 2025)

By: Karol Pąk

Open Access

|Sep 2025

Abstract

This paper presents a formal definition of the Conway normal form, a structured representation uniquely suited to characterising surreal numbers by expressing them as sums within a hierarchically ordered group. To this end, we formalise the first sections of the chapter The Structure of the General Surreal Number in Conway’s book. In particular, we define omega maps and prove the existence and uniqueness of the Conway name for surreal numbers.

References

Vincent Bagayoko and Joris van der Hoeven. Surreal substructures. Fundamenta Mathematicae, 266(1):25–96, 2024. doi:10.4064/fm231020-23-2.
Search in Google Scholar Back to article
Alessandro Berarducci, Salma Kuhlmann, Vincenzo Mantova, and Mickaël Matusinski. Exponential fields and Conway’s omega-map. Proceedings of the American Mathematical Society, 151(6):2655–2669, 2023. doi:10.1090/proc/14577.
Search in Google Scholar Back to article
Wolfgang Bertram. On Conway’s numbers and games, the von Neumann universe, and pure set theory. ArXiv preprint arXiv:2501.04412, 2025.
Search in Google Scholar Back to article
John Horton Conway. On Numbers and Games. A K Peters Ltd., Natick, MA, second edition, 2001. ISBN 1-56881-127-6.
Search in Google Scholar Back to article
Ovidiu Costin and Philip Ehrlich. Integration on the surreals. Advances in Mathematics, 452:109823, 2024. doi:10.1016/j.aim.2024.109823.
Search in Google Scholar Back to article
Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic, 65(2):525–549, 2000. doi:10.2307/2586554.
Search in Google Scholar Back to article
Philip Ehrlich. Conway names, the simplicity hierarchy and the surreal number tree. Journal of Logic and Analysis, 3(1):1–26, 2011. doi:10.4115/jla.2011.3.1.
Search in Google Scholar Back to article
Philip Ehrlich. The absolute arithmetic continuum and the unification of all numbers great and small. The Bulletin of Symbolic Logic, 18(1):1–45, 2012. doi:10.2178/bsl/1327328438.
Search in Google Scholar Back to article
Philp Ehrlich. Number systems with simplicity hierarchies: A generalization of Conway’s theory of surreal numbers. Journal of Symbolic Logic, 66(3):1231–1258, 2001. doi:10.2307/2695104.
Search in Google Scholar Back to article
Harry Gonshor. An Introduction to the Theory of Surreal Numbers. London Mathematical Society Lecture Note Series, 110. Cambridge University Press, 1986. ISBN 0521312051.
Search in Google Scholar Back to article
Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.
Search in Google Scholar Back to article
Donald E. Knuth. Surreal Numbers: How Two Ex-students Turned on to Pure Mathematics and Found Total Happiness. Addison-Wesley, 1974.
Search in Google Scholar Back to article
Lionel Elie Mamane. Surreal numbers in Coq. In Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors, Types for Proofs and Programs, TYPES 2004, volume 3839 of LNCS, pages 170–185. Springer, 2004. doi:10.1007/11617990 11.
Search in Google Scholar Back to article
Steven Obua. Partizan games in Isabelle/HOLZF. In Kamel Barkaoui, Ana Cavalcanti, and Antonio Cerone, editors, Theoretical Aspects of Computing – ICTAC 2006, volume 4281 of LNCS, pages 272–286. Springer, 2006.
Search in Google Scholar Back to article
Karol Pąk. Conway numbers – formal introduction. Formalized Mathematics, 31(1): 193–203, 2023. doi:10.2478/forma-2023-0018.
Search in Google Scholar Back to article
Karol Pąk. Surreal dyadic and real numbers: A formal construction. Formalized Mathematics, 33(1):11–23, 2025. doi:10.2478/forma-2025-0002.
Search in Google Scholar Back to article
Karol Pąk. Integration of game theoretic and tree theoretic approaches to Conway numbers. Formalized Mathematics, 31(1):205–213, 2023. doi:10.2478/forma-2023-0019.
Search in Google Scholar Back to article
Karol Pąk 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–29:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.ITP.2024.29.
Search in Google Scholar Back to article
Alex Ryba, Philip Ehrlich, Richard Kenyon, Jeffrey Lagarias, James Propp, and Louis Kauffman. Conway’s mathematics after Conway. Notices of the American Mathematical Society, 69:1145–1155, 2022. doi:10.1090/noti2513.
Search in Google Scholar Back to article
Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle framework. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, pages 33–38. Springer Berlin Heidelberg, 2008.
Search in Google Scholar Back to article

Articles in this issue

DOI: https://doi.org/10.2478/forma-2025-0003 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 25 - 41

Submitted on: Apr 10, 2025

|

Accepted on: Sep 4, 2025

|

Published on: Sep 30, 2025

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Keywords:

surreal number,

Conway’s game,

Related subjects:

Logic and set theory,

Computer sciences,

Artificial intelligence

© 2025 Karol Pąk, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 License.

Volume 33 (2025): Issue 1 (September 2025)

Previous article