formalisation of Bourbaki, General Topology Is there a formalisation of Bourbaki, General Topology book, 
particularly its first chapter? 
Are there formal proofs of elementary topology arguments such as a Hausdorff compact space is necessarily normal? 
There is a project GAIA but it does not seem to do elementary topology.
http://www-sop.inria.fr/apics/gaia .
 A: Someone just drew my attention to this old question, but maybe the answer is still relevant. As mentioned by Reid, Lean mathlib has a lot of Bourbaki general topology. I don't think anyone checked lemma by lemma, but I'm pretty sure chapter I (structures topologiques) and II (structures uniformes) are almost 100% there, and overlooked parts would be easy to add. Large parts of chapter III are also there (or in the perfectoid spaces repository, waiting to be merged in mathlib). Topological groups operations (III.4) are missing, but that is probably the only big hole. Chapter IV (nombres réels) is mostly there (I don't think anyone did semi-continuous functions, and decimal expansion is done but still stuck in another repository if I understand correctly). Chapter V (groupes à un paramètre) is partly done. The first part of chapter VI is done ($\mathbb{R}^n$). Chapter VIII (nombre complexes) is probably mostly done without projective space. Then it becomes more patchy, but metric spaces are there, with Baire theorem.
A: The particular theorem you mention is formalized in the standard library of the Lean theorem prover here.
Comments at the top of this and other files related to topology indicate that "parts of the formalization are based on [...] General Topology", though I don't have a copy to check how much of the book (or its first chapter) is covered.
