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 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:
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.