I had written what now seems to me to be an unnecessarily long response to this, but along the way I think I thought of an example to demonstrate my point: Shi

I had written what now seems to me to be an unnecessarily long response to this, but along the way I think I thought of an example to demonstrate my point: Shinichi Mochizuki spent several years compiling a large body of work which he calls "Inter-Universal Teichmuller Theory" which which implies a number of important results in number theory, algebraic geometry, and other areas (if I understand the gist of it). However, he has run into a wall in the mathematical community in that almost no one wants to spend the time to try to understand what he wrote (I believe he said he believes it would take someone well-versed in the field around 6 months of study to get a grasp of it). If a human could produce enough work in sufficiently dense terms that other mathematicians don't want to touch it, I can imagine a computer could generate exponentially more work in a much less human-readable format than Mochizuki (albeit formally correct).