Doctoral Dissertation Research: On Negotiating the Role of Computers in Developing Mathematical Proofs

博士论文研究：论计算机在数学证明开发中的作用

• 批准号: 1154889
• 负责人: Peter Galison
• 金额: $ 0.99万
• 依托单位: Harvard University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-03-15 至 2014-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1154889&HistoricalAwards=false
• 关键词: Doctoral; Dissertation; Research; Negotiating; Role

IntroductionDigital 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 MeritThis 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 ImpactThe 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.

数字计算改变了数学的每一个层面，直到数学实践的核心，即寻找证明。该奖项支持博士论文研究，追溯计算机如何被用于证明的发展，以及它们的使用如何改变美国的数学知识和实践。该项目的动机是历史学，人类学，并探讨以下问题。数学思想与发现和探索它们的技术有什么关系？计算的引入如何改变了数学的认知工作？如何通过尝试构建推理机器来理解人类智能？感兴趣的时期开始于20世纪50年代中期的早期人工智能，并以菲尔兹奖获得者弗拉基米尔沃沃德斯基的当代工作结束。智力优点这个项目从事科学研究在知识的持续兴趣，特别是在人类和机器之间的接口。它将探索数学知识及其物质层面，这在很大程度上是迄今为止尚未探索。使用档案材料，访谈和技术文件，包括操作手册和源代码，博士生将探索在机构设置，材料构成，实践和数学研究的认知景观，体现在数字计算机周围的转变。这个项目的智力价值在于它综合和干预来自科学研究，数学史，技术史和科学史（通常单独进行）的理论学术。潜在的更广泛的影响计算机辅助证明在数学研究中的重要性正在加强。该项目可以帮助当前的研究人员和资助机构根据过去的研究和历史背景评估和追求新的项目。此外，对过去和现在在数学中使用计算的各种策略的分析可以为在其他学科中使用计算机辅助提供新的可能性，否则这些学科可能不知道它们。