A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into peril. Now may be the time to reconcile theory and practice, i.e. precision and intuition, through the advent of computer proof assistants. For the most time this has been a topic for experts in specialized communities. However, mathematical proofs have become increasingly sophisticated, stretching the boundaries of what is humanly comprehensible, so that leading mathematicians have asked for formal verification of their proofs. At the same time, major theorems in mathematics have recently been computer-verified by people from outside of these communities, even by beginning students. This article investigates the gap between the different definitions of a proof and possibilities to build bridges. It is written as a polemic or a collage by different members of the communities in mathematics and computer science at different stages of their careers, challenging well-known preconceptions and exploring new perspectives.
翻译:证明是数学中最重要的概念之一。 但是,在理论上如何界定证据和如何实际使用证据之间,存在着明显的差别。 这使得数学作为精确科学的独特地位处于危险之中。 现在也许是通过计算机校对助理的出现来协调理论和实践(即精确和直觉)的时候。 这在多数时候一直是专业社区专家的话题。 然而,数学证据已经变得越来越复杂,扩大了人类可以理解的界限,因此主要数学家要求正式核实其证据。 同时,数学的主要理论最近也由这些社区以外的人,甚至由刚开始学习的人进行计算机验证。 文章研究了证据的不同定义与架设桥梁的可能性之间的差距。 文章是作为数学和计算机科学不同社区成员在其职业生涯不同阶段的论调或串联而写成的,挑战了众所周知的预知和探索了新的观点。