Proving the Standard Part Principle in Nonstandard Analysis with Rocq Prover

The Standard Part Principle (SPP) is a fundamental theorem relevant to the hyperreal numbers that serve as the foundation of nonstandard analysis. SPP asserts that each finite hyperreal number can be represented as the sum of a standard real number and an infinitesimal, which clearly reflects the structure of finite hyperreal numbers. This paper presents a formal proof of the Standard Part Principle, implemented using the Rocq Prover and grounded in Morse-Kelley axiomatic set theory. Formalizing this theorem in a computer could facilitate the understanding of hyperreal numbers and provides an effective approach to learn about nonstandard analysis. The implementation includes a formal construction of hyperreal numbers, the formal verification of some fundamental arithmetical properties, and the formal proof of SPP. This work sets the foundation for the formalization of nonstandard analysis.