So this looks like a useful use case for a mcp pipeline. You have a set of agents that are designed to look through the mathematics to discover what is useful, you then pipeline over to a set of agents that are distinguished by having training data on sets of mathematical fields, you have cross check proof agents, and then you have connections between fields agents. You see if you can use connections across mathematics through Wikipedia to crawl through the math and see if there's a correspondence between citations or links between proofs and their mathematical interdependence. Then you can start building trees and see if you can make righter linkages between set theory and number theory or topology or something.then see if you can get closer to a total theory or universal theory of mathematics (or prove it doesn't exist). If you can do that by just throwing money at it why not? It might be able to come up with all sorts of applications in the real world just byd default.