This dissertation examines the history of three early computer programs that were designed to prove mathematical theorems: The Logic Theory Machine, the Program P, and the Automated Reasoning Assistant, all developed between 1955 and 1975. I use these programs as an opportunity to explore ways in which mathematical knowledge and practice were transformed by the introduction of modern computing. The prospect of automation generated disagreement about the character of human mathematical faculties like intuition, reasoning, and understanding and whether computers could be made to possess or participate in them. It also prompted novel discourse concerning the character of mathematical knowledge and how it should be produced. I track how the architects of each program built their beliefs about minds, computation, and proof into their theorem-proving programs and, in so doing, crafted new tools and techniques for the work of mathematics.
The practitioners featured in this dissertation were interested in whether or not computers could “think.” I, on the other hand, am interested in how people think differently when they work with computers. And in particular how they thought differently about mathematics as they crafted a place for computers in the work of proof. I look for traces of their new ways of thinking in how they implemented their software. This is a new historiographical approach from existing history of computing that, for the most part, does not engage software at all or engages high-level descriptions or models of software.
I argue this: what were for my actors implementation concerns are in fact significant epistemological issues for the history of mathematics. Especially in the early decades, actually getting programs to run on computers was no small feat. In implementing programs practitioners had to craft many new tools, both formal and material - from programming languages and data structures to punched card encodings and user interfaces. The work of implementation spans multiple media - from paper to transistor - and involves many practices - from diagramming to coding - demonstrating that the media of the “digital age” are multiple indeed. Moreover, implementation is the site where we see practitioners rethinking their objects of interest, their disciplines, their theories, through the lens of computation - what is possible and impossible for computers to do. Implementation is the practice of automation.
In implementing their theorem-proving software, the actors in this dissertation gave new formulations and had new experiences of mathematical intuition, logical rules of inference, and other key tenets of twentieth-century notions of proof. The communities explored here were among the most influential and celebrated early contributors to automated theorem-proving. Each had quite a different relationship to the postwar American academic landscape relative to their disciplinary, institutional, and political makeup. Most importantly for they fundamentally and explicitly disagreed with each other about how the automation of proof should be done. Because of this, they developed very different automated theorem-proving programs – one seeking to simulate the human mind, another seeking to surpass it, and another seeking to develop theorem-proving software that would collaborate with a human user. Each of these projects intervened in the history of mathematics by introducing new forms – both social and technical – of proof.
| Identifer | oai:union.ndltd.org:harvard.edu/oai:dash.harvard.edu:1/14226096 |
| Date | January 2015 |
| Creators | Dick, Stephanie Aleen |
| Contributors | Galison, Peter L. |
| Publisher | Harvard University |
| Source Sets | Harvard University |
| Language | English |
| Detected Language | English |
| Type | Thesis or Dissertation, text |
| Format | application/pdf |
| Rights | embargoed |
Page generated in 0.0015 seconds