基于 Morse-Kelley（MK）公理化集合论框架，在 Lean 4 定理证明器中完成了实数公理系统的完整形式化。实数集 R 被声明为 MK 中的一个类，加法与乘法被定义为 R×R 上的 MK 函数，序关系被定义为 R×R 的子类。公理系统涵盖域公理（加法与乘法的封闭性、结合律、交换律、单位元、逆元与分配律）、序公理（自反性、反对称性、传递性与全序性）、完备性公理及加法与乘法的序相容性公理。在此基础上，推导并形式化验证了加法逆元与乘法逆元的存在唯一性、上确界与下确界定理、自然数集 N、整数集 Z 与有理数集 Q 的构造及其代数性质、数学归纳法、无理数的存在性、Archimedes 性质以及绝对值与距离的基本性质。全部定义与定理均通过 Lean 4 类型检查器的验证。