i believe i've read about automatically --(i believe automatically, and it's a crucial distinction, but i'm not looking it up right now, so take it with a grain

i believe i've read about automatically --(i believe automatically, and it's a crucial distinction, but i'm not looking it up right now, so take it with a grain of salt)-- generated proofs so long they can't be reasonably understood by a human, but it "convinces" a computer. such a proof isn't a proof in the sense that it doesn't convince a human being, which is the point of the proof. but, since it checks out, maybe a better way to think of it is it's a mathematical proof but for an audience other than human beings. i wonder if a game is much different from a proof. i mean, we can implement games as programs, so there is a connection at that level.