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.

翻译：康威超实数的真类构成了一个丰富的全序代数闭域，具有许多与实数、序数和无穷小数相近的算术与代数性质。本文在Mizar系统中通过两种方法形式化了康威数的构造，并提出了连接这两种方法的桥梁，旨在结合其优势以实现高效的形式化。通过用超限归纳替代超限归纳-递归，我们简化了其构造过程。此外，我们引入了一种利用全局选择公理合并两种方法证明的技术，以促进形式化证明。我们证明了超实数构成一个域（包含平方根运算），并且其包含实数、序数及$\omega$的幂等子集。通过将康威的工作与埃利希的推广相结合，我们形式化地证明了康威范式，为超实数理论的诸多形式化发展铺平了道路。