once it was established that automated proof was not keeping all its promises, mathematicians conceived a less ambitious project, namely that of proof checking. When one uses an automated theorem proving program, one enters a proposition and the program attempts to construct a proof of the proposition. On the other hand, when one uses a proof-checking program, one enters both a proposition and a presumed proof of it and the program merely verifies the proof, checking it for correctness.

Although proof checking seems less ambitious than automated proof, it has been applied to more complex demonstrations and especially to real mathematical proofs. Thus, a large share of the first-year undergraduate mathematics syllabus has been checked by many of these programs. The second stage in this project was initiated in the nineties; it consisted in determining, with the benefit of hindsight, which parts of these proofs could be entrusted to the care of software and which ones required human intervention. The point of view of mathematicians of the nineties differed from that of the pioneers of automated proof: as we can see, the idea of a competition between man and machine had been replaced with that of cooperation.

One may wonder whether it really is useful to check mathematical proofs for correctness. The answer is yes, first, because even the most thorough mathematicians sometimes make little mistakes. For example, a proof-checking program revealed a mistake in one of Newton's demonstrations about how the motion of planets is subjected to the gravitational attraction of the sun. While this mistake is easily corrected and does not challenge Newton's theories in the slightest, it does confirm that mathematical publications often contain errors. More seriously, throughout history, many theorems have been given myriad false proofs: the axiom of parallels, Fermat's last theorem (according to which, if n ≥ 3, there exist no positive integers x, y and z such that xn + yn = zn) and the four-color theorem (of which more in Chapter 12) were all allegedly “solved” by crank amateurs, but also by reputable mathematicians, sometimes even by great ones.

at the beginning of the twentieth century, two theories about computation developed almost simultaneously: the theory of computability and the theory of constructivity. In a perfect world, the schools of thought that produced these theories would have recognized how their work was connected and cooperated in a climate of mutual respect. Sadly, this was not the case, and the theories emerged in confusion and incomprehension. Not until the middle of the century would the links between computability and constructivity finally be understood.

To this day, there are traces of the old strife in the sometimes excessively ideological way in which these theories are expounded, both of which deserve a dispassionate presentation. After our call for unity, we must nevertheless concede that, although both schools of thought developed concepts that turned out to be rather similar, the problems they set out to solve were quite different. Therefore, we will tackle these theories separately. Let's start with the notion of computability.

THE EMERGENCE OF NEW ALGORITHMS

As they each in turn attempted to clarify inference rules, Frege, Russell, and Hilbert contributed to the elaboration of predicate logic. Predicate logic, in keeping with the axiomatic conception of mathematics, consists of inference rules that enable proofs to be built, step by step, from axiom to theorem, without providing any scope for computation. Ignoring Euclid's algorithm, medieval arithmetic algorithms, and calculus, predicate logic signaled the return to the axiomatic vision passed down from the Greeks that turns its back on computation.

In predicate logic, as in the axiomatic conception of mathematics, a problem is formulated as a proposition, and solving the problem amounts to proving that the proposition is true (or that it is false). What is new with predicate logic is that these propositions are no longer expressed in a natural language – say, English – but in a codified language made up of relational predicate symbols, coordinating conjunctions, variables, and quantifiers.

astronomers used to observe the sky with the naked eye until, in the early seventeenth century, Galileo made his first telescope – or, as some historians would have it, simply pointed a spyglass skywards. Similarly, biologists originally observed living organisms with the naked eye until Anton van Leeuwenhoek started using a microscope. Thus, in the history of many sciences, there are two distinct periods, separated by the introduction of the science's first instrument.

Until the seventies, mathematics was practically the only science not to use any instruments. Unlike their lab-coated colleagues, mathematicians only required a blackboard and some chalk to make their science progress. This peculiarity can be explained by the fact that mathematical judgments are analytic: they do not require any interaction with nature and, above all, they require no measurements. Telescopes, microscopes, bubble chambers, and the like are measuring instruments or, to put it differently, instruments that extend the faculties of our senses. Therefore, it seemed natural not to need any of those when practicing mathematics.

In 1976, mathematics entered the instrumented period of its history. The instruments used by mathematicians, namely computers, are no measuring instruments; their function is not to extend the faculties of our senses, but to extend the faculties of our understanding, that is, to prolong our reasoning and computing faculties.

When an instrument is introduced in a science, a change occurs which is more quantitative than qualitative. There are many similarities between observing Jupiter's satellites with a telescope and observing the moon with the naked eye. One could imagine a human being endowed with superior eyesight who would be capable of seeing Jupiter's satellites with the naked eye, just like we are able to see the moon without the aid of instruments. Similarly, whereas the human being can only produce, by hand, demonstrations of some thousand pages, computers push back that limit by producing proofs of several million pages.

