Barry Mazur suggests keeping track of existing theory when making conjectures: to only make conjectures that are not implied by existing theory. This is what we currently do with respect to the program’s own conjectured theory, but we haven’t currently been keeping track of what has actually been known and proved. If we did this then the program’s conjectures would really be (in Fajtlowicz’s terms) “informative”.

Adding this functionality is of no technical difficulty. For the generation of conjectures that would improve the lower bound theory of the independence number of a graph, for instance, it means reading the literature and finding the existing lower bounds for independence number and only adding a conjectured bound if there was at least one graph where the bound was better than all other previously conjectured bounds AND better than all other published bounds.

At this point we are testing and experimenting with how the program works – but if you intend to make a novel contribution to the literature, Mazur’s approach seems necessary.