In addition to my comment that the thread is too "discussion-y" (meaning too opinion or speculation driven), my feeling about this question is that there is probably no one in our community who can render an expert opinion on the matter based on demonstrable facts. It's all just speculation and "this is what I guess" about the matter, or even sentiments along the lines of "we shouldn't worry though, math will always be fun". And it could hardly be otherwise based on what little anybody really knows about human brains and AI (which I believe is beyond the scope of MathOverflow).
I think the problem is on how the question is put: "are there any fundamental reasons why a machine learning algorithm trained on a large database of formal proofs couldn't reach a level of skill that is comparable to humans?" I think that question is shooting much too high: no one can really say!! But if the question were to be reworded so as to emphasize more what actually has been accomplished and what is currently in the offing, on a concrete level, that would allow for more influx of expertise. So what is wrong with the question now is too much gazing into the future.
(My own opinion on the subject, for what little it may be worth, is that the role of human vision and even our kinesthetic sense in creating mathematics has hardly been touched on. There are huge swaths of geometry and low-dimensional topology, for example, that are just immensely difficult to cast into fully formal language, partly because the brain modules involved (the famous left/right brain dichotomy) are very different. I would aver that human vision endows human brains with a decisive advantage in certain respects for creating and communicating mathematics as we normally do it, at least for the foreseeable future, although I don't aver that this situation will never change. I'm actually hoping it does.)