You want proof? I'll show you proof!

Mathematical proofs have a special place in the spectrum of human knowledge. In no other field are the claims so certain, the conclusions so universally accepted as correct. Why is this? What is the secret behind mathematical proofs that accounts for their incredible success?

Intuition and Objectivity

There are two traits which characterize a good mathematical proof of a claim. First, it should provide an explanation that will help the reader understand on an intuitive level why the given claim is true. Second, it must be objective. The veracity and correctness of the proof should not depend on subjective opinion of anyone.

But these two claims are sometimes not mutually compatible. What if two people have a different intuitive impression of the same claim? One intuitively believes it is true, another believes it is false? How can we referee such a situation to maintain the objective nature of our mathematical results? How can we achieve objectivity in our proofs?

One solution is to take intuition and subjectivity out of the picture completely by devising a completely algorithmic mechanism for determining if our proof is correct. If a machine, an electromechanical device with presumably no intuition whatsoever can verify that our proof is correct, then we can be confident that no personal subjective bias or intuition is required. Proofs of this sort, which can be verified algorithmically by a computer (in theory) in a finite amount of time are often referred to as formal proofs.

One drawback to formal proofs is that they can be quite lengthy and detailed and tedious, sometimes obscuring the intuitive understanding we wish to achieve with our proofs. Most of the mathematical proofs found in math textbooks and journals are not formal proofs. Instead an experienced mathematician tries to convey to his audience two things: (1) a lucid intuitive explanation of why the claim being proved must be valid and (b) enough details about the key steps in a formal proof of the claim that his audience could, if needed, produce a formal proof of the statement. Thus, a typical mathematician uses many shortcuts and convenience conventions to convey to give his proofs the brevity and clarity needed for intuitive understanding of the proof, while providing sufficient information to reconstruct a formal proof of the same claim, thus effectively providing the objective certainty we also demand.

In this introduction to mathematical proofs, we will first introduce you to formal proofs, and then later add shortcuts and convenient conventions that allow you to slowly make the transition from formal proofs to the standard kinds of mathematical proofs found in books and journals. In this way you will first gain a solid, rigorous, objective method of constructing proofs, and later relax the formality to obtain more intuitive informal mathematical proofs. Having a bridge between these two types of proofs, by having a formal proof skeleton and a repertoire of rigorous, well-defined shortcuts for making them more human readable and intuitive, will allow the best of both worlds in our proofs: intuitive understanding and objective certainty.

Toy Proofs!

As you might expect, formal mathematical proofs can be somewhat complicated beasties. Thus, we begin by introducing smaller "Toy" proof systems that illustrate some of the basic features of a real formal proof system, but do it in small incremental steps that illustrate the common mechanisms involved.

In some sense making a formal proof is like playing a game. The kinds of games we have in mind have the following features in common.

Each of these aspects are illustrated in the games that follow.

Let's Play!

In this collection there are currently three games: Scrambler!, TrixGame, and Circle-Dot. You can read the help file for each game before you begin if you wish, but they are fairly self-explanatory if you want to dive right in and try them. Each illustrates the concept of a formal proof in a way that is simpler than what you will encounter when you do actual formal mathematical proofs. There is also some sophisticated mathematics hidden behind the first two games. Beware - all three games can be quite addictive!