whereas the theory of computability placed computation at the heart of several major mathematical issues, the theory of constructivity, which was developed independently, does not appear, at first glance, to assign such an essential role to computation. If you look closer, however, you will find that computation also plays an important part.

CONSTRUCTIVE VERSUS NONCONSTRUCTIVE ARGUMENTS

Let's start with a story. It takes place in Europe, shortly after World War I. The explorer has returned from his many travels and, now clean shaven and well rested, decides to ride the Orient Express from Paris to Constantinople. In his compartment, he finds an intriguing, scented note sent by a secret admirer: the mystery woman asks him to meet her on the platform of the last station the train calls at on French territory. The explorer gets hold of a list of the stations the Orient Express stops at from Paris to Constantinople: Strasbourg, Utopia, Munich, Vienna, Budapest,… He knows that Strasbourg is in France and that Munich is in Germany, but he has no idea where Utopia is. He asks his fellow passengers, he asks the conductor, but Utopia is such a small, obscure station that nobody on board the train is able to help him – it is hard to fathom why the Orient Express would even stop in a town no one seems ever to have heard of! Will the explorer manage to meet his lady? It's not a sure thing. Yet it is not hard to prove that there exists a station at which the Orient Express stops that is in France and is such that the next station is no longer in France. For either Utopia is in France, and then is the train's last stop there, or it is not, in which case Strasbourg is the train's last stop on French soil.

in the early seventies, when word of Martin-Löf's type theory and subsequent research on the subject had not yet reached computer scientists, the idea that a proof is not built solely with axioms and inference rules but also with computation rules developed in computer science – especially in a branch called “automated theorem proving.” Thus, work on type theory and work on automated theorem proving were pursued contemporaneously by two distinct schools that ignored each other – admittedly, an improvement on the behavior of the schools that developed, respectively, the theory of computability and the theory of constructivity, which abused each other. It was not until much later that the links between these projects were finally revealed.

An automated theorem proving program is a computer program that, given a collection of axioms and a proposition, searches for a proof of this proposition using these axioms.

Of course, Church's theorem sets a limit on this project from the outset, because it is impossible for a program to decide whether the proposition that it has been requested to supply with a proof actually has one or not. However, there is nothing to prevent a program from searching for a proof, halting if it finds one, and continuing to look as long as it does not.

THE FANTASY OF “INTELLIGENT MACHINES”

In 1957, during one of the first conferences held about automated theorem proving, the pioneers in the field made some extravagant claims. First, within ten years, computers would be better than humans at constructing proofs and, as a consequence, mathematicians would all be thrown out of work. Second, endowed with the ability to build demonstrations, computers would become “intelligent”: they would soon surpass humans at chess, poetry, foreign languages, you name it. Cheap sci-fi novels began to depict a world in which computers far more intelligent than humans ruthlessly enslaved them. Ten years went by and everyone had to face the facts: neither of these prophecies were even close to being fulfilled.

Key moments in tech history

I can still, and perhaps will always, remember:

• The first day we connected our NES to our TV and Mario appeared

• The first day I instant messaged a friend using MSN Messenger from France to England

• The first day I was doing a presentation and said I could get online without a cable

• The first day I was carrying my laptop between rooms and an email popped up on my computer

• The first day I tentatively spoke into my computer and my friend’s voice came back

• The first day the map on my phone automatically figured out where I was

Each of these moments separately blew my mind on the day. It was like magic when they happened. The closest I have had recently was probably the first successful call using Facetime and waving my hand at a Kinect sensor. (Another, that most people probably haven’t experienced, was watching a glass door instantly turn opaque at the touch of a button. Unbelievable.)

Each of these moments blew me away because things happened that weren’t even part of my expectations. I expect our expectations these days have now risen sufficiently high that it’ll probably take teleportation to get a similar effect from a teenager. Maybe life would be more fun if we kept our expectations low?

Silicon and semiconductors

When we left the early history of computers in Chapter 2, we had seen that logic gates were first implemented using electromechanical relays – as in the Harvard Mark 1 – and then with vacuum tubes – as in the ENIAC and the first commercial computers. These early computers with many thousands of vacuum tubes actually worked much better and more reliably than many engineers had expected. Nevertheless, the hunt was on for a more dependable technology. After World War II, Bell Labs (Fig. 7.1) initiated a research program to develop solid-state devices as a replacement for vacuum tubes. The focus of the program was not on materials that were metals or insulators but on strange, “in-between” materials called semiconductors.

