Johan Commelin (Utrecht University)

Mathlib:  a look behind the curtain of the digital Bourbaki 2.0

The mathlib library is a community effort to formalize a large body of mathematics in the Lean theorem prover. It can be viewed as a crowd-sourced experiment in mathematical knowledge management. In this talk I will give a brief introduction to Lean, and then I will explain how mathlib is organized.

I will give an overview of the current mathematical content of the library. We will also take a look a some of the social aspects of the project, and give some insights into the design choices that were made, and the trade-offs that were involved.

Mireille Boutin (Eindhoven University of Technology)

Algebraic Problems in Localization and Mapping Applications

Localization is the task of determining one’s location in their environment. Mapping is the task of determining the shape and location of the objects in one’s environment. Either task can be accomplished using various types of sensors, for example cameras or Lidar.  In this talk I will talk about two localization problems (global positioning —GPS — and gun shot localization) and one mapping problem (hearing the shape of a room). I will show how these problems relate to algebra and highlight some new results and their practical implications. This is joint work with Gregor Kemper.