Do not nerd snipe me! There's tons of juice left on the CPU side. Again I recommend Metamath Zero (which is somewhat of an opposite direction as HoTT), as it's

Do not nerd snipe me! There's tons of juice left on the CPU side. Again I recommend Metamath Zero (which is somewhat of an opposite direction as HoTT), as it's able to check the entire Metamath proof database in a few hundred milliseconds. This is orders of magnitude faster than most other proof systems. If you did want to manipulate trees on the GPU, then my stack monoid work[1] might be a good basis for it. Of course, a whole nother direction is to use AI to develop proofs, which is a fascinating and growing area (see Holophrasm[2] and DeepMind work[3]). That of course runs on the GPU. [1]: https://arxiv.org/abs/2205.11659 https://arxiv.org/abs/2205.11659 [2]: https://arxiv.org/abs/1608.02644 https://arxiv.org/abs/1608.02644 [3]: https://www.deepmind.com/publications/proving-theorems-using-incremental-learning-and-hindsight-experience-replay https://www.deepmind.com/publications/proving-theorems-using...