CounterExamples in Topology

Stream: maths

[Suryansh Shrivastava]

Hello all! I am a 5th year BS-MS student from IISc and I have been working on formalising Counter-Examples in Topology from this book :-Counter Examples in Topology , here is my websiteCounterExamples. So, any comments about my code will be deeply appreciated.The main objective of this project is to make Counter Examples and some tactics so that for any given conjecture in topology, one can use a formal tactic to specialize it for that particular topological space and give an instant disproof of it.

[Suryansh Shrivastava]

I am also open to collaborate

[Junyan Xu]

pi-base is a project that also centers around that book, and coincidentally they now has a PR open for mathlib integration.

[Junyan Xu]

I think all (counter)examples could go into mathlib archive, and missing properties of spaces will go into mathlib proper.

[Suryansh Shrivastava]

Junyan Xu said:

I think all (counter)examples could go into mathlib archive, and missing properties of spaces will go into mathlib proper.

How does one contribute to mathlib archive?

[Aaron Anderson]

You'll want these instructions: https://leanprover-community.github.io/contribute/index.html

[Scott Morrison]

(To clarify, the "archive" is just the Archive/ subdirectory of the mathlib4 repository. The rule is that you can't / shouldn't import things from the Archive/ directory.)

[Johan Commelin]

There is also Counterexamples/ which might also be a suitable place for these results.

[Mario Carneiro]

I think some of the "counterexamples in topology" are already there

[Yury G. Kudryashov]

If some spaces can be useful outside of the "counterexample" settings, then they can go to Topology/Instances.