Jonas Bayer, Christoph Benzmüller, Kevin Buzzard, Marco David, Leslie Lamport, Yuri Matiyasevich, Lawrence Paulson, Dierk Schleicher, Benedikt Stock, Efim Zelmanov
备注：
17 pages, 1 figure
发表信息：
Notices of the American Mathematical Society (January 2024), Vol. 71, No. 1, pp. 79-92
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.
Correctness, Artificial Intelligence, and the Epistemic Value of Mathematical Proof
Department of Logic and Philosophy of Science University of California, Irvine（逻辑与科学哲学系加州大学伊维奇分校）；Department of Mathematics University of California, Irvine（数学系加州大学伊维奇分校）
Epistemic Phase Transitions in Mathematical Proofs
Stanford University（斯坦福大学）；Carnegie Mellon University（卡内基梅隆大学）；Santa Fe Institute（圣塔菲研究所）
数学证明既是确定性的范式，也是我们在文化记录中拥有的一些最明确合理的论点。然而，它们的明确性导致了一个悖论，因为随着论证的扩展，错误的概率呈指数级增长。当一个数学家遇到一个证明时，她是如何相信它的？在这里，我们表明，在一个认知上合理的信念形成机制结合演绎推理和溯因推理，相信数学论点可以经历我们所说的认知相变：一个戏剧性的和快速传播的跳跃，从不确定性到接近完全的信心，在合理的水平的索赔到索赔的出错率。为了证明这一点，我们分析了一个不寻常的数据集，其中包含来自形式化推理系统Coq的48个机器辅助证明，包括从古代到21世纪数学的主要定理，以及五个手工构建的案例，包括Euclid，Apollonius，Hernstein's Topics in Algebra和Andrew Wiles对Fermat's Last Theorem的证明。我们的研究结果既与数学历史和哲学中关于我们如何理解证明的最新工作有关，也与认知科学中的一个基本问题有关，即我们如何证明复杂的信念。
