Extension: MathSoMac: the social machine of mathematics

这是该奖学金的延伸：《MathSoMac：数学的社交机器》，这是一项既定的职业奖学金，2014-2018年，EPSRC EP/K040251/2数学被公认为一项深刻的智力成就，对财富创造和生活质量的许多方面产生了影响，并作为独特的文化资本，吸引了大量人群前往展览和公开讲座。几个世纪以来，最高水平的数学一直被视为一种孤立的创造性活动，用来证明一个困难的定理，供同行审查和接受。然而，在一个显著的拐点上，新技术正在从根本上扩展个人的力量和限制。像Polyath或MathOverflow这样的网站允许研究人员相互协作，并“展示他们的工作”，这样他们专业领域以外的其他人就可以参与他们的研究，并及早洞察可能有用的东西。现在，计算机证明通常被用于硬件和软件设计的验证，在网络安全中，计算机证明超越了符号计算或数值模拟，以生成人类无法理解的过于复杂的数学论点，并从基本原理检查这些推理链。这些现象通常被认为是截然不同的，仅通过它们与数学的关系联系在一起。然而，它们有许多共同的特征，尤其是，正如我们在最初的项目中所展示的那样，它们归根结底依赖于人类和社会问题的数学判断和创造力。在这项提案中，为了扩展我们目前的研究，我们将这些现象视为一个统一的整体，其中人和计算机系统结合成一个单一的问题解决实体，其中个人彼此交互，并与利用计算机证明的单个“引擎”的计算机进行交互。我们把这种数学生产和应用的模型称为基于伯纳斯-李大约20年前提出的“社会机器”新范式的“数学社会机器”。我们关注两个研究问题：=“超越推理”：我们如何让人类数学家享受计算机证明的好处，同时保护他们免受其复杂性的影响？=“走向影响：我们如何评估基础研究的影响和文化资本？”

This is an extension of the Fellowship: 'MathSoMac: the social machine of mathematics', which is an Established Career Fellowship, 2014-2018, EPSRC EP/K040251/2Mathematics is recognized as a profound intellectual achievement, with impact on many aspects of wealth creation and quality of life, and as unique cultural capital, drawing crowds to exhibitions and public lectures. For centuries, the highest level of mathematics has been seen as an isolated creative activity, to produce a proof of a difficult theorem for review and acceptance by research peers. However, at a remarkable inflexion point, new technology is radically extending the power and limits of individuals. Websites such as the polymath or mathoverflow sites allow researchers to collaborate with each other, and "show their working", so that others outside their specialist field can engage with their research and get early insight into things that might be useful. Now routinely used for verification of hardware and software designs, and in cyber-security, computer proof goes beyond symbolic computation, or numerical simulation, to generate mathematical arguments too complex for humans to grasp, and to check these chains of inference from first principles. These phenomena have typically been viewed as distinct, linked only by their relationship to mathematics. Yet they have many common features, not least, as we showed in the original project, their dependence, ultimately, on human and social issues of mathematical judgement and creativity. In this proposal, to extend our current research, we view these phenomena as a united whole, in which people and computer systems combine into a single problem-solving entity, where individuals interact with each other, and with computers which draw on a single "engine" of computer proof. We call this model of the production and application of mathematics the "social machine of mathematics" based on the new paradigm of "Social machines", identified by Berners-Lee about 20 years ago.We focus on two research questions: === "Beyond Inference": how can we give human mathematicians the benefits of computer proof, while shielding them from its complexity?=== " Towards impact: how can we evaluate the impact and cultural capital of foundational research?