Epistemic roles of diagrams in short proof (Henrik Kragh Sørensen & Mikkel Willum Johansen)
Recent case studies in the philosophy of mathematical practice have pointed out that certain types of diagrams play epistemic roles in mathematical proofs. To complement such case studies and provide a quantitative basis for further analysis and discussions, we undertake an empirical study based on a large and contemporary corpus of mathematical texts. Following an a priori assumption that diagrams in short proofs carry more epistemic warrant, we focus on 1- or 2-sentence proofs that refer to diagrams, and we build a corpus of such proofs from the arXiv.
Based on this corpus we analyze and develop a typology of such proofs in order to conduct selected qualitative close-readings of diagrams in their argumentative contexts. This leads us to discuss tensions between visual and syntactical aspects of diagrams that suggest that hybrid diagrams play distinct roles in mathematical practice.
Frames for Mathematical Texts (Bernhard Schröder, Bernhard Fisseni & Deniz Sarikaya)
The frame concept, developed in Artificial Intelligence, cognitive science and linguistics, has recently regained interest in philosophy and philosophy of science. There have also been attempts at modelling mathematical proofs using frames, starting from a distinction between structural frames, which capture expectations about proof methods as well as constituents of proofs and their relations, and ontological frames, which capture the mathematical structures and typical referring linguistic and formulaic expressions. We will illustrate two points about using frames to model mathematical proofs: First, how frames can be used to explain aspects of innovation in mathematics, e.g. the discovery of zero or the transfer between different subject areas. Secondly, how frame theory relates to concepts of understanding proofs, notably Avigad's (2008) theory.
Proofs = Programs (Thorsten Altenkirch)
I want to discuss the idea coming from intuitionistic type theory that propositions are types and hence proofs are programs. This is not only useful when teaching logic but it also is close to verbal explanations of theorems. I will demonstrate the agda system, an interactive theorem prover and also a programming language, to illustrate the concept.
Content from Expressions: Some Ideas for a Distributional Approach to Arithmetical Content (Juan Luis Gastaldi)
Recent applications of deep neural network techniques for data analysis to the field of mathematics suggest in various ways that semantic aspects of mathematical knowledge can be inferred from pure syntax. However, those results are as surprising as uninterpretable and uninformed by any philosophical or epistemological perspective. In this talk, I will start by providing a quick overview of the state of the art and its philosophical significance, including the renewed role of distributionalism in neural models. Drawing on this perspective, I will propose some ideas, based on empirical evidence, of how aspects of arithmetical content, such as recursive structure and total order, could be inferred through explicit and interpretable means from the distributional properties of a natural language corpus.
Frames and Proof-Comprehension Research (Hinrich Lorenzen, Michael Schmitz)
We introduce a contemporary perspective on the frame concept and assess its potential value to university level mathematics education. We present the somewhat dated applications of frame-related concepts in mathematics education (such as Schemeta, Scripts, Subjective Domains of Experience, and Microworlds) and argue that frames may help university educators boost students' ability to read and comprehend mathematical proofs. To stimulate and create a basis for future work on this topic, we develop several hypotheses about the role frames might play in proof-comprehension research. Moreover, we present some first data from a study on the relationship of proof-comprehension and frames conducted recently with about 90 students at the University of Flensburg.
Designing a Proof-Frame Library for the Linguistic Analysis of Mathematical Texts (Marcos Cramer)
Abstract: When interpreting mathematical proof texts, mathematicians make use of knowledge that they have acquired about various proof methods. Based on this background knowledge, they have expectations about the structure of proofs that help them fill in gaps left by the author. The goal of our work is to formalize this background knowledge using the frame formalism that was first proposed for AI research by Marvin Minsky in 1974 and has found many applications in linguistics. A proof frame captures the background knowledge that mathematicians have about a given proof method, including knowledge about the common linguistic realizations used when the proof method is applied in practice. In this talk I report on preliminary results concerning the goal to construct a library of common proof frames. This library codes proof frames as feature structures according to the standards set out by the Text Encoding Initiative.
Open Texture, Rigor, and Proof (Benjamin Zayton)
Open texture is a kind of semantic indeterminacy first systematically studied by Waismann. In this paper, extant definitions of open texture will be compared and contrasted, with a view towards the consequences of open-textured concepts in mathematics. It has been suggested that these would threaten the traditional virtues of proof, primarily the certainty bestowed by proof-possession, and this suggestion will be critically investigated using recent work on informal proof. It will be argued that informal proofs have virtues that mitigate the danger posed by open texture. Moreover, it will be argued that while rigor in the guise of formalisation and axiomatisation might banish open texture from mathematical theories through implicit definition, it can do so only at the cost of restricting the tamed concepts in certain ways.