25
$\begingroup$

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?

$\endgroup$
15
  • 49
    $\begingroup$ Yes.​​​​​​​​​​​ $\endgroup$
    – user2345215
    Mar 18, 2014 at 23:33
  • 19
    $\begingroup$ @MitchKnight Most all mathematicians prefer elegant proofs to brute-force proofs (no matter the source). This preference has nothing to do with age. $\endgroup$
    – Bill Dubuque
    Mar 18, 2014 at 23:46
  • 5
    $\begingroup$ @camel: Human brains are certainly not failproof either. Computer proofs are verified exactly the same way any proof is: by having enough eyes on it until it is "pretty certain" to be right. Mathematical proofs have gone decades with flaws in them, only to be found later. It doesn't invalidate the endeavor of mathematics. $\endgroup$
    – ex0du5
    Mar 19, 2014 at 0:35
  • 8
    $\begingroup$ The four color theorem was proved in that way (en.wikipedia.org/wiki/Four_color_theorem) $\endgroup$
    – Quimey
    Mar 19, 2014 at 3:42
  • 8
    $\begingroup$ @camel brute force proofs, in general, are frowned upon not just because the chance of errors is much greater (which is one reason), but also because it tends to imply that there is no fundamental mathematical "reason" why the proof works, it "just so happens to work" for every possible case. IOW, there is a vague notion that a brute force proof is "a valid proof of a now provably-boring statement". $\endgroup$
    – KutuluMike
    Mar 19, 2014 at 16:45

5 Answers 5

Reset to default
43
$\begingroup$

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.

$\endgroup$
5
  • 9
    $\begingroup$ To nitpick, it does work for infinite sets (brute forcing, not proof by exhaustion) if you only n0eed to prove existence. $\endgroup$
    – TC1
    Mar 19, 2014 at 11:23
  • 2
    $\begingroup$ @TC1 True, but I was really thinking more of what the asker was talking about. $\endgroup$
    – foobar1209
    Mar 19, 2014 at 16:36
  • 4
    $\begingroup$ @TC1 note that proving existence is recognizable, but not decidable using brute force. (That is, if it's true, you will eventually find it, but if it's false it will run forever, and at no point can you determine "it definitely doesn't exist" as it may find it on the next iteration) math.stackexchange.com/questions/25802/… $\endgroup$
    – Cruncher
    Mar 19, 2014 at 17:12
  • 2
    $\begingroup$ @Cruncher Of course, that's why I said "brute forcing, not proof by exhaustion". Obviously you can't exhaust an infinite set. :) $\endgroup$
    – TC1
    Mar 19, 2014 at 17:17
  • 6
    $\begingroup$ @TC1 Chuck Norris can :D $\endgroup$
    – Spook
    Mar 20, 2014 at 7:33
16
$\begingroup$

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.

$\endgroup$
9
$\begingroup$

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.

$\endgroup$
2
  • 4
    $\begingroup$ Funny that you say "more direct". I'd say exhaustion is the most direct way possible, though it's certainly not always the most efficient / concise / elegant way. $\endgroup$
    – leftaroundabout
    Mar 19, 2014 at 1:53
  • $\begingroup$ @leftaroundabout You're certainly right. I'll change the wording a bit. $\endgroup$
    – user135562
    Mar 19, 2014 at 3:26
6
$\begingroup$

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.
$\endgroup$
6
  • 5
    $\begingroup$ What a spoil-sport! Prove the program correct. Then, prove the compiler correct. Then prove the design of the CPU correct. And so on... $\endgroup$
    – GEdgar
    Mar 19, 2014 at 12:40
  • $\begingroup$ Then prove the proof is correct. $\endgroup$
    – Lazar Ljubenović
    Mar 19, 2014 at 17:25
  • $\begingroup$ @GEdgar So of course this is going to rest on some assumptions. Hell, there's no guarantee that the transistors work... These happen to be assumptions that we base on every day. If we run the same code, on many platforms, using many compilers and/or interpreters, different processors and architectures and produce the same result every time... I'd say we're looking pretty good. $\endgroup$
    – Cruncher
    Mar 19, 2014 at 17:27
  • 1
    $\begingroup$ @GEdgar FYI, the compiler step can be skipped, and that's probably the most likely place for this to fail. $\endgroup$
    – Cruncher
    Mar 19, 2014 at 17:28
  • $\begingroup$ We have a huge amount of empirical data for the behaviour of compilers, CPUs and transistors; they're not perfect, but many of their bugs are known and can be avoided. We have exactly no data about the brand-new program I just wrote to help with a proof, so we have no reason to trust it. In fact, all of the empirical data from software engineering says that it will be buggy, hence we have specific reason not to trust it! $\endgroup$
    – Warbo
    Mar 20, 2014 at 10:02
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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