Formalizing real numbers in a formal proof tool represents a particular challenge. It is not only a question of representing numbers in computers but also of preserving all mathematical properties needed to make proofs.
We will review the history of real numbers formalization in different proof assistants and the different ways of formalizing them, before giving an overview of real numbers libraries that exist today in provers. As application, we will finish by presenting real analysis developments in Coq
Copyright. All Rights Reserved.
