# 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 .

• It's a old question (almost 2-y old). As a comment, I would say that to the best of my knowledge, there is no formalization of Bourbaki with a proof assistant (but I may be wrong). Concerning this kind of topological argument, the proof assistant Mizar (mizar.org) should have it in its library. – Philippe Gaucher May 2 '18 at 8:15

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.