I've been considering something like this for a while. It only makes sense as a free, open-source, decentralized sharing protocol (where anyone can host theorems and no one can limit sharing them).

If a company were to manage to commercialize this, it would end public open research.

I suspect tools like this will change human behaviour in the future so that no one really understands the math any more. If a solution to the Riemann hypothesis is found with it, I wouldn't be surprised if the person finding it didn't even understand analytic continuation. And that those that do just click like and scroll to the next problem.