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

[2]: https://arxiv.org/abs/1608.02644

[3]: https://www.deepmind.com/publications/proving-theorems-using...