Conway正规形式：连接超现实数综合形式化的方法

Conway超现实数的真类构成了一个丰富的全序代数闭域，其许多算术和代数性质接近于实数、序数和无穷小数的性质。本文使用Mizar通过两种方法形式化了Conway数的构造，并提出了它们之间的桥梁，旨在结合它们的优势以实现高效的形式化。通过用超限归纳法替换超限归纳-递归法，我们简化了它们的构造。此外，我们引入了一种使用全局选择合并两种方法证明的方法，以促进形式化证明。我们证明了超现实数构成一个域（包括平方根），并且它们包含了诸如实数、序数和$\omega$的幂等子集。我们结合了Conway的工作与Ehrlich的推广，以形式化证明Conway正规形式，为超现实数理论的许多形式化发展铺平了道路。