Repository navigation
Reduce derived proofs #82
Description
The proof that a 2-point discrete space is T2.5 uses an assumption that the space is Finite, but the proof that a countably infinite discrete space is T2.5 finds a simpler, more natural proof using just the Discrete assumption.
It's almost certainly computationally infeasible to generate the "most natural" proof (if that's even well-defined), but we can look at some reasonable heuristics and simplification strategies. One straightforward one to implement would be –
- prefer "less complex" proofs
- record proofs exactly as we do today
- at display time, search for alternate proofs, removing assumptions
Activity
StevenClontz commentedon Nov 13, 2023
So I had some trouble parsing this graph: https://graph.topology.pages.dev/spaces/S000002/properties/P000044 One thing that'd help a lot is color-coding whether properties are true or false.
Another thing that'd help: for compound theorems, I think we really need a directed hypergraph: https://en.wikipedia.org/wiki/Hypergraph#/media/File:Directed_hypergraph_example.svg So for
P and Q then R, we should show an arrow starting fromPandQand pointing toR.StevenClontz commentedon Nov 13, 2023
The other thing that would have helped me: presenting T309 as the equivalent
Cardinality<c + not Strongly Connected => not Connectedbecause nested contrapositives are hard.