Mathematics for Computer Science (Lehman, Leighton, and Meyer)

In a book he was reading around 1630, Fermat claimed to have a proof for this proposition, but not enough space in the margin to write it down. Over the years, the Theorem was proved to hold for all up to 4,000,000, but we’ve seen that this shouldn’t necessarily inspire confidence that it holds for all . There is, after all, a clear resemblance between Fermat’s Last Theorem and Euler’s false Conjecture. Finally, in 1994, British mathematician Andrew Wiles gave a proof, after seven years of working in secrecy and isolation in his attic. His proof did not fit in any margin.

Finally, let’s mention another simply stated proposition whose truth remains unknown.

Proposition 1.1.8 (Goldbach’s Conjecture). Every even integer greater than 2 is the sum of two primes. Goldbach’s Conjecture dates back to 1742. It is known to hold for all numbers up to but to this day, no one knows whether it’s true or false.

For a computer scientist, some of the most important things to prove are the correctness of programs and systems— whether a program or system does what it’s supposed to. Programs are notoriously buggy, and there’s a growing community of researchers and practitioners trying to find ways to prove program correctness. These efforts have been successful enough in the case of CPU chips that they are now routinely used by leading chip manufacturers to prove chip correctness and avoid mistakes like the notorious Intel division bug in the 1990’s. Developing mathematical methods to verify programs and systems remains an active research area. We’ll illustrate some of these methods in Chapter 5.

The symbol ::= means “equal by definition.” It’s always ok simply to write “=” instead of ::=, but reminding the reader that an equality holds by definition can be helpful. Two regions are adjacent only when they share a boundary segment of positive length. They are not considered to be adjacent if their boundaries meet only at a few points.

A predicate can be understood as a proposition whose truth depends on the value of one or more variables. So “ is a perfect square” describes a predicate, since you can’t say if it’s true or false until you know what the value of the variable happens to be. Once you know, for example, that equals 4, the predicate becomes the true proposition “4 is a perfect square”. Remember, nothing says that the proposition has to be true: if the value of were 5, you would get the false proposition “5 is a perfect square.” Like other propositions, predicates are often named with a letter. Furthermore, a function-like notation is used to denote a predicate supplied with specific variable values.