There are theorems like that now, like de Grey's lower bound for the Hadwiger-Nelson (unit distance graph) problem. He used a SAT solver to check that a certain graph with 1581(?) vertices is not 4-colorable. There's no way for a human to check that.

Even simpler, imagine Anthropic announces Goldbach's conjecture is false and they have a billion digit counterexample. Anyone can download it (300MB compressed), but how do you check it?

Doron Zeilberger for decades has expected incomprehensible computer proofs to eventually take over mathematics.