Conway’s Normal Form in the Mizar System

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.