A wiki-like mathematical structure/example data base
I can imagine this better as an online service than a locally running software, but nevertheless I imagine it to be very useful.
You ever wondered (because of your research or out of curiosity) whether there is an example of a structure A (e.g. a topological space, graph, group, ...) which has the properties B, C and D, but not E? If Yes, what is an example of such a structure? If No, how can this be proven?
Wouldn't it be nice to have an online service, something like Wikipedia, where you can enter that you are browsing the database of structures A, and you specify the filters [B], [C], [D] and [not E]. You press enter and it spits out:
- Here is an example of such a structure: ...
- These structures are exactly the 3-dimensional compact manifolds. An example would be: ...
- No structure can have this combination of properties. Source: ...
- It is conjectured that no such structure exists. Source: ...
- It is a known open problem whether there is such a structure: Read more here: ...
- Property [B] and [C] imply [D] and [not E]. Hence you are actually looking for structures A with only [D] and [not E].
- The database does not contain information on this combination of properties. Do you want to extend the knowledge?
"wiki-like" means that the database's knowledge can be extended/corrected by anyone $-$ like in Wikipedia. Even though this might seem like a complicated semantic search engine, I think that the strong formalization we have in mathmatics enables us to choose a strict syntax for the input.
- We always specify the general structure we are looking for, e.g. vector space, topological space, metric space, group, ring, field, graph, function $\Bbb R\to\Bbb R$, subset of $\Bbb R$, curve (in metric space), field-automorphism, ...
- It follows a list of properties, e.g. finite, compact, 3-dimensional, connected, Hausdorff, has inner point, metrizable, bijective, ... . Every such property can be suffixed with a [not]-operator. The listed properties are joined by conjunction.
The structures and property names are no free-form input, but chosen from a pop-up menu or by auto-completion, so that the users know what to input. The database should implement very basic reasoning, e.g.
- If a property A implies B, and B implies C, so does A imply C.
- If A and B contradict each other and C implies A, so C and B contradict each other too.
- The structures can be linked, e.g. every metric space is a topological space (by its induced topology). Hence, every property which is available for topological spaces, is also available for metric spaces.
I know of several such services of varying generality: e.g. for rings, groups, graphs (here and here), polyhedra, or general counterexamples. The differences to what I am looking for can mostly be described by the following points:
- General: I want a combined database for all/most structures. All this under a common interface.
- Extendable: I think everyone should be allowed to add his knowledge to the database.
- Searchable: Most of the time I know only the names (or some names or vague descriptions) of some properties of the desired structure. I do not know the structures name. Hence I want to filter by these properties. Sometimes I might be not even interested in examples, but in the relation between two properties: e.g. do they contradict each other, are they the same, does one imply the other, ...?
- Structured: Not a loose collection of examples/counterexamples/articles, but highly interconnected and analysable data.
- Userfriendly/Beautiful: I think mathcounterexamples and of course StackExchange is a good demonstration of these goals.
I once had an idea how this can be realized. I even asked a question on Computer Science StackExchange to see whether useful data structure for this kind of task already exist. I would love to realize such a project, but I am definitely lacking the web-developer skills, and currently also the time.