Digital computing changed mathematics at every level down to the core of mathematical practice, the search for proofs. This award supports doctoral dissertation research that traces how computers have been used in the development of proofs and how their use changed mathematical knowledge and practice in the United States. The project is motivated historically, anthropologically, and philosophically to explore the following questions. How are mathematical ideas related to the technologies with which they are discovered and explored? How is the cognitive work of mathematics altered by the introduction of computing? How is human intelligence understood through attempts to build reasoning machines? The period of interest begins in the mid-1950s with early Artificial Intelligence, and it concludes with the contemporary work of Fields medalist Vladimir Voevodksy.
Intellectual Merit This project engages the ongoing interest of Science Studies in knowledge making, especially at the interface between humans and machines. It will explore mathematical knowledge and its material dimensions, which has until now been largely unexplored. Using archival materials, interviews, and technical documents including operations manuals and source code, the doctoral candidate will explore transformations in the institutional setting, material constitution, practices, and cognitive landscape of mathematical research that manifested around the digital computer. The intellectual merit of this project lies in its synthesizing and intervening in theoretical scholarship from science studies, history of mathematics, history of technology, and history of science (often pursued separately).
Potential Broader Impact The significance of computer proof assistance in mathematical research is intensifying. This project can assist current researchers and funding agencies in the assessment and pursuit of new projects in light of past research and historical context. Further, an analysis of the multifarious past and present strategies for using computing in mathematics can suggest new possibilities for using computer assistance in other disciplines that may otherwise be unaware of them.
This project is motivated by an interest in how different communities developed new practices of knowledge-production using digital computing. The project culminated in a doctoral dissertation - After Math: (Re)configuring Minds, Proof, and Computing in the Postwar United States - that documents early attempts to use computers to prove mathematical theorems. Historically, mathematical proof has been considered an exclusive and exemplary accomplishment of human reasoning. The dissertation tracks how computing intervened in that history by offering new and often controversial possibilities for mathematical demonstration. The dissertation argues that existing disciplines, including mathematics, had to be re-conceptualized through the lens of computing technology in order to create a place for its use. In tandem, computers had to be re-tooled to make new uses possible. To make computer proof a reality, mathematical objects were transformed into digital objects and theorem-proving practices were translated into algorithmic computer operations and techniques of programming and usership. Early programmers had to navigate materialities and concerns quite foreign to the human experience of mathematics, introducing novel perspectives to the formulation and exploration of mathematical problems. This project focuses in particular on material and formal tools – like programming languages, computational models, data structures, and user interfaces – that were developed in the context of early attempts to represent and study the objects of mathematics in the media of digital computation. The dissertation situates the development of these technical tools in broader narratives, imaginations, and philosophies about the character of the computer itself, how it should be studied, and its possible futures. Computers challenged more than practices and understandings of proof. They also troubled traditional disciplinary distinctions like those between mathematics and engineering, pure and applied science, and a priori and empirical research. As such, the project also attended to the disciplinary and institutional landscape that informed, enabled, and challenged the use of computers in theorem-proving. This is in part a story about the relocation of the work of proof to new sites. Many attempts to automate proof were not undertaken in mathematics departments or even at universities. Instead, some were based in government, military, or industrial research institutions and some even became commercial ventures. Through this work, proof was also transported into the hands of practitioners from diverse disciplinary backgrounds including classics, psychology, and business. The project follows the elements of mathematical proof into the materiality of computing, into the discourse surrounding computers, and into the communities and institutions in which computing took place. The project attended to all three of these dimensions in order to understand where and how the work of proof is being done in new ways in the digital age. Computers can now be found in virtually every corner of social life. They are largely taken for granted. However, getting computers to be useful and usable in those myriad places was surprisingly difficult, especially in the early decades. Little historical and sociological attention has been paid to what was actually involved in negotiating a place for computers in different arenas of society. This project contributes to our understanding of how computers were introduced to mathematical knowledge-production. The lessons of this story are generalizable. The kinds of obstacles, innovations, and repercussions that were involved in introducing computers to mathematical theorem-proving can also be found where computers were introduced to medicine, corporate management, education, and so on. This work engages questions about the character of digital media and of computer-assisted knowledge production that remain relevant and prolific today. The project also contributes to ongoing conversations about representation, materiality, practice, and cognition in the history of science and technology, but also in media studies and the history and philosophy of mathematics. These conversations concern how our knowledge is made, and made differently, and made possible in different times and places where practitioners are equipped with different tools.
