Is a brute force method considered a proof?

Question

Say we have some finite set, and some theory about a set, say "All elements of the finite set $X$ satisfy condition $Y$".

If we let a computer check every single member of $X$ and conclude that the condition $Y$ holds for all of them, can we call this a proof? Or is it possibly something else?

Answer 1

Yes, you can. This method is known as proof by exhaustion.

Also, see computer-assisted proof.

Edit: As others have noted, this of course works only for finite sets.

Answer 2

Yes, but some mathematicians think of it as an inferior way of proving things. They think that it's not "pure" and it doesn't really explain(on a deeper level) about what's going on.

One of the most famous computer-assisted proofs is the proof for the four color theorem.

EDIT:

Also note that this technique does not work for infinite sets(I personally think this is one of the biggest reasons why some prefer a more traditional proof). There are conjectures in number theory that are true for a huge huge huge chunk of numbers but are ultimately false.

Answer 3

The more general question is, when is anything a proof.? There are a least two answers, but the one I think is relevant here is that something is a proof if it is a persuasive argument that someone skilled in the art will find convincing. In this sense, your finite enumeration is a proof, if:

1. There is a persuasive argument that your enumeration of the cases is in fact exhaustive
2. The argument for each case is persuasive

There was a lot of controversy in the 1980s about the Haken-Appel proof of the four-color map theorem, which states that that every map in the plane can be colored with only four colors so that no adjoining regions are the same color. Haken and Appel had an argument that showed that every map could be reduced to one of a few thousand cases, an argument that showed that if a case satisfied certain conditions then the corresponding maps could be four-colored, a computer enumeration of the several thousand cases, and a computer-generated demonstration that each case had the desired property.

The arguments were checked and now everyone agrees that this was a proof. But for a while it wasn't clear.

Answer 4

Using a computer to brute-force can be the first step to a proof. The next step is to prove that the program is correct!

A few ways you might do this are:

1. Have the program output a proof for each member of the set. We can then check these proofs without having to trust the program at all. We could even send them all through an automated proof checker, which of course would also need to be proven correct! This may be worth doing, since proof checkers are generally simpler (easier to prove correct) and more general than proof finders; you might output proofs in a format understood by an existing proof checker.
2. Prove that the program is correct for each member of the set. This might defeat the point of using a program in the first place!
3. Prove that the program is correct for all possible inputs. This can be a good strategy, since the program only needs to simplify the problem, it doesn't need to solve it. For example, we might prove that our program returns "TRUE" if our property holds and "FALSE" if it doesn't; we specifically don't have to prove the more difficult part about which one it will actually return. To do that, we just run it.

Answer 5

Exhaustive checking is certainly a valid method proof, that is, everyone agrees that it is a proof.

It is usually considered a not very satisfying proof, though, because it usually fails to produce any insight why such-and-such is true. It just observes that it is true, but mathematicians are generally interested in understanding rather than mere facts, and that is something you don't get from an exhaustive search.

In contrast an "elegant" proof will generally tell you not only that such-and-such is true but will also give you an understanding why it has to be true.