I didn't say they have no value. Just limited value. A novel readable proof that expands the horizons of human insight is certainly more valuable than a megabyte sized trychnobezoar of machine generated predicates.
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).
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).