Can't you kind of think of them as a genetic algorithm that has a very good hypothesis generator? Humans could, in principle, help guide that (already very impressive) hypothesis generator to make better guesses to find the proof more easily.