After Math: Reasoning, Computing, and Proof in the Postwar United States (via Skype)

Duration: 1 hour 5 mins

Share this media item:

Embed this media item:

<iframe width="_width_" height="_height_" src="https://sms.cam.ac.uk/media/2525593/embed" frameborder="0" scrolling="no" allowfullscreen></iframe>

Choose size:

About this item

Available Formats

About this item

Description:	Dick, S Friday 14th July 2017 - 13:30 to 14:30


Created:	2017-07-26 15:49
Collection:	Big proof
Publisher:	Isaac Newton Institute
Copyright:	Dick, S
Language:	eng (English)


Abstract:	Computers ought to produce in the long run some fundamental change in the nature of all mathematical activity.” These words, penned in 1958, capture the motivation behind an early field of computing research called Automated Theorem-Proving or Automated Reasoning. Practitioners of this field sought to program computers to prove mathematical theorems or to assist human users in doing so. Everyone working in the field agreed that computers had the potential to make novel contributions to the production of mathematical knowledge. They disagreed about almost everything else. Automated theorem-proving practitioners subscribed to complicated and conflicting visions of what ought to count and not count as a mathematical proof. There was also disagreement about the character of human mathematical faculties - like intuition, understanding, and reasoning - and how much the computer could be made to possess them, if at all. Different practitioners also subscribed to quite different imaginations of the computer itself, its limitations and possibilities. Some imagined computers as mere plodding “slaves” who would take over tedious and mechanical elements of mathematical research. Others imagined them more generously as “mentors” or “collaborators” that could offer novel insight and direction to human mathematicians. Still others believed that computers would eventually become autonomous agents of mathematical research. Automated theorem-proving practitioners took their visions of mathematicians, minds, computers, and proof, and built them right in to their theorem-proving programs. Their efforts did indeed precipitate transformations in the character of mathematical activity but in varied and often surprising ways. They crafted new formal and material tools and practices for wielding them that reshaped the work of proof. They also reimagined what “reasoning” itself might be and what logics capture or prescribe it. With a focus on communities based in the United States in the second half of the twentieth century, this talk will introduce different visions the novel practices and materialities of mathematical knowledge-making that emerged in tandem.

Abstract:

Computers ought to produce in the long run some fundamental change in the nature of all mathematical activity.” These words, penned in 1958, capture the motivation behind an early field of computing research called Automated Theorem-Proving or Automated Reasoning. Practitioners of this field sought to program computers to prove mathematical theorems or to assist human users in doing so. Everyone working in the field agreed that computers had the potential to make novel contributions to the production of mathematical knowledge. They disagreed about almost everything else. Automated theorem-proving practitioners subscribed to complicated and conflicting visions of what ought to count and not count as a mathematical proof. There was also disagreement about the character of human mathematical faculties - like intuition, understanding, and reasoning - and how much the computer could be made to possess them, if at all. Different practitioners also subscribed to quite different imaginations of the computer itself, its limitations and possibilities. Some imagined computers as mere plodding “slaves” who would take over tedious and mechanical elements of mathematical research. Others imagined them more generously as “mentors” or “collaborators” that could offer novel insight and direction to human mathematicians. Still others believed that computers would eventually become autonomous agents of mathematical research. Automated theorem-proving practitioners took their visions of mathematicians, minds, computers, and proof, and built them right in to their theorem-proving programs. Their efforts did indeed precipitate transformations in the character of mathematical activity but in varied and often surprising ways. They crafted new formal and material tools and practices for wielding them that reshaped the work of proof. They also reimagined what “reasoning” itself might be and what logics capture or prescribe it. With a focus on communities based in the United States in the second half of the twentieth century, this talk will introduce different visions the novel practices and materialities of mathematical knowledge-making that emerged in tandem.

Available Formats

Format	Quality	Bitrate	Size
MPEG-4 Video	640x360	1.94 Mbits/sec	947.24 MB	View	Download
WebM	640x360	451.18 kbits/sec	214.80 MB	View	Download
iPod Video	480x270	527.83 kbits/sec	251.29 MB	View	Download
MP3	44100 Hz	252.7 kbits/sec	120.31 MB	Listen	Download
Auto *	(Allows browser to choose a format it supports)