But we have pretty good understanding of the logical foundations and the truth of computer generated math. So having a big library which humans could never produce or fully understand has still a value on its own. It is just another level of abstraction.