Craig Larson, Department of Mathematics and Applied Mathematics, Virginia Commonwealth UniversityDepartment

Automated Conjecturing for Proof Discovery
CONJECTURING is an open-source Sage program which can be used to make invariant-relation or property-relation conjectures for any mathematical object-type. The user must provide at least a few object examples, together with functions defining invariants and properties for that object-type. These invariants and properties will then appear in the conjectures. Here we demonstrate how the CONJECTURING program can be used to produce proof sketches in graph theory. In particular, we are interested in graphs where the independence number of the graph equals its residue. Residue is a very good lower bound for the independence number - and the question of characterizing the class of graphs where these invariants are equal has been of continuing interest. The CONJECTURING program can be used to generate both necessary and sufficient condition conjectures for graphs where the independence number equals its residue, and proof sketches of these conjectures can also be generated. We will discuss the program and give examples. This is joint work with Nico Van Cleemput (Ghent University).