There are some huge (not insurmountable) obstacles to this happening. The biggest one, as I see it, is that so many mathematical objects need to be formalised i

There are some huge (not insurmountable) obstacles to this happening. The biggest one, as I see it, is that so many mathematical objects need to be formalised into the system so that a theorem can even be stated, let alone its proof checked. Coming up with useful (and correct) formalisms of these objects, objects that mathematicians use constantly every day, are entire research projects of their own. There are some excellent talks by Kevin Buzzard about this, and where he sees it going in the future from a mathematician’s perspective. We’re getting there but progress is slow, and a large part of why it’s slow is that modern mathematics is fantastically complicated.