Sign up ×
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|cite|improve this question

1 Answer 1

If you are going to bring in the question of bugs, then no: there is no way to use any program to prove any conjecture, ever. Even if it is open source, being able to look at the code doesn't insure it works properly. A bug could be inherent in the programming language even!

If you are willing to trust software, then you need to make some theoretical assurances that what the software tests is equivalent to testing everything. Maybe using some symmetry arguments, you can identify a finite number of cases that every instance will fall into. Then by testing over these, you can be sure of a correct result. This is the case in many searches for combinatorial objects, where each possible candidate (up to isomorphism) is tested to see if it can be extended to the desired object.

share|cite|improve this answer

Your Answer


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

Not the answer you're looking for? Browse other questions tagged or ask your own question.