Aktuelles & Events

Lean is a proof assistant which has a large mathematical library containing results from most areas of mathematics. It contains a good foundation to verify current research problems in various areas of mathematics, and enables new collaborative projects. In this talk, I will give an overview of Lean and its mathematical library Mathlib, and describe some of the exciting formalization projects in this area. In particular, I will describe a recently finished project formalizing a generalization of Carleson's 1966 theorem in harmonic analysis, about the pointwise convergence of Fourier series. This is a major result in harmonic analysis with a difficult proof, and this result has been fully verified in Lean. The formalization was a large collaborative project with 13 main contributors.

I will present recent advances in applying AI-based methods to interpret genetic sequences, with a particular focus on identifying disease-causing mutations. In addition, I will share insights from establishing GHGA—the German Human Genome-Phenome Archive—an NFDI initiative dedicated to the secure sharing of human genomic data for secondary research.

In this talk we are going to compare two approaches (quenched and annealed) for obtaining invariant measures in open random dynamical systems. The quenched approach employs thermodynamic formalism techniques applied to a weighted transfer operator, constructing conditionally invariant measures for each fiber of the system and deriving a corresponding fiberwise limit invariant measure. On the other hand, the annealed approach relies on spectral analysis of the stochastic Koopman operator to derive a state-space invariant measure for the open system. We focus on establishing a correspondence theorem linking the results of both methods and introducing an annealed framework for a weighted transfer operator on the state space through which one can obtain an invariant measure that is absolutely continuous with respect to the conformal measure of the open system. We lastly discuss large deviation principles for the empirical measures of the killed process under both the annealed Koopman and weighted transfer operators, highlighting the role of spectral gaps in determining fluctuation behavior.

Nonlinear acoustic phenomena are highly relevant in many applications, from medical imaging to industrial cleaning. This talk first provides an overview of how the modeling equations arise from fundamental physical principles, such as the Navier–Stokes equations, and how standard models can be extended, for example, by incorporating fractional damping due to viscoelasticity. Then, while second-order wave equations are standard, we focus on a first-order-in-time formulation and highlight key aspects of a proof of existence and uniqueness of solutions in suitable Sobolev spaces.