Mathematical theorem-proving was among the earliest domains of interest to Artificial Intelligence practitioners in the United States. Their automation of proof, however, involved nontrivial transformations in the character and constitution of mathematical objects and practices. These transformations were characterized in large part by the material specificity of computing technologies themselves and by the Cold War research ethos in which this work was pursued. This talk will explore one early example - the Logic Theory Machine - developed by Allen Newell, Herbert Simon, and John Clifford Shaw during 1955-1957 at the RAND Corporation. It was designed to produce proofs of logical theorems from Alfred North Whitehead and Bertrand Russell's Principia Mathematica. The talk follows the migration of logical expressions and inferences from the pages of Principia into the digital media of the JOHNNIAC mainframe computer.