Let's start with Boolean algebra and throw in same basic set theory. Surely that is not too hard to handle for someone able to program. Indeed it is not hard to

Let's start with Boolean algebra and throw in same basic set theory. Surely that is not too hard to handle for someone able to program. Indeed it is not hard to imagine that our programmer could write some program that can systematically spit out Boolean formulas of set relationships that are tautologies, a.k.a. math theorems. In theory her program could conceivably produce all possible theorems. The problem is that only vanishingly small portion of the produced theorems are of any interest to another person. So the hardest part is actually to know/find what is interesting and relevant.