# Using an automatic tool for checking geometric conjectures

I do a lot of research about squares, and I thought of using some automatic tool for proving / disproving some geometric conjectures.

As a simple example, consider the following Square coloring question:

There are 3 red squares and 3 blue squares.
All squares are axis-parallel.
All squares of the same color are interior-disjoint.
CONJECTURE: There always exists a red square and a blue square
that are interior-disjoint.


Altough Abel already proved that the conjecture is true, I wanted to check if this can be proved automatically.

For this experiment I used Minion - a state-of-the-art solver for constraint-satisfaction problems. I started with a simpler problem, where there are only 2 red squares and 3 blue squares. I asked Minion to find a counter-example to the conjecture, i.e., find an arrangement of squares such that every square intersects all squares of the other color. Here is an abbreviated version of my Minion program:

**VARIABLES**
// There are 2 red squares and 3 blue squares.
// for every square, x and y are the south-west corner, and s is the side-length:
DISCRETE xred[2] {1..10}
DISCRETE yred[2] {1..10}
DISCRETE sred[2] {1..10}

DISCRETE xblu[3] {1..10}
DISCRETE yblu[3] {1..10}
DISCRETE sblu[3] {1..10}

**CONSTRAINTS**
//(Here I defined the macros "disjoint" and "intersect"; details skipped)

// Squares of the same color must be disjoint:
disjoint(red[0],red[1])
disjoint(blu[0],blu[1])
disjoint(blu[0],blu[2])
disjoint(blu[2],blu[1])

// Squares of the different colors must intersect:
intersect(red[0],blu[0])
intersect(red[0],blu[1])
intersect(red[0],blu[2])
intersect(red[1],blu[0])
intersect(red[1],blu[1])
intersect(red[1],blu[2])


I ran Minion and it returned in no time with the following nice counter-example:

Then I added a third red square to the program, with the relevant constraints, and ran Minion again. After 7 hours it returned saying that - as we already know - there is no solution, i.e., no counter-example.

Is this answer a sufficient proof that the conjecture is true? Probably not:

• First, the CSP solver checked x, y and s that are integers from 1 to 10, but there are infinitely many other values.
• Additionally, there is no formal proof that the CSP solver itself is correct. There may be a bug that prevents it from finding an existing counter-example.

So my question is: Is there a way to use an automatic program in order to prove the above conjecture (and similar such conjectures)? Is this realistic to expect a state-of-the-art automatic prover to prove such a conjecture? If so, what is the right tool for that task?

-