# Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers

Source: [Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers](<https://www.sota2.com/research/paper/68fa75071e209131cea655f4>)

Collection index: [llms.txt](<https://www.sota2.com/research/llms.txt>)

Data updated: 2025-10-26T03:24:17.272Z

Authors: Karol P\\k{a}k, Cezary Kaliszyk

Published: 2024-09-30T03:55:54.000Z

## Abstract

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 $\\omega$. 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.

## Recorded benchmark results

A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage.

## Original sources and implementation

[Original paper](<https://arxiv.org/abs/2410.00065>)

[PDF](<https://arxiv.org/pdf/2410.00065.pdf>)