数学真理的爆炸性证明

• 2020 年 4 月 3 日
• 笔记

数学证明既是确定范式又是一些最清楚为阐释的论证，这些在我们文化中都已经十分确定。然而，它们的这种明确性又会导致悖论，因为当论证扩大时，误差概率就会呈指数增长。这篇文章中，介绍了认知似然信念形成机制。它结合了演绎推理和外展推理、数学论证内容，可以解释我们称之为认知阶段过渡的过程：这是一种对合理水平内误差率从不确定到近乎完全肯定的急剧快速的转变过程。

为此，我们分析了一个包含48个机器辅助的证明数据集。其中有已标准化的推理系统 Coq，包括从古代到21世纪数学的主要数学定理，同时，也有四种手动建立的案例，例如欧几里得，阿波罗尼乌斯，斯宾诺莎和安德鲁·怀尔斯相关数学定理。本文结果涉及了历史和数学哲理，以及从基础和认知科学层面，探究了我们是如何形成一种信念并向其他人证明他的这一问题。

原文：Explosive Proofs of Mathematical Truths

Mathematical proofs are both paradigms of certainty and some of the most explicitly-justified arguments that we have in the cultural record. Their very explicitness, however, leads to a paradox, because their probability of error grows exponentially as the argument expands. Here we show that under a cognitively-plausible belief formation mechanism that combines deductive and abductive reasoning, mathematical arguments can undergo what we call an epistemic phase transition: a dramatic and rapidly-propagating jump from uncertainty to near-complete confidence at reasonable levels of claim-to-claim error rates.

To show this, we analyze an unusual dataset of forty-eight machine-aided proofs from the formalized reasoning system Coq, including major theorems ranging from ancient to 21st Century mathematics, along with four hand-constructed cases from Euclid, Apollonius, Spinoza, and Andrew Wiles. Our results bear both on recent work in the history and philosophy of mathematics, and on a question, basic to cognitive science, of how we form beliefs, and justify them to others.

原文：Explosive Proofs of Mathematical Truths

数学证明既是确定范式又是一些最清楚为阐释的论证，这些在我们文化中都已经十分确定。然而，它们的这种明确性又会导致悖论，因为当论证扩大时，误差概率就会呈指数增长。这篇文章中，介绍了认知似然信念形成机制。它结合了演绎推理和外展推理、数学论证内容，可以解释我们称之为认知阶段过渡的过程：这是一种对合理水平内误差率从不确定到近乎完全肯定的急剧快速的转变过程。

为此，我们分析了一个包含48个机器辅助的证明数据集。其中有已标准化的推理系统 Coq，包括从古代到21世纪数学的主要数学定理，同时，也有四种手动建立的案例，例如欧几里得，阿波罗尼乌斯，斯宾诺莎和安德鲁·怀尔斯相关数学定理。本文结果涉及了历史和数学哲理，以及从基础和认知科学层面，探究了我们是如何形成一种信念并向其他人证明他的这一问题。

原文链接：https://arxiv.org/abs/2004.00055

原文作者：Scott Viteri,Simon DeDeo