# Naproche - Seminar on Formal Mathematics 2007

Organized by Peter Koepke, Grigori Mints, and Bernhard Schröder.

**Thursday, March 22, 10:00-12:00**, MPI (joint session with the Trimestre on
Methods of Proof Theory in Mathematics):

**Peter Koepke**, The Language of Proofs
(Slides)

Abstract:
*Proof theory treats mathematical proofs as formal proofs which proceed by
syntactic manipulations of sequences of symbols. To the human reader proofs
rather appear as tales about numbers, figures and other mathematical objects.
We discuss whether standard linguistic techniques for the understanding of
simple discourse are able to generate formal proofs from natural language
proofs. This work may lead to natural interfaces for proof-checkers and
provers and to a better understanding of the natural language and logic
used in mathematical discourse. See also
http://www.math.uni-bonn.de/people/naproche*

**Wednesday, March 28 17:00-19:00**, MPI:

Technical Discussion of Naproche

**Tuesday, April 3, 13:00-15:00**, MPI:

**Grigori Mints, Stanford**,
Advanced tools in computerized logic education

Abstract: *An overview of computerized exercises developed for teaching
definability and related notions in a course of first order logic at
Stanford University*

**Tuesday, April 10, 13:00-15:00**, MPI:

**Bernhard Schröder**,
Dynamic aspects of the semantics of semi-formal proofs

Abstract:
*Like everyday language the language of semi-formal proofs exhibits a lot
of phenomena, as e.g. anaphora and the interaction of quantifying
expressions and implications, which can best be described in the
framework of dynamic semantics. The talk will give a brief overview over
dynamic-semantic approaches like Discourse Representation Theory (DRT)
and Dynamic Predicate Logic (DPL), their motivation, and their basis in
dynamic logic. Some dynamic-semantic phenomena are quite rare in
everyday language, but pervasive in mathematics, like hypothetical
propositions. Others, as the interaction of quantifying and anaphorical
expressions with variables and other formal means of notation, are
rather uniquely used in mathematics. Therefore, so far, natural language
semantics has neglected them widely. The talk will try to fill parts of
this gap.*

**Tuesday, April 17, 13:00-15:00**, MPI:

**Freek Wiedijk, Nijmegen**, Readable formalization of mathematics.

**Tuesday, April 24, 13:00-15:00**, MPI:

**Jesse Alama, Stanford**,
Formalizing Euler's Polyhedron Formula

Abstract: *I describe a project to formalize Euler's polyhedron formula
(in the three-dimensional genus 0 form "V-E+F=2") in the MIZAR
proof-checking system. I discuss in detail the particular proof of
Euler's formula that is being formalized, the progress that has been
made so far, what obstacles have been encountered, and what remains to
be done. I will also get in to the underlying motivations for such a
project, which are to evaluate the role of computer-checked formal
proofs in contemporary mathematical practice and to find a place for
them in the philosophy of mathematics.*

**Tuesday, May 15, 13:00-15:00**, MPI:

**Fritz Hamm, Stuttgart**
A computational semantics for nominalizations

Abstract:*
The talk introduces an event calculus originally developed by M. Shanahan
for high level control of mobile robots. It is argued that a combination
of the event calculus with one of Feferman's type free systems allows for
a formalization of the notion *reification*.
The combined system will be used to develop an empirically
adequate computational semantic theory of nominalisations. If time
allows relationships of the proposed theory to Discourse
Representation Theory will be discussed.*

**Tuesday, May 22, 13:00-15:00**, MPI:

**Henk Barendregt, Nijmegen**,
Reflection in and on proof-assistants

Abstract:*
The technical notion of reflection, first employed explicitly by Gödel,
denotes doing mathematics via metamathematics. It is quite useful, even
indispensable, in formal mathematics.
Nevertheless the goal of having a proof-assistant that makes formalizing an informal
proof as easy as writing the informal argument in latex is still not reached.
A view is given on the difficulties encountered. Some proposals are made
for an interactive proof language.
*