ACMES Talk on Generating Proof Sketches

Today is the last day of ACMES 2: “Computationally Assisted Mathematical Discovery
and Experimental Mathematics”, a conference at Western Ontario University, in London, Ontario, Canada. Neal Sloane, Jon Borwein, David Bailey, Yuri Matiiyasevich, were among the many who gave interesting (even exciting) talks.

I gave a talk on using the CONJECTURING program to generate sketches of proofs of theorems. Here are the slides. The talk generated some interest. I got lots of questions, and positive response.

Automated Conjecturing I

Our first paper in a projected series of papers on using automated conjecturing as a foundation for designing machines with intelligent behaviors just appeared in the journal Artificial Intelligence.

Here is the abstract:

We discuss a new implementation of, and new experiments with, Fajtlowicz’s Dalmatian conjecture-making heuristic. Our program makes conjectures about relations of real number invariants of mathematical objects. Conjectures in matrix theory, number theory, and graph theory are reported, together with an experiment in using conjectures to automate game play. The program can be used in a way that, by design, advances mathematical research. These experiments suggest that automated conjecture-making can be a useful ability in the design of machines that can perform a variety of tasks that require intelligence.

New Conjecturing Talk

There has been a lot of news about our program, and experiments with the program. I just gave a talk at Computers in Scientific Discovery 7 (CSD 7) that has several examples. Here are the slides.

The slides include conjectures for the independence number of a graph, the domination number, linear programs, matrices, graph properties, Chomp, and much much more.

Graph Brain

Patrick Gaskill called the code for the conjecturing module of our Independence Number Project Graph Brain. Nico and I have one growing file (gt.py) with all the graph invariants, graph properties and graph objects used for making graph conjectures, which can be found on Github. We would ideally like to include all published graph invariants, graph properties and graph objects in this file. Graph Brain seems like a great name to repurpose for this project.

I have an intention in the next year to add lots more graphs, invariants and properties. I’m curious to see what kinds of conjectures we get as we add more and more knowledge to the program. It would be even better if students and others contributed even more graphs, invariants and properties – to have a community effort, at least for graph theory. Of course, this idea could be duplicated for any other object type. Getting a critical mass of ingredients may be the secret to getting the most useful conjectures.

I gave a talk on the program at Johns Hopkins University today and got lots of great questions, comments and suggestions. Tamas Budavari suggested or gave me the idea of having a web page or public interface to make it easy for others to add new graphs, invariants and properties. Wow, that would be great. There are so many interesting things to do!

Graphs where the Independence Number equals its Residue

The residue of a graph is the number of zeros that remain after repeated application of the Havel-Hakimi process to the degree sequence of a graph. This invariant can be computed efficiently (it is clearly no worse than O(n^2)). The residue is often the best performing of the known lower bounds for the independence number (alpha) of a graph. Its not great – but the lower bound theory is relatively poor compared to the upper bound theory (and Lovasz’s amazing theta function).

Characterizing graphs where alpha = residue is a theoretical challenge and of practical utility. A recognition algorithm for graphs in this class would expand the class of graphs where the independence number can be computed efficiently. These include, for instance, odd cycles \$C_{2n+1}\$ and the complete bipartite graphs \$K_{n,n}\$.

We are testing the new property-relations version of the program. So we generated some necessary and sufficient conditions for a graph to have this property. First some necessary conditions for graphs where residue = alpha. If a graph is 2-connected and the degree sum of any pair of non-adjacent vertices is at least n, it “is ore” (this is a sufficient condition for a graph to be hamiltonian). “is circular planar”” means outerplanar. “weakly chordal” means no induced cycle of length >= 5.
1.  (has_residue_equals_alpha)->((is_regular)->(is_ore))
2. (has_residue_equals_alpha)->((is_bipartite)->(is_circular_planar))
3. (has_residue_equals_alpha)->((is_regular)->(is_odd_hole_free))
4. (has_residue_equals_alpha)->((is_cartesian_product)->(is_regular))
5. (has_residue_equals_alpha)->((is_line_graph)->(is_weakly_chordal))
6. (has_residue_equals_alpha)->((is_perfect)|(is_eulerian))
Now here are some sufficient conditions for graphs where residue = alpha. “generalized dirac” is the condition that the graph is 2-connected and non-adjacent vertices have at least (2n-1)/3 neighbors. It is also a sufficient condition for hamiltonicity.

1. ((has_perfect_matching)&(is_generalized_dirac))->(has_residue_equals_alpha)
2. ((is_line_graph)&(is_circular_planar))->(has_residue_equals_alpha)
3. (is_chordal)->(has_residue_equals_alpha)
4. ((is_even_hole_free)&(is_eulerian))->(has_residue_equals_alpha)

As always counterexamples would be of interest. They will help the program make better conjectures. Proofs would be of interest too!

An Experiment with Property-derived Invariants

We’ve coded a number of graph invariants and properties. One easy way to get more invariants is to use the characteristic functions of the properties we’ve already coded. That is, if P is a property then P_value is an invariant where P_value = 1 if a given object has property P and 0 otherwise.

So, for instance, the following upper bound conjectures for the chromatic number for a graph include invariants like “is_eulerian_value” which is 1 if the graph is eulerian and 0 otherwise. So the Conjecture 7, for instance, “chromatic_num(x) <= card_periphery(x)/is_eulerian_value(x)”, should be interpreted as “if graph G is eulerian then the chromatic number is no more than the cardinality of the periphery (the vertices of maximum eccentricity) and if graph G is not eulerian then the chromatic number is no more than the cardinality of the periphery divided by 0 (which Sage interprets as Infinity and the relation as True)”. Since the second part is trivially true, Sage’s conjecture is really about the special case where the graph is eulerian.

1. chromatic_num(x) <= card_periphery(x) + 1
2. chromatic_num(x) <= average_distance(x)/is_semi_symmetric_value(x). This conjecture should be interpreted: “If a graph is semi-symmetric then the chromatic number is less than average distance”. The program only knows two of these, the Gray graph and the Folkman graph, so this is a very bold conjecture.
3. chromatic_num(x) <= maximum(clique_number(x), min_degree(x) + 1)
4. chromatic_num(x) <= min_degree(x)/is_cartesian_product_value(x)
5. chromatic_num(x) <= matching_number(x)/is_strongly_regular_value(x)
6. chromatic_num(x) <= card_periphery(x)^card_center(x)
7. chromatic_num(x) <= card_periphery(x)/is_eulerian_value(x)
8. chromatic_num(x) <= card_periphery(x)/is_bipartite_value(x)
9. chromatic_num(x) <= -is_cartesian_product_value(x) + wilf(x)
10. chromatic_num(x) <= brooks(x) – is_semi_symmetric_value(x)
11. chromatic_num(x) <= -is_cartesian_product_value(x) + szekeres_wilf(x)
12. chromatic_num(x) <= number_of_triangles(x) + rank(x)
13. chromatic_num(x) <= clique_number(x)/is_bipartite_value(x)
14. chromatic_num(x) <= clique_number(x)^2 + 1
15. chromatic_num(x) <= girth(x)^2/is_overfull_value(x)
16. chromatic_num(x) <= brooks(x) + chi_equals_min_theory_value(x) – 1
17. chromatic_num(x) <= number_of_triangles(x) + residue(x) + 1
18. chromatic_num(x) <= (different_degrees(x) + 1)^clique_number(x)
19. chromatic_num(x) <= has_lovasz_theta_equals_alpha_value(x)+szekeres_wilf(x)-1