Community Call 10/18 - Tools using and displaying direct implications between properties

[danflapjax]

@StevenClontz: We'll have a call to discuss this tool Friday Oct 18 at 4pm Eastern at https://southalabama.zoom.us/j/93833246214

---

I mentioned in a community call that I had been working on a tool implementing my ideas on computing and displaying all of the direct implications between properties (see this for example). There is still much that I would like to add to it, but it has already been paying dividends in my contributions, so I think it's time to share it: https://observablehq.com/@dinod123/pi-base-tools Note that all graphs are zoomable by scrolling or pinching on touchscreen and all nodes and edges are hyperlinks to the main site.

Interestingly, my tool is able to derive 5 more traits of spaces than the main website has, but I have not yet investigated what those traits are.

Some example outputs, for the search P123 Locally n-Euclidean ∧ ¬P78 Finite.

It's hard to find attractive screenshots of the full graph of direct implications, but here's a subset for a search I was actively referencing while working on PR #800: P1 T0 ∧ P90 Alexandrov ∧ P181 Countably infinite ∧ P196 Hereditarily connected. Green nodes are ones where a space with the property exists, and green edges are ones where the converse fails for some space. Without referencing the results for this search, I could not have managed to find as many theorems or traits to add as I did.

[prabau]

This is seriously impressive! Beautifully presented results.

[StevenClontz]

Yes, very nice. If you happen to be available at the usual time (4pm Eastern) this Friday, perhaps we can have a show-and-tell community call? I'd like to see you showcase this and ponder how we might get some of this functionality into pi-Base directly.

[danflapjax]

Yeah, I should be available to meet then.

[StevenClontz]

Cool! See you in about an hour.

[StevenClontz]

Thanks all for today's discussion. Merging pi-base/web#181 and should have the link ready at https://topology.pi-base.org/dev soon.