论文标题
数学证明中的认知阶段过渡
Epistemic Phase Transitions in Mathematical Proofs
论文作者
论文摘要
数学证明既是确定性的范式，又是我们在文化记录中拥有的一些最明确的论点。但是，它们的明确性导致了悖论，因为误差的可能性随着参数的扩展而成倍增长。当数学家遇到证据时，她如何相信？在这里，我们表明，在结合演绎和绑架推理的认知性信仰形成机制下，对数学论点的信念可以经历我们所谓的认知阶段转变：从不确定性到近乎完整的置信度，以合理的索赔索赔级别的索赔级别的索赔率，从不确定性到几乎完整的置信度。为了证明这一点，我们分析了正式推理系统COQ的四十八个机器辅助证明数据集，包括从古代到21世纪数学的主要定理，以及五个手工构建的案例，包括Euclid，Apollonius，Apollonius，Apollonius，Apollonius，Apollonius，Hernstein在Algebra和Aldrew Wiles Wiles的Pirct of Fermass of oferoreor的证明。我们的结果既依赖数学历史和哲学的最新工作，涉及我们如何理解证据，以及关于认知科学的基本问题，关于我们如何证明复杂信念的正当性。
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 the probability of error grows exponentially as the argument expands. When a mathematician encounters a proof, how does she come to believe it? Here we show that, under a cognitively-plausible belief formation mechanism combining deductive and abductive reasoning, belief in 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 five hand-constructed cases including Euclid, Apollonius, Hernstein's Topics in Algebra, and Andrew Wiles's proof of Fermat's Last Theorem. Our results bear both on recent work in the history and philosophy of mathematics on how we understand proofs, and on a question, basic to cognitive science, of how we justify complex beliefs.
