Formal definition of numbers is the foundation of formal verification of software. However, due to the complexity and flexibility of mathematical proofs in classical real number theory, it is difficult to formalize real number in formal proof systems like Coq.

This project is aimed to implement the formal definition and completeness proof of real numbers constructed by the Cauchy sequence in Coq. We will first formalize the definition of real number, according to the mainstream mathematical analysis textbooks, and then prove that real number field constructed satisfies the real number axioms either by formalizing the existing proof in maths or through a more suitable proof in Coq. It turns out that the completeness of real numbers constructed by Cauchy sequence can be formally verified in Coq.

What’s more, we have constructed an injection from a non-empty, single-element set of real numbers to a particular real number in this paper, which makes our formalization more portable and useful to further work.

In conclusion, it is feasible to construct classical real numbers from rational numbers in formal verification systems, and the real number field we construct can be applied to higher order proofs.