### Saturday - **January 16**, 2021

# Formalize!(?)

### A philosophical & educational perspective on

formalization in mathematics

### Zurich / Online

15:50 - 20:00 (CET / UTC+1)

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.

## Speakers

Imperial College London

CLE- Unicamp

Freie Universität Berlin

Mathematics Education Centre at Loughborough University

### Adrian De Lon

Universität Bonn

Universität Bonn

Universität Bonn

ETH Zurich

Mathematics Education Centre at Loughborough University

University of East Anglia

## Schedule

**15:50 - 16:00 Introduction16:00 - 16:30 Talk 1: David Fuenmayor & Walter Carnielli: Gödelian flowers in exotic fields: automating (meta-)mathematical reasoning for non-classical logics**

**16:30 - 17:00 Talk 2: Anna Steensen: A semiotic perspective on the distinction of syntax and semantics in mathematical practice ***

(will be held later, you can still join, write us an email)

(will be held later, you can still join, write us an email)

**17:00 - 17:30 Talk 3: Peter Koepke: Formalize, Naturally!**

17:30 - 18:00 Naproche Tutorial: Adrian De Lon, Peter Koepke and Anton Lorenzen (Optional) // Break

18:00 - 18:30 Break

18:30 - 19:00 Talk 4: Fenner Stanley Tanswell: Rigour and Formalisability

19:00 - 19:30 Talk 5: Kevin Buzzard: Teaching Mathematicians the New Way

19:30 - 20:00 Talk 6: Paola Iannone & Athina Thoma: Learning about proof with LEAN

20:00 - 21:00 The room will stay open for unofficial discussion.

17:30 - 18:00 Naproche Tutorial: Adrian De Lon, Peter Koepke and Anton Lorenzen (Optional) // Break

18:00 - 18:30 Break

18:30 - 19:00 Talk 4: Fenner Stanley Tanswell: Rigour and Formalisability

19:00 - 19:30 Talk 5: Kevin Buzzard: Teaching Mathematicians the New Way

19:30 - 20:00 Talk 6: Paola Iannone & Athina Thoma: Learning about proof with LEAN

20:00 - 21:00 The room will stay open for unofficial discussion.

## Abstracts:

**Kevin Buzzard: Teaching Mathematicians the New Way Abstract: **Why should mathematicians formalise mathematics in theorem provers? Because it's now not too difficult, and we have no idea what will happen once this becomes normal. But first, we have to teach them how to do it. I will talk about my efforts in this area.

**David Fuenmayor & Walter Carnielli: Gödelian flowers in exotic fields: automating (meta-)mathematical reasoning for non-classical logics**How is it possible to employ automated theorem provers and proof assistants for formalization and reasoning in non-classical logics? We will discuss the semantic embedding approach and use it to formalize the 'last mile' of the proof of Gödel's incompleteness theorems in Isabelle/HOL. We aim at motivating a discussion on the use of automated reasoning with non-classical logics for the formalization and interpretation of (meta-)mathematical results.

**Paola Iannone & Athina Thoma: Learning about proof with LEAN****Abstract:** Why using theorem provers in university instruction? What does one investigation about their use tells us in terms of students producing proofs? We will report on a study on the introduction of LEAN in one first year mathematics module and we will discuss benefits, uptake and (educational) future of this endeavour.

**Peter Koepke: Formalize, Naturally!Abstract: **I shall present a version of Euclid's proof of the infinitude of primes in the natural language proof assistant Naproche. Naproche can be understood as an implementation of the derivation indicator view of mathematical proofs: a perfectly natural proof text is transformed into a formal derivation in some proof calculus, using natural language processing, logical transformations and automatic theorem proving. In the subsequent short tutorial on Naproche I shall go into details of the Euclid formalization. The tutorial demonstrates the potential of natural formalizations: in a couple of years and after extensive further development work natural formalizations will become commonplace in mathematical research and teaching!

**Anna Steensen: A semiotic perspective on the distinction of syntax and semantics in mathematical practice**

There is a common intuition that from a semiotic point of view, formalization in mathematics has to do with introducing and performing transformations of some notation while ignoring meaning. However, studies of various historical mathematical practices have shown this intuition to be problematic both historically and historiographically. I will suggest an approach for analyzing formalization as semiotic process, which hopefully can lead to more nuanced descriptions of historical as well as contemporary mathematical practices.

**Fenner Stanley Tanswell: Rigour and FormalisabilityAbstract: **In this talk I will discuss the relationship between rigour and formalisability, especially focusing on whether informal proofs can be rigorous. I will argue that the concepts of rigour and formalisability don’t coincide for a number of reasons. Nonetheless, these reasons also tell us about why the process of formalising proofs is very useful for the mathematical community.

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

unfortunately not in Zurich

unfortunately not in Zurich