I'd really love to see someone like Deepmind get a hold of this. They are perfectly placed to apply a lot of resources to it and it's right in their wheelhouse.
> We outline a program in the area of formalization of mathematics to automate theorem proving in algebra and algebraic geometry. We propose a construction of a dictionary between automated theorem provers and (La)TeX exploiting syntactic parsers. We describe its application to a repository of human-written facts and definitions in algebraic geometry (The Stacks Project). We use deep learning techniques.
https://arxiv.org/abs/1907.07794
https://arxiv.org/pdf/1904.03241.pdf