In a solid, it is the flow of electrons that gives rise to electric currents when a voltage is applied. One of the great successes of quantum physics has been in giving us an understanding of the way in which different types of solids – metals, insulators, and semiconductors – conduct electricity. This quantum mechanical understanding of materials has led directly to the present technological revolution, with its accompanying avalanche of stereo systems, color TVs, computers, and mobile phones. A good conductor, such as copper, must have many conduction electrons that are able to move and thus constitute a current when a voltage is applied. By contrast, an insulator such as glass or carbon has very few conduction electrons, and little or no current flows when a voltage is applied. Semiconductors are solids that conduct electricity much better than insulators but much worse than metals. The elements germanium and silicon are two examples. The importance of silicon for computer technology is evident in the naming of California’s “Silicon Valley,” home to many of the earliest electronic component manufacturers (Fig. 7.2).

Going through the layers

In the last chapter, we saw that it was possible to logically separate the design of the actual computer hardware – the electromagnetic relays, vacuum tubes, or transistors – from the software – the instructions that are executed by the hardware. Because of this key abstraction, we can either go down into the hardware layers and see how the basic arithmetic and logical operations are carried out by the hardware, or go up into the software levels and focus on how we tell the computer to perform complex tasks. Computer architect Danny Hillis says:

We will also see the importance of “functional abstraction”:

In this chapter, like Strata Smith going down the mines, we’ll travel downward through the hardware layers (Fig. 2.1) and see these principles in action.

Ideas of probability: The frequentists and the Bayesians

We are all familiar with the idea that a fair coin has an equal chance of coming down as heads or tails when tossed. Mathematicians say that the coin has a probability of 0.5 to be heads and 0.5 to be tails. Because heads or tails are the only possible outcomes, the probability for either heads or tails must add up to one. A coin toss is an example of physical probability, probability that occurs in a physical process, such as rolling a pair of dice or the decay of a radioactive atom. Physical probability means that in such systems, any given event, such as the dice landing on snake eyes, tends to occur at a persistent rate or relative frequency in a long run of trials. We are also familiar with the idea of probabilities as a result of repeated experiments or measurements. When we make repeated measurements of some quantity, we do not get the same answer each time because there may be small random errors for each measurement. Given a set of measurements, classical or frequentist statisticians have developed a powerful collection of statistical tools to estimate the most probable value of the variable and to give an indication of its likely error.

The next revolution

The first age of computing was concerned with using computers for simulation. As we have seen, the first computers were built to do complex calculations. The initial motivation for building the ENIAC was to calculate artillery tables showing the angles at which guns should be fired based on the distance to the target and other conditions. After World War II, scientists used the ENIAC to explore possible designs for a hydrogen bomb. More generally, computers were used to simulate complex systems defined in terms of a mathematical model that captured the essential characteristics of the system under study. During the first thirty years of computing, from about 1950 until the early 1980s, researchers increasingly used computers for simulations of all sorts of complex systems. Computer simulations have transformed our lives, from designing cars and planes to making weather forecasts and financial models. At the same time, businesses used computers for performing the many, relatively simple calculations needed to manage inventories, payroll systems, and bank transactions. Even these very early computers could perform numerical calculations much, much faster than humans.

WARNING: This chapter is more mathematical in character than the rest of the book. It may therefore be hard going for some readers, and they are strongly advised either to skip or skim through this chapter and proceed to the next chapter. This chapter describes the theoretical basis for much of formal computer science.

Hilbert’s challenge

Are there limits to what we can, in principle, compute? If we build a big enough computer, surely it can compute anything we want it to? Or are there some questions that computers can never answer, no matter how big and powerful a computer we build. These fundamental questions for computer science were being addressed long before computers were built!

In the early part of the twentieth century, mathematicians were struggling to come to terms with many new concepts including the theory of infinite numbers and the puzzling paradoxes of set theory. The great German mathematician David Hilbert (B.6.1) had put forward this challenge to the mathematics community: put mathematics on a consistent logical foundation. It is now diffi cult to imagine, but in the early twentieth century, mathematics was in as great a turmoil as physics was at that time. In physics, the new theories of relativity and quantum mechanics were overturning all our classical assumptions about nature. What was happening in mathematics that could be comparable to these revolutions in physics?

The hypertext visionaries

Vannevar Bush (B.11.1), creator of the “Differential Analyzer” machine, wrote the very influential paper “As We May Think” in 1945, reflecting on the wartime explosion of scientific information and the increasing specialization of science into subdisciplines:

Bush concluded that methods for scholarly communication had become “totally inadequate for their purpose.” He argued for the need to extend the powers of the mind, rather than just the powers of the body, and to provide some automated support to navigate the expanding world of information and to manage this information overload.