We have made good use of Grinvin in the classroom, not only in graph theory classes, but also in general mathematics courses for younger people. We use Grinvin to give students a first hand experience on what consititutes a valid mathematical proof and how a mathematician comes up with proofs for new problems.

We do this by playing the following ‘game’:

• The teacher chooses a few (simple) invariants (say number of vertices, number of edges, minimal degree …) up front.
• The teacher also choose a small graph (say, a triangle) which is handed to Grinvin to set off the whole process.
• Grinvin is asked to compute the values of the selected invariants for the given graph and to make a conjecture about them - say:

The number of edges of a graph is always less than the minimal degree multiplied by the number of vertices

Note that a conjecture generated by Grinvin will always be true for the graphs it has investigated to obtain that conjecture. Indeed, a triangle has 3 edges, and 3 is indeed less than 2 (the minimal degree of a vertex in a triangle) multiplied by 3 (the number of vertices).

Of course, this is only a conjecture and it need not hold for all graphs. The first task for the students is therefore to try to find a counterexample for this conjecture - which is not so hard - or better still, the smallest possible counterexample.

In this case ‘smallest’ means: with the minimal number of vertices and in case of equality, also the minimal number of edges. However, Grinvin does not enforce this. The rules of the game are set by the teacher, and it may be interesting to change them once in a while. Another rule which we often use (and which again is not enforced by Grinvin) is to require that all graphs are connected.

With these assumptions, the smallest (connected) counterexample is a graph on four vertices with four edges and minimum degree one (a triangle with an additional edge through one of its vertices). It is however not sufficient that the students find this counterexample, they must also prove that it is the smallest possible.

The ‘game’ now continues as follows:

• We add the new counterexample graph to the list of graphs for Grinvin to consider
• We ask Grinvin for a new conjecture based on the new information we have provided
• Again we try to find a counterexample to this new conjecture and hand it (i.e., the smallest of them) to Grinvin so it can improve its conjectures, and the process repeats as before

At some point the students will no longer be able to find a counterexample, suggesting that Grinvins conjecture might actually be true, i.e., a theorem. At this point it becomes the task of the students to actually prove the conjecture. If they succeed, the game is over.