Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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:

// 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}

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

// Squares of the same color must be disjoint:

// Squares of the different colors must intersect:

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

enter image description here

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?

share|improve this question
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.