Crossposting note: This is a crosspost from a question I first asked in MathOverflow.
———————————————————————————————————————————
Perhaps one of the biggest issues when carrying out research in category theory is managing large amounts of data, e.g.:
Recently I've been thinking more and more about how we might be able to employ computer-assisted tools in facilitating this process, and that perhaps we may only be able to carry out certain programs with the assistance of such tools.
A concrete example might be Johnson–Gurski–Osorno's program, aiming to find categorical models for low-dimensional truncations of the sphere spectrum. For instance, in the $n=2$ case, described here, we can directly see how $\pi_{1}(\mathbb{S})=\mathbb{Z}_{/2}$ and $\pi_{2}(\mathbb{S})=\mathbb{Z}_{/2}$ arise from considering homotopy-coherent invertibility. I've always been amazed by the fact that invertibility + homotopy coherence can recover a structure as complicated as the sphere spectrum, and seeing how this goes for $n=3$ — where the wonders of $\pi_{3}(\mathbb{S})=\mathbb{Z}_{/24}$ lie — would be beyond incredible. However, the $n=2$ case already takes place at the setting of symmetric monoidal bicategories, so the average diagram looks more or less like this:
Considering that the move from $n=2$ to $n=3$ represents an increase of complexity just as big as the move from $n=1$ (i.e. the usual friendly monoidal categories) to $n=2$, one might wonder whether carrying out this program to $n=3$ would be feasible at all — at least without the use of computer tools, that is.
At its core, the problem is conceptually simple: for instance, one could view the proof that “precomposing a dinatural transformation by a natural transformation gives a dinatural transformation again” as a special case of string rewriting with 3 rewriting steps:
One could imagine a naive implementation of such a tool as follows:
- First, one specifies a number of rewriting rules such as “naturality”, “associativity”, “preservation of composition for functors”, etc.
- Second, the program accepts two strings of morphisms, which we aim to prove are equal.
- Then, the program tries to rewrite one string into another using the valid rewriting rules it has at hand (either purely symbolically or neuro-symbolically via deep learning).
Question. What efforts have there been trying to pursue something like this? In particular, have there been attempts hoping to augment symbolic methods (e.g. some Lean tactics) with deep learning¹?
¹I specifically mention deep learning because I think it might help at solving the resulting combinatorial explosion that happens as one starts to consider more and more involved diagram and proof steps.
