-> Here you can find a live-blog by Ulrik Buchholtz, following the talks at the FOMUS meeting (facebook login required).

**FOMUS: Foundations of Mathematics: Univalent Foundations and Set Theory -**

*What are Suitable Criteria for the Foundations of Mathematics?*The FOMUS workshop was held at the Center for Interdisciplinary Research of Bielefeld University from the 18th to the 23rd of July. Within this framework approximately 80 graduate students, junior researchers and leading experts gathered in order to investigate and discuss suitable foundations for mathematics and their qualifying criteria, with an emphasis on HoTT/Univalent Foundations and set theory. This interdisciplinary workshop, designed as a hybrid between summer school and research conference, was aimed at students and researchers from the fields of mathematics, philosophy and computer science.

Zermelo-Fraenkel axioms are widely assumed to be the foundation of mathematics within the mathematical practice of set theory. However, an increasing number of researchers are currently working on the

The workshop was opened with an introduction to these two different foundational theories, with an emphasis on the less popular homotopy type theory, and then progressed into indepth panel discussions and (research) talks. With regard to the philosophical discipline of mathematics, the formal requirements of the foundations of mathematics, their limitations and their naturality were examined. Recently, it has become increasingly important to formalise mathematics by computer-aided formal proof systems, such as Coq. With this in mind, it was investigated which foundation is most suitable for the changing needs of mathematical practice.

This workshop can be seen as the continuation of the event on Formal Mathematics, held at the University of Bonn in March 2015.

The poster for the workshop can be downloaded here.

Organisers: Balthasar Grabmayr, Deborah Kant, Lukas Kühne, Deniz Sarikaya, Mira Viehstädt

This workshop was organised with the generous support of the Association for Symbolic Logic (ASL), the Association of German Mathematicians (DMV), the Berlin Mathematical School (BMS), the Center of Interdisciplinary Research (ZiF), the

*Univalent Foundations*as an alternative foundation of mathematics. This relatively young approach is based on*Homotopy Type Theory*, which is a link between Martin Löf's intuitionistic type theory and the homotopy theory from topology.The workshop was opened with an introduction to these two different foundational theories, with an emphasis on the less popular homotopy type theory, and then progressed into indepth panel discussions and (research) talks. With regard to the philosophical discipline of mathematics, the formal requirements of the foundations of mathematics, their limitations and their naturality were examined. Recently, it has become increasingly important to formalise mathematics by computer-aided formal proof systems, such as Coq. With this in mind, it was investigated which foundation is most suitable for the changing needs of mathematical practice.

This workshop can be seen as the continuation of the event on Formal Mathematics, held at the University of Bonn in March 2015.

The poster for the workshop can be downloaded here.

Organisers: Balthasar Grabmayr, Deborah Kant, Lukas Kühne, Deniz Sarikaya, Mira Viehstädt

This workshop was organised with the generous support of the Association for Symbolic Logic (ASL), the Association of German Mathematicians (DMV), the Berlin Mathematical School (BMS), the Center of Interdisciplinary Research (ZiF), the

*Deutsche Vereinigung für Mathematische Logik und für Grundlagenforschung der Exakten Wissenschaften*(DVMLG), the German Academic Merit Foundation (*Stipendiaten machen Programm*), the*Fachbereich Grundlagen der Informatik*of the German Informatics Society (GI) and the German Society for Analytic Philosophy (GAP).