Even people can't always produce human friendly proofs. There's Shinichi Mochizuki who might have proven the ABC conjecture but no one can confirm it because he created a whole method and set of techniques/theories that no one else really gets. This is a person creating a branch so dense that it's taken 3 years and we still haven't determined if it's wrong.

There's also the controversial Computer Assisted Proof. Which I think is a lesser version of completely computer generated proofs where there's the question of procedural errors and the difficulty of checking for them.

https://en.wikipedia.org/wiki/Computer-assisted_proof