### Saturday - **January 15**, 2021

# Formalize!(?) - 2

### A philosophical & educational perspective on

formalization in mathematics

### Zurich / Online

15:15 - 19:45 (CET / UTC+1)

## A one-day Zoom Workshop

You can register via this google form. If you do not want to use a google form, please write an email to the contact listed below.

If you have any problem with the registration write an email to: jose.perez (at) gess.ethz.ch with your name and affiliation to get the zoom link.

This is the second iteration of Formalize. This was the first iteration,

The participants are listed here.

What are the chances and problems of the act of formalization in the context of mathematics? It is often said, that all of mathematics can be reduced to first-order logic and set theory. The derivation indicator view says that all proofs stand in some relation to a derivation, i.e. a mechanically checkable syntactical objects following fixed rules, that would not have any gaps. For a long time this was a mere hope. There may have been proofs of concepts from early logicists but derivation never played a big role in mathematical practice. The modern computer might change this. Interactive and automated theorem provers promise to make the construction of a justification without any gaps feasible for complex mathematics.

Is this promise justified? Will the future of mathematical practice shift to more formal mathematics? Should it? We hope to illuminate such questions and focus especially on what these developments mean for the future of the curriculum of university students.

This event features speakers speaking about both concrete projects and reflections on such endeavours in general.

## Speaker

(Europa Universität Flensburg)

Bernhard Fisseni

(University Duisburg-Essen)

Dominik Kirst

(Saarland University)

Gisele Secco

(Universidade Federal de Santa Maria)

Bernhard Schröder

(Universität Duisburg-Essen)

Anna Steensen

(ETH Zurich)

## Schedule

**15:15 - 15:30 Introduction**

**1**

**5**

**:**

**3**

**0 - 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**

**1**

**6**

**:30 - 1**

**7**

**:0**

**0**

**Break**

**1**

**7: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 - S

18:00 - 18:30 Break

18:30 - 19:00 Talk 5: Merlin Carl - S

**ociomathematical Norms and Automated Proof Checking in Math Education - Reflections and Experiences**

19:00 - 19:1

19:00 - 19:1

**5**

**closing**

19:15 - 20:00 The room will stay open for unofficial discussion

19:15 - 20:00 The room will stay open for unofficial discussion

**CHANGES:**

**1****7: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:

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.

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

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.

## Due to the global pandemic we will meet online and

unfortunately not in Zurich

unfortunately not in Zurich