4
$\begingroup$

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 .

Improve this question
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Philippe Gaucher
    Commented May 2, 2018 at 8:15

2 Answers 2

Reset to default
8
$\begingroup$

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.

Improve this answer
$\endgroup$
5
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .