It’s alive! Go look!

The π-Base is a database of topological information, similar to Steen & Seebach’s classic Counterexamples in Topology, but with automated deduction and powerful search. It is the tool that I wished existed when I started looking into cozero complemented spaces, replacing a stultifying literature search with the following process:

• Add the cozero complemented property
• Record its relationships with other known properties: perfectly normal, completely regular and ccc
• Let the site deduce what it can about the examples it knows about
• Query for spaces which are not determined by the known theorems

The ultimate goal being to pool knowledge about interesting examples, and to let people get straight to examining interesting cases in hopes of extrapolating out new theorems (… which go back in to the database, creating a nice little feedback loop).

I also hope that the site can be a useful pedagogical tool, since it lets students explore results that may seem counterintuitive, and since all deductions are traceable back to first principles. Austin Mohr - an Assistant Professor at Nebraska Wesleyan University - has been working in this direction, and I am indebted for his contributions.

Planned Features

There are several planned improvements for the site, most of which are in the Github issue tracker. If anything would be particularly useful to you, please create a feature request there (or :+1: an existing one).

As it stands, deduction is fairly simple-minded, essentially just applying modus ponens / tollens. My hope is to one day integrate with existing proof assistants like Coq, so that we can formally describe the internal structure of these spaces and verify all assertions. This should also allow us to track more subtle interactions like spaces embedding in others, or properties being weakly hereditary. This is a large task, but if you are interested in helping, please get in touch with me.

Getting Involved

Ultimately the best thing you can do is just use the site. If you find bugs, file a bug report (though I should automatically get an email if the server errors). If you’d like a features that doesn’t exist yet, file a feature request. If you have any comments or questions drop me a line. Any user is able to add new spaces, properties and theorems, so feel free to contribute whatever your interest is. There are some admin-only tools, like deleting false assertions and reverting edits - please contact me if you need any of those.

I have added several assertions without proof, for the sake of getting interesting search results. You can see those on each space under the “needing proof tab”. It would be a big help if you can fill these in. Along those lines, there is a “contribute” button in the nav bar that will take you to a random assertion in need of a proof.

If you are interested in contributing to the software side of things, there is a Github repo. Pull requests welcome. If you are interested, but don’t have the Haskell chops or don’t know where to start, get in touch and I’ll be glad to work with you.

Happy Topologizing!