You are assuming that the latter, once autonomously discovered and verified at scale, could not simply be translated into the former, also perhaps autonomously at scale (or otherwise selectively as determined by human interest, taste, and relevance).
Well we're literally discussing a human readable machine generated proof here yet you don't seem happy with that.