Related papers: Epistemic Phase Transitions in Mathematical Proofs
"Systems that Explain Themselves" appears a provocative wording, in particular in the context of mathematics education -- it is as provocative as the idea of building educational software upon technology from computer theorem proving. In…
A model of knowledge representation is described in which propositional facts and the relationships among them can be supported by other facts. The set of knowledge which can be supported is called the set of cognitive units, each having…
Euclid pioneered the concept of a mathematical theory developed from axioms by a series of justified proof steps. From the outset there were critics and improvers. In this century the use of computers to check proofs for correctness sets a…
Mathematics cannot anymore be assimilated to a linguistic game, where formal proofs are strongly differentiated with conjectural thinking, without building any category of knowledge to understand the passage (Wittgenstein's gist). Nowadays,…
The problem of induction has persisted since Hume exposed the logical gap between repeated observation and universal inference. Traditional attempts to resolve it have oscillated between two extremes: the probabilistic optimism of Laplace…
Although most of the automated theorem-proving approaches depend on formal proof systems, informal theorem proving can align better with large language models' (LLMs) strength in natural language processing. In this work, we identify a…
Belief systems are often treated as globally consistent sets of propositions or as scalar-valued probability distributions. Such representations tend to obscure the internal structure of belief, conflate external credibility with internal…
Can artificial intelligence truly contribute to creative mathematical research, or does it merely automate routine calculations while introducing risks of error? We provide empirical evidence through a detailed case study: the discovery of…
The increasing incorporation of Artificial Intelligence in the form of automated systems into decision-making procedures highlights not only the importance of decision theory for automated systems but also the need for these decision…
Proofs of the fundamental theorem of algebra can be divided up into three groups according to the techniques involved: proofs that rely on real or complex analysis, algebraic proofs, and topological proofs. Algebraic proofs make use of the…
In a recent historical overview, Cristian S. Calude, Elena Calude, and Solomon Marcus identify eight stages in the development of the concept of a mathematical proof in support of an ambitious conjecture: we can express classical…
Artificial intelligence assisted mathematical proof has become a highly focused area nowadays. One key problem in this field is to generate formal mathematical proofs from natural language proofs. Due to historical reasons, the formal proof…
We introduce a logic for reasoning about evidence, that essentially views evidence as a function from prior beliefs (before making an observation) to posterior beliefs (after making the observation). We provide a sound and complete…
Interpretability is the study of explaining models in understandable terms to humans. At present, interpretability is divided into two paradigms: the intrinsic paradigm, which believes that only models designed to be explained can be…
This essay explores the impact of automated proof construction on three key areas of mathematical cognition: on how we judge the role one piece of mathematics plays in another, on how we make mistakes in reasoning about mathematical…
A significant amount of research has considered mathematical proofs, the students who learn them, and the instructors that teach them, from a variety of perspectives. This paper considers this topic from four main perspectives: students'…
We consider the problem of automated reasoning about dynamically manipulated data structures. The state-of-the-art methods are limited to the unfold-and-match (U+M) paradigm, where predicates are transformed via (un)folding operations…
The belief revision field is opulent in new proposals and indigent in analyses of existing approaches. Much work hinge on postulates, employed as syntactic characterizations: some revision mechanism is equivalent to some properties.…
Analogy has received attention as a form of inductive reasoning in the empirical sciences. However, its role in pure mathematics has received less consideration. This paper provides an account of how an analogy with a more familiar…
Formal logic has often been seen as uniquely placed to analyze mathematical argumentation. While formal logic is certainly necessary for a complete understanding of mathematical practice, it is not sufficient. Important aspects of…