Extension: MathSoMac: the social machine of mathematics

点击翻译按钮获取中文摘要

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?