Analysis Seminar

Christoph ThieleUniversity of Bonn
On the foundations of anaylsis

Monday, March 5, 2018 - 2:30pm
Malott 406

Abstract: We develop from scratch a formal code that can be used to express analysis or mathematics. Such code could be used as basis for automated proof checking, or it can be used as a reference by mathematicians who want to understand or teach the basic principles of mathematics. Our design of the code serves the following goals: it aims to be minimal, it aims to be close to mathematicians' way of thinking, and it aims to be comparable to the Zermelo Fraenkel Choice system. We share some of the insights and surprises that the exercise of designing this code has triggered.