Virtual Talk: An overview of the real numbers in theorem provers: an application with real analysis in Coq

Micaela Mayero
Galilee Institute - Paris Nord University

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

Presentation (PDF File)

Back to Machine Assisted Proofs