Prof. (em.) Dr. Peter Koepke

Axiomatic Set Theory, General Logic, and Formal Mathematics

Research profile

• Axiomatic set theory: determination of consistency strengths of infinitary combinatorial principles, using forcing and core models; determination of consistency strengths without assuming the axiom of choice, characterizations of large cardinal axioms by embeddings of models of set theory.
• Constructibility theory and ordinal computability theory: new fine structure theories for constructible models of set theory, with applications; generalized machines with tapes of arbitrary ordinal lengths or registers working on ordinal numbers.
• Descriptive set theory and infinitary games.
• Formal mathematics: the language of mathematics and designing a natural proof checking system Naproche with natural language interfaces, in collaboration with linguistics.

Teaching Winter 2026/27:
Praktikum Mathematische Logik (P2A1) and Practical Project in Mathematical Logic (P4A1)
Axiomatic Set Theory, with AI-Generated Formalizations

Lecturer Peter Koepke

Time and Place Tuesdays 16-18, Wednesdays 16-18, N 0.008

Contents

Under the impression of the latest breakthroughs in the formalization of Mathematics, enabled by frontier models in AI, I have modified the original course plans towards the exploration of autoformalizations in set theory

The practical project will focus on two themes: an introduction to Zermelo-Fraenkel set theory along previous Bonn lecture notes, and on formalizations of that exact theory in First-Order Logic and in the Naproche system with the help of ChatGPT and Claude.

The course will meet for four hours each week. Initially the larger part of our time will be devoted to lectures by me on set theory:

Sets are ubiquitous in modern mathematics. Structures are sets of objects with certain properties. Fundamental notions like numbers, relations, functions and sequences can be defined from sets. Set theory, together with formal logic, provides a universally accepted foundation for mathematics and also a theory of (mathematical) infinity. We will cover: the Zermelo-Fraenkel axioms; relations, functions, structures; ordinal numbers, induction, recursion, ordinal arithmetic; natural numbers; the axiom of choice and equivalent principles; cardinal numbers and cardinal arithmetic; infinitary combinatorics and possibly large cardinals.

Further lecture topics will be about Formal Mathematics. We will use first-order logic in a format adequate for automated proving by the provers EProver and Vampire, and also the Naproche system (Natural Language Proof Checker) which translates (a restricted) natural language mathematics into first-order proof tasks.

The practical part, which will increase along the course, will consist of hands-on introductions to automated theorem proving, manual formalizations, and the use of frontier AI systems for formalizations. Practical projects will be assigned and carried out on Naproche and autoformalizations.

Participants are supposed to have a reasonably powerful laptop which can run Isabelle. You can apply for a practical slot by email to koepke@math.uni-bonn.de. Please state your

– name, matriculation number, email address, subject, Bachelor or Master and study semester, completed logic modules, programming experience, and optional further information.

The practical project will be organized via email and appointment.

Contact

• Mathematisches Institut
  Rheinische Friedrich-Wilhelms-Universität Bonn
  Endenicher Allee 60
  D-53115 Bonn
  Germany
  
• E-mail: koepke [emailsymbol] math.uni-bonn.de
• Sprechstunden nach Vereinbarung per Email.