Quando orientur controversiae, non magis disputatione opus erit inter duos philosophos, quam inter duos Computistas. Sufficiet enim calamos in manus sumere sedereque ad abacos, et sibi mutuo (accito si placet amico) dicere: calculemus.

When a disagreement arises between two philosophers, they will no more need to argue than if they were two [human] computers: it will suffice for them to take pen in hand, sit down at an abacus, and say to each other (inviting, if they like, a friend): let us calculate.

—Die philosophischen Schriften von Gottfried Wilhelm Leibniz (ed. C. J. Gerhardt), Volume 7, Berlin, 1890, p. 200

Mathematics was for a long time an interplay between strict logic, which governed the methodical formulation of proofs, and leaps of intuition, which governed those necessary mathematical postulations which did not fit into Aristotelian logic, especially statements concerning the geometry of the infinite and infinitesimal. This style of mathematics was sufficient to achieve that great triumph, the development of calculus; but the reliance on intuition meant that two mathematicians could easily disagree on whether a theorem was true.

In the nineteenth century, mathematicians set out to remove this flaw. Mathematicians such as Cauchy and Weierstrass developed mathematical analysis: a new foundation for calculus, based on precisely defined concepts of limits and continuity (the epsilon-delta definition of the limit, for example, was first formulated in 1817 and given its definitive form by Karl Weierstrass a few years later). The postulated content of mathematics was eventually reduced to a foundation of set theory and logic, an achievement which naturally increased mathematical scrutiny of those fields. At this point mathematicians found themselves looking into the very foundations of their fields, where mathematical problems blurred into philosophical questions: what is logic? What is truth? What is infinity? What exists? Philosophers also became interested in the potential for mathematical techniques to provide new insight into these old questions.

A mood of optimism was evident across both disciplines, and ambitious programs were launched: in mathematics, the formalist program, headed by the celebrated mathematician David Hilbert, sought to find a universal symbolic language for mathematics, consisting of fundamental axioms and rules to move from one symbolic expression to another. The idea was to define this language only in symbolic or formal terms, sidestepping the difficult question of whether something like a number actually existed, and if so what kind of existence it partook of. Of course, by embracing the arbitrariness of their symbols, formalist mathematicians invited the question of why we should be interested in the results of this symbol-game over any other, or why we should even believe that this symbol-game had any real meaning. The intended capstone to this project, which would bypass this problem of arbitrariness, would be a proof that, whenever this symbol-game produced an arithmetic statement which could be checked by simple calculation, the result would be correct: with such a proof in hand, the meaning or validity of the symbol-game would no longer be a concern.

Meanwhile the analytic philosophers, inspired by the formalization of mathematics, looked further, to an old dream of Leibniz’: they sought a universal language of thought, a symbolic system which could be evaluated by a “calculus ratiocinator” to produce uncontroversial judgments of truth or falsehood. The basic scheme, considerably elaborated by such philosophers as Carnap and Wittgenstein, was to combine atomic facts of sense experience with logic for the discovery of relationships between facts; any sentence in such a language could be systematically reduced to its empirical atoms, and those atoms checked against reality. The use of such a language would completely circumvent any philosophical questions about the meaning of the many things people think about (truth, goodness, love, etc.), for each concept would either resolve to an empirical statement, or simply be excluded from discussion.

These two projects, mathematical and philosophical, culminated in the publication, in 1912, of the Principia Mathematica by Russell and Whitehead, which reduced all mathematics to a sophisticated and fully specified symbolic set theory; and in the publication in 1921 of the Tractatus Logico-Philosophicus by Wittgenstein, an attempt to provide a logical basis for all philosophy. The mathematical project was ultimately more successful. Hilbert’s original goal —to prove that this formal system would never conflict with finitary calculation—would eventually be shown impossible by Godel’s Incompleteness Theorems. But the axiomatic systems developed by Russell and others did provide a workable basis for mathematics, even if this basis could never be completely guaranteed to be sound. The philosophers by contrast were never able to create a credible candidate for “universal language”, and the movement largely fell out of fashion, with Wittgenstein himself turning against his original position.

The final piece in the formalization of mathematics came in 1936-37, when Hilbert’s “Entscheidungsproblem” [decision-problem] was answered independently by two researchers, Church and Turing. The Entscheidungsproblem asked for an algorithm which could produce, for any sufficiently simple mathematical statement, a proof or disproof of that statement. To approach this problem, whose solution turned out to be that no such algorithm was possible, Church and Turing first had to come up with a formal notion of an “algorithm.” Church developed a system called the lambda-calculus, and Turing developed a theoretical machine, the Turing machine. In the following decade, these two systems would prove foundational to the construction and development of electronic computers.

It is remarkable that the transformation of mathematics into an algorithmic form suitable for an electronic computer, an absolutely breathtaking accomplishment requiring approximately a century of work, was undertaken and actually completed before the first electronic computer was ever constructed. The entire project was pursued based on an ideal of a mechanized, formalized human reason (aided by—an abacus!) The electronic computer—which quickly exceeded any human in its ability to carry out mechanical sequences of formal manipulations—would lead to a deep reordering of the relationship between math and machine.

