I don't think we'd currently have any way of producing such a thing, because the two processes we have are 1. producing proofs suitable to human mental processe

I don't think we'd currently have any way of producing such a thing, because the two processes we have are 1. producing proofs suitable to human mental processess and 2. producing long and tedious proofs by a series of steps programmed by humans in the first place. Although it also depends to some extent on your definition of "suitable to human mental processes"... for instance, the famous proof that produced Graham's number is not "unsuitable to human mental processes" in the meta sense, but if you try to directly apprehend Graham's number with human mental processes, you fail. You can comprehend it and manipulate it mathematically, but you can not apprehend it.