Together with doctoral student Eloi Torrents (from UAB) we have started a project to formalize the construction of real numbers from the book "Constructive analysis" (written by Douglas S. Bridges and Errett Bishop).

We have based our definition on the book mentioned before but, we have reformulated some parts with topological filters. In a near future, we will write down all the changes we have made in a paper.

If you want to see the GitHub repository you can see it here.