🌌 Abstract Spacecraft - diagram chasing for the mathemacians, enthusiasts, and beginners.
-
It's a work in progress. This is the 4th time I've written diagramming code be it on a Django site using Neo4j or in PyQt5 using QGraphicsObjects, so this time it should work. With my Python prototypes the graphics scene speed started to drag. With Django, I just gave up, but that approach would also not approach the speed that we can from your own desktop PC.
For example, once you draw out a diagram, say that it commutes, and you have a surjective module hom f: A -> B and you "Right-click > Take element" x @ B, then you can auto populate an element at A if you want to do some sort of automated diagram chasing, or just have that as an option when you "Right-click A > Take pre-image of x:B".
So there is no rule, ultimately coded in the too/language itself, that specifies what to do when we take elements. That type of thing will get hardcoded because it's so common, and there's a lot of interaction with the scene elements and GUI widgets when you want it done comprehensively. Other things can be encoded in the language itself such as theorems together with their diagrammatic proofs.
The first version will not support polynomial expressions. It should and will support, however, expressions of elements of modules, and know how to manipulate them for at least proving that d^2 = 0 for a given, supposed boundary map d.
So it's not just a diagram tool, it's not CAS, and it's not a full-fledged proof assistant. It's kind of a blend of all of those things, and will also let the user generate nice-looking and human-readable proofs. If the user is already familiar with notations from the standard category theory texts, then they will feel right at home in this new tool. In otherwords, the learning curve for LEAN / Coq is very steep, while Abstract Spacecraft's learning curve can potentially be a day or two.
1/1