Where: Essen, Germany & Online (Zoom), all talks are streamed online

When: September 7 & 8, 2022

What: TDPhiMa3

Please register here. 

TDPhiMa is a conference series that looks at mathematical texts from a philosophical and linguistic perspective. Text is a crucial medium for the dissemination of mathematical ideas, agendas, and results to the scientific community and educational contexts. This makes focusing on mathematical texts a natural and significant part of the philosophical study of mathematics. In addition, research on mathematical texts can benefit from the knowledge and methods of other disciplines such as linguistics and computer science to study problems in the philosophy of mathematics.

In the third iteration of TDPhiMa, we focus on the application of these methods within computational mathematics, including the context of automated theorem proving. Relevant topics include:

1. Big data approaches.

2. Input language for automated theorem provers

3. Language processing for evidence texts

4. Frame Semantics and other tools from classical AI.

5. Philosophical implications of the aforementioned topics 

The first two iteration were:

https://www.uni-due.de/tdphima2/ (2021, Essen / Online)

https://tdphima.weebly.com/ (2019, Prague)

Organizitation by: Bernhard Fisseni, Juan Luis Gastaldi, Deborah Kant, Deniz Sarikaya and Bernhard Schröder

Thorsten Altenkirch, University of Nottingham

Marcos Cramer, Technische Universität Dresden

Bernhard Fisseni, Universität  Duisburg-Essen 

Juan Luis Gastaldi, ETH Zurich 

Mikkel Willum Johansen, Københavns Universitet 

Hinrich Lorenzen, Europa-Universität Flensburg

Deniz Sarikaya, CLPS, Vrije Universiteit Brussels

Michael Schmitz, Europa-Universität Flensburg

Bernhard Schröder, Universität Duisburg-Essen 

Henrik Kragh Sørensen, Københavns Universitet 

Benjamin Zayton, MCMP LMU Munich 

All times local Essen times (CET)

Wednesday, September 7, 2022

13:45 Opening

14:00 Talk 1: Mikkel Willum Johansen & Henrik Kragh Sørensen: Epistemic roles of diagrams in short proof 

14:45 Talk 2: Bernhard Schröder, Bernhard Fisseni & Deniz Sarikaya: Frames for Mathematical Texts

15:30 Break

16:00 Talk 3: Thorsten Altenkirch: Proofs = Programs
16:45 Talk 4: Juan Luis Gastaldi: Some Ideas for a Distributional Approach to Arithmetical Content

17:30 Discussion

ca. 19:00 Conference dinner

Thursday, September 8, 2022

09:00 Talk 5 Michael Schmitz and Hinrich Lorenzen: Frames and Proof-Comprehension Research

09:45 Talk 6: Marcos Cramer: Designing a Proof-Frame Library for the Linguistic Analysis of Mathematical Texts 

10:30 Break

11:00 Talk 7: Benjamin Zayton: Open Texture, Rigor, and Proof

11:45 Discussion

12:45/13:00 End

== Wednesday

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.

== Thursday

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.

The even is possible due to the generous support of: 

Turing Center of ETH Zürich, the Universität Duisburg-Essen, the Marie Skłodowska-Curie Individual Fellowship, H2020-MSCA-IF-2018, the Deutsche Vereinigung für mathematische Logik und für Grundlagenforschung der Exakten Wissenschaften.