[sanxiyn]

Indeed. We now actually have some math results of interest for which we have only formal proofs and no human proofs. https://arxiv.org/abs/1509.05468 is an example.