Formalize!(?) - 2

Schedule

15:15 - 15:30 Introduction
15:30 - 16:00 Talk 1: Anna Steensen - Formal text: a semiotic perspective. The case of the ‘Combinatorial School’
16:00 - 16:30 Talk 2: Dominik Kirst - A Feasible Formalization of Incompleteness
16:30 - 17:00 Break
17:00 - 17:30 Talk 3: Deniz Sarikaya - Frames for Mathematical Texts Friday (jww : Bernhard Fisseni, Bernhard Schröder)
17:30 - 18:00 Talk 4: Bernhard Schröder - Meaning and beyond - considerations on the semantics and pragmatics of mathematical frames
18:00 - 18:30 Break
18:30 - 19:00 Talk 5: Merlin Carl - Sociomathematical Norms and Automated Proof Checking in Math Education - Reflections and Experiences
19:00 - 19:15 closing
19:15 - 20:00 The room will stay open for unofficial discussion

CHANGES:

17:00 - 17:30 Postponed (hopefully for formalize 3) : ̵Talk 3: Bernhard Fisseni - Framing mathematical meaning – considerations on structuring mathematical language and proofs
19:00 - 19:30 Postponed (hopefully for formalize 3) : ̵ ̵T̵a̵l̵k̵ ̵6̵:̵ ̵ ̵ ̵G̵i̵s̵e̵l̵e̵ ̵S̵e̵c̵c̵o̵ ̵-̵ ̵F̵r̵o̵m̵ ̵C̵o̵m̵p̵u̵t̵e̵r̵s̵ ̵t̵o̵ ̵D̵i̵a̵g̵r̵a̵m̵s̵ ̵a̵n̵d̵ ̵B̵a̵c̵k̵:̵ ̵n̵o̵t̵e̵s̵ ̵o̵n̵ ̵t̵h̵e̵ ̵F̵o̵u̵r̵-̵C̵o̵l̵o̵r̵ ̵T̵h̵e̵o̵r̵e̵m̵
1̵9̵:̵3̵0̵ ̵-̵ ̵1̵9̵;̵4̵5̵ C̵l̵o̵s̵i̵n̵g̵
̵1̵9̵:̵4̵5̵ ̵-̵ ̵2̵1̵:̵0̵0̵ ̵ ̵ ̵ ̵ ̵ ̵T̵h̵e̵ ̵r̵o̵o̵m̵ ̵w̵i̵l̵l̵ ̵s̵t̵a̵y̵ ̵o̵p̵e̵n̵ ̵f̵o̵r̵ ̵u̵n̵o̵f̵f̵i̵c̵i̵a̵l̵ ̵d̵i̵s̵c̵u̵s̵s̵i̵o̵n̵.̵ ̵

Abstracts (in alphabetical order of the authors):

Sociomathematical Norms and Automated Proof Checking in Math Education - Reflections and Experiences

Merlin Carl

According to a widely held view, mathematical proofs are essentially (indications of) formal derivations, and thus in principle mechanically checkable. This should in particular hold for the kind of simple proof exercises typically given to beginner students of mathematics. If that is so, then automated proof checking should be an attractive option for math education at the beginner's level.

An opposing view would be that mathematical proofs are social objects and that what constitutes a mathematical proof can thus not be separated from the social context in which it arises. In particular, such "sociomathematical norms" play a role in teaching situations, see, e.g., [Stephan].

Indeed, the standards for what constitutes an acceptable proof may change quite quickly in educational situation: What needs to be justified in week 1 may simply be taken for granted in week 4 (and even vice versa).

In automated proof checkers, such standards are hard to implement, not only because they are subject to rapid change, but also because they are a subject of constant negotiation (see, e.g., again [Stephan]).

There thus seems to be a tension between the inherent social nature of "natural" mathematical proofs and attempts at their automated verification.