Early developments in electronic computing were very promising for mathematical software. In 1956, a team of scientists constructed the “Logic Theory Machine,” a computer program able to manipulate symbolic proofs; it was able to prove a number of basic theorems from the Principia Mathematica. In 1958 John McCarthy created a computer programming language called LISP: based on Church’s lambda-calculus, it allowed symbolic manipulation to be much more easily specified for a computer. The first encounter with a computer executing what could be seen as the highest level of human reason — the symbolic manipulation of mathematical proofs — and doing so at speeds impossible for any human — must have been an incredible one, and the sense of possibility among some researchers soared. In 1965, Marvin Minsky predicted that the problem of “artificial intelligence” would be solved within a generation.

But the symbolic road to intelligence led into a morass of difficulties. An algorithm to generate mathematical truths had already been worked out; but this algorithm relied on an enumeration of all possible symbolic expressions, and such a list would be vastly too long to be searched even by the most powerful computers. The constraints of real computers began to force researchers to confront a problem hardly considered during the construction of formalist mathematics: algorithmic efficiency. To prove theorems at the level of human mathematicians, computers would have to discard almost all possible expressions, homing in somehow on those with a good chance of unlocking the proof. This is the role played, in a human mathematician’s work, by intuition; it proved very difficult indeed to teach to a computer.

In the early decades of AI research, most researchers saw the efficiency issues which plagued mathematical algorithms—as well as other AI problems, like language translation and chess—as something that could be resolved with a bit of work. They were confident in the ability of symbolic manipulation by computer to match human reasoning. In 1965, philosopher Hubert Dreyfus challenged these optimistic assumptions: human intelligence, he stated, was not just formal symbolic manipulation. Aspects of human cognition like common sense and unconscious mastery were essentially different from explicit symbol manipulation, and thus could not be imitated by the symbol-manipulating algorithms on which the AI program was based, but were extremely important to human thought.

Dreyfus was ignored or scorned by most in the AI community, but his critique now seems prescient in many ways. The AI projects which aimed to supplement symbolic reasoning with heuristics, fact databases, guided search, or automated learning—to supplement computer algorithms with something analogous to human intuition—never made very much progress. In 1997, the computer Deep Blue beat the human champion at chess, in what was seen as a triumph for AI. But it is telling that the basic algorithm used by Deep Blue, alpha-beta pruning, was a very crudely-guided exhaustive search of positions, invented in 1958. Deep Blue was a capable chess player, not because it had any kind of intuition to guide its brute force search, but because it was so stunningly fast at brute force search; its victory was a triumph more of transistor research than of AI research. Machine mathematics, with an exponentially larger search space than that required for chess, remained out of reach.

What is so interesting about machine mathematics compared with other branches of AI projects is that, as with chess, the rules of the game can easily be encoded in a computer, and there are simple objective criteria for a competent program. A computer philosopher, no matter how brilliant, would always face questions about whether their programming truly encompassed all the essentials of human thought; but a computer mathematician, if it could come up with good theorems, would face few such objections. Nonetheless, human mathematicians, relying on intuition, on pictures in their minds, on imprecise notions and imaginary objects, are easily more capable than the fastest and best-programmed computer. If two mathematicians sat at an abacus and calculated, they would eventually resolve whatever problem they started with—but it seems that their friends, who stood around and argued and gestured and made leaps of unsupported intuition, would resolve it in far less time.

Since the fall of the early AI program, machine mathematics has adapted to its capabilities and limitations. In 1976, the mathematicians Appel and Haken proved a long-standing conjecture, the four-color theorem, by reducing it to a few thousand special cases, then checking those cases with a computer. The cases given to the computer were what a mathematician would call “trivial”: they required no creativity to check. Nonetheless, the proof as written would have been essentially impossible without the computer’s untiring ability to tackle the large number of individual cases. In 1984, the logician Per Martin-Löf created type theory, a scheme by which a computer program could be equated to a mathematical proof.

Type theory and its descendants are used, now, for two purposes: to aid the creation of proofs by using programs called proof assistants to check logic and solve small pieces of logic; and to aid the creation of reliable software by writing the software alongside a proof of its properties. In 2012 a proof assistant was used to double-check the long, difficult proof of the Feit-Thompson theorem; the same proof assistant, Coq, has been used to write a compiler for the programming language C, a compiler which is proven to compile correctly. The explicit use of mathematical inference in computation is still very limited, but a division of labor seems to be taking shape: mechanical computation is used for its reliability, its exhaustiveness, its tireless attention to detail; while human thought constructs meaning and intuition from symbols, and plans, considers, and organizes the mechanical details of proof-making.

The prospect of thinking machines has always tended to arouse two contrary reactions: on the one hand a utopian faith that mechanized intelligence will spell an end to all that is quarrelsome, vague, halting, and uncertain in human thought; on the other a revulsive fear that mechanized intelligence would also mean the end of human ethics and aesthetics, and generally all the indefinable things that we hold dear as part of the human condition. The history of machine mathematics raises a startling idea: perhaps machine intelligence, if it is to really overcome the dominance of human thought even in the most precisely defined and abstract fields, must grow to encompass something much like human intuition.

---