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.
...MoreSimilar Citations
Article
Laura Leondina Campanozzi;
Eugenio Guglielmelli;
Eleonora Cella;
Giampaolo Ghilardi;
Mirta Michilli;
Alfonso Molina;
Massimo Ciccozzi;
Vittoadolfo Tambone;
(December 2019)
Building Trust in Social Robotics: A Pilot Survey
(/isis/citation/CBB220307519/)
Thesis
Mamo, Andrew Benedict;
(2011)
Post-Industrial Engineering: Computer Science and the Organization of White-Collar Work, 1945--1975
(/isis/citation/CBB001567323/)
Book
Corinna Schlombs;
(2019)
Productivity Machines: German Appropriations of American Technology from Mass Production to Computer Automation
(/isis/citation/CBB010027447/)
Article
Ada Diaconescu;
(2019)
Efficiency Versus Creativity as Organizing Principles of Socio-Technical Systems: Why Do We Build (Intelligent) Systems? [Commentary]
(/isis/citation/CBB344168616/)
Book
Mark Coeckelbergh;
(2020)
AI Ethics
(/isis/citation/CBB990965100/)
Article
Cook, Diane J.;
(2012)
How Smart is Your Home?
(/isis/citation/CBB001320459/)
Article
Ross D. King;
Vlad Schuler Costa;
Chris Mellingwood;
Larisa N. Soldatova;
(March 2018)
Automating Sciences: Philosophical and Social Dimensions
(/isis/citation/CBB373191091/)
Book
Copeland, B. Jack;
(2012)
Turing: Pioneer of the Information Age
(/isis/citation/CBB001253045/)
Book
Kwinter, Sanford;
Davidson, Cynthia C.;
(2007)
Far from Equilibrium: Essays on Technology and Design Culture
(/isis/citation/CBB000831105/)
Article
Ashley Shew;
(March 2020)
Ableism, Technoableism, and Future AI
(/isis/citation/CBB740369225/)
Book
Ethem Alpaydın;
(2021)
Machine Learning
(/isis/citation/CBB513990166/)
Book
Giovanni Landi;
(2020)
Intelligenza Artificiale come Filosofia
(/isis/citation/CBB832397878/)
Chapter
Graham Matthews;
(2020)
‘A Push-Button Type of Thinking’: Automation, Cybernetics, and AI in Midcentury British Literature
(/isis/citation/CBB748811083/)
Article
Grier, David Alan;
(1998)
The Math Tables Project of the WPA: The Reluctant Start of the Computing Era
(/isis/citation/CBB000112041/)
Article
Helen Piel;
Rudolf Seising;
Christian Götter;
(2022)
The Computer Metaphor. Anchoring the Fear of Human Obsolescence(s) since the 20th Century
(/isis/citation/CBB645368745/)
Article
Theodora Vardouli;
David Theodore;
(April-June 2021)
Walking Instead of Working: Space Allocation, Automatic Architecture, and the Abstraction of Hospital Labor
(/isis/citation/CBB134939420/)
Article
Grier, David Alan;
(2001)
The Rise and Fall of the Committee on Mathematical Tables and Other Aids to Computation
(/isis/citation/CBB000102447/)
Book
Jack Copeland;
Jonathan Bowen;
Mark Sprevak;
Robin Wilson;
(2017)
The Turing Guide
(/isis/citation/CBB709222979/)
Article
Dick, Stephanie;
(2011)
AfterMath: The Work of Proof in the Age of Human--Machine Collaboration
(/isis/citation/CBB001220009/)
Article
R. A. Nelsen;
(2017)
Race and Computing: The Problem of Sources, the Potential of Prosopography, and the Lesson of Ebony Magazine
(/isis/citation/CBB045609712/)
Be the first to comment!