In this talk, we will explore this tension both theoretically and on the basis of our experiences with developing the Diproche system, a program for the automated verification of natural language proof in beginner's introduction to proof classes (modelled after the example of the Naproche system by Cramer, Koepke et al.) and its use at the Europa-Universität Flensburg during the winter term 2020/2021.

[Stephan] M. Stephan: "Sociomathematical Norms in Mathematics Education".

***

A Feasible Formalization of Incompleteness

Dominik Kirst

Spelled out in full detail, the standard proof of the incompleteness of, say, Peano arithmetic following Gödel is notoriously technical and therefore tricky to formalize in a proof assistant. However, there is also the well-known approach to incompleteness via undecidability (anticipated by Post and formally noted by Kleene), which can be feasibly implemented in the constructive type theory underlying the Coq proof assistant, using ideas from synthetic computability. I will give a quick but self-contained demo of an abstract version of this proof outline and, if time allows, show its instantiation to a first-order axiomatisation of Peano arithmetic.

***

Frames for Mathematical Texts
Deniz Sarikaya

We discuss the concept of frames with respect to mathematical texts. The concept of frames has been developed in the context of Artificial Intelligence since the 1970s, but recently also in linguistics and philosophy. We defend the following theses:

1. Frames can be used to model both (textual) structural properties of proofs and ontological aspects of mathematical knowledge, and to relate both aspects of proof understanding.

2. Specifically, using frames it is possible to model how mathematicians understand proofs texts where patterns have not been executed in a fully explicit way.

3. The inheritance hierarchy of frames allows, among others, to represent generalization and creative application of proof methods.

This is joint work with Bernhard Fisseni and Bernhard Schröder.

Meaning and beyond - considerations on the semantics and pragmatics of mathematical frames

Bernhard Schröder

We use the concept of frames from AI, cognitive science and linguistics to model stereotypical knowledge of mathematicians about proof structures and mathematical objects and relations which guides them to decode the intended interpretation of proof texts. Frames are triggered by linguistic constructions and semantic structures. They can be regarded as expectations regarding components or actants in a certain proof step. In my talk I will argue that there are two kinds of expectations triggered by frames: strict expectations regarding components or actants which are semantically required and „soft" pragmatic hints regarding the intended embedding of some proof part in the proof context.

***

From Computers to Diagrams and Back: notes on the Four-Color Theorem

Gisele Secco

Since its sensational popularization at the end of the 1970s, the computer-assisted proof of the Four-Color Theorem (4CT) has been the subject of innumerable debates – among mathematicians, computer scientists and philosophers. Within philosophical investigations, whenever the use of computers in mathematical practice is considered, the 4CT proof is mentioned. Philosophical discussion of the proof has centred mainly on Tymoczko’s argument for the introduction of experimentation in mathematics via 4CT – notably made in (Tymoczko 1979). (See Johannsen & Misfeldt 2016 for a recent version of this position.) Given the plethora of philosophical commentary on this famous result, it is reasonable to ask why and in which ways the case might still engender relevant philosophical reflections. In my communication I will argue for the pertinence of Appel and Haken’s solution for the Four-Color problem as a case study in the philosophy of mathematical practice, showing evidence for considering the 4CT proof as an exemplary case of the indispensability of diagrams in contemporary mathematical practices.

***

Formal text: a semiotic perspective. The case of the ‘Combinatorial School’

Anna Steensen

With starting point in the intuition that formal mathematical practices have to do with agents following rules and manipulating textual expressions without interpreting them, and using a 1800-paper by Rothe of the so-called ‘Combinatorial School’ as example, I suggest a way to use structuralist semiotic analysis to understand how ‘formal text’ emerges when an agent is reading mathematical text. With this approach, I wish to explore on the one hand how we can use the current syntax-semantics distinction as an analytical tool for describing and comparing specific mathematical textual practices, on the other how a semiotically informed analysis of text can offer a perspective that compliments historical, philosophical and logical-mathematical perspectives on formalization.