Epistemic Phase Transitions in Mathematical Proofs

• URL: http://arxiv.org/abs/2004.00055v2
• Date: Tue, 12 Apr 2022 15:25:22 GMT
• Title: Epistemic Phase Transitions in Mathematical Proofs
• Authors: Scott Viteri and Simon DeDeo
• Abstract summary: We show that under a cognitively-plausible belief formation mechanism, belief in mathematical arguments can undergo a dramatic and rapidly-propagating jump from uncertainty to near-complete confidence at reasonable levels of claim-to-claim error rates. 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.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof. Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
  Minimo is an agent that learns to pose problems for itself (conjecturing) and solve them (theorem proving) We combine methods for constrained decoding and type-directed synthesis to sample valid conjectures from a language model. Our agent targets generating hard but provable conjectures - a moving target, since its own theorem proving ability also improves as it trains.
  arXiv  Detail & Related papers  (2024-06-30T13:34:54Z)
• Machine learning and information theory concepts towards an AI Mathematician [77.63761356203105]
  The current state-of-the-art in artificial intelligence is impressive, especially in terms of mastery of language, but not so much in terms of mathematical reasoning. This essay builds on the idea that current deep learning mostly succeeds at system 1 abilities. It takes an information-theoretical posture to ask questions about what constitutes an interesting mathematical statement.
  arXiv  Detail & Related papers  (2024-03-07T15:12:06Z)
• Quantum theory can consistently describe the use of itself in Frauchiger-Renner's Gedankenexperiment [0.0]
  Frauchiger and Renner have presented a no-go theorem, which makes quantum mechanics more controversial. We discuss the validity of their proof approach in this letter.
  arXiv  Detail & Related papers  (2022-09-19T12:36:53Z)
• Connes implies Tsirelson: a simple proof [91.3755431537592]
  We show that the Connes embedding problem implies the synchronous Tsirelson conjecture. We also give a different construction of Connes' algebra $mathcalRomega$ appearing in the Connes embedding problem.
  arXiv  Detail & Related papers  (2022-09-16T13:59:42Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  Theorem proving in natural mathematical language plays a central role in mathematical advances and education. We develop NaturalProver, a language model that generates proofs by conditioning on background references. NaturalProver is capable of proving some theorems that require short (2-6 step) proofs, and providing next-step suggestions that are rated as correct and useful over 40% of the time.
  arXiv  Detail & Related papers  (2022-05-25T17:01:18Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  We present a novel stepwise method NLProofS (Natural Language Proof Search) NLProofS learns to generate relevant steps conditioning on the hypothesis. It achieves state-of-the-art performance on EntailmentBank and RuleTaker.
  arXiv  Detail & Related papers  (2022-05-25T02:22:30Z)
• Maieutic Prompting: Logically Consistent Reasoning with Recursive Explanations [71.2950434944196]
  We develop Maieutic Prompting, which infers a correct answer to a question even from the noisy and inconsistent generations of language models. Maieutic Prompting achieves up to 20% better accuracy than state-of-the-art prompting methods.
  arXiv  Detail & Related papers  (2022-05-24T06:36:42Z)
• Noisy Deductive Reasoning: How Humans Construct Math, and How Math Constructs Universes [0.5874142059884521]
  We present a computational model of mathematical reasoning according to which mathematics is a fundamentally process. We show that this framework gives a compelling account of several aspects of mathematical practice.
  arXiv  Detail & Related papers  (2020-10-28T19:43:14Z)
• Epistemic Horizons: This Sentence is $\frac{1}{\sqrt{2}}(|True\rangle + |False\rangle)$ [0.0]
  In [Found. Phys. 48.12: 1669], the notion of 'epistemic horizon' was introduced as an explanation for many of the puzzling features of quantum mechanics. We give a brief presentation of the framework, and then demonstrate how it naturally yields Bell inequality violations.
  arXiv  Detail & Related papers  (2020-07-29T15:26:53Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.