Date: Wed. November 22, 2023
Event: FAU MoD Lecture Series (Special double session. November 2023)
Organized by: FAU MoD, Research Center for Mathematics of Data at Friedrich-Alexander-Universität Erlangen-Nürnberg (Germany)

First session: 13:45H

Prospects of formalized mathematics
Speaker: Prof. Dr. Michael Kohlhase
Affiliation: Friedrich-Alexander-Universität Erlangen-Nürnberg. Carnegie Mellon University

Abstract. In (informal) mathematics (pure and applied) a human studies rigorously represented objects or mathematical models of the real world, comes up with conjectures about their properties, proves or refutes them, submits them for review and finally publication in the academic literature. While it is commonly accepted that all of mathematics could be expressed and indeed developed in first-order logic based on (some axiomatic) set theory, this option is almost never executed in practice. Formalized mathematics aims to enable computer support of “doing mathematics” by representing objects, conjectures, proofs, and even publications in formal systems, usually expressive logical languages with machine-checkable proof calculi, and highly efficient algorithms for automating various aspects of “doing mathematics”. Highlights of formalized mathematics are – machine-checked proofs of major theorems like the Kepler Conjecture, – Feit/Thomson’s “odd order theorem”, or the four color theorem, – search engines for mathematical formulae, – synthesis and verification of computer algebra algorithms – multiple libraries of formalized and verified mathematics with more than 100.000 theorems/proofs each. This talk will give an overview over the issues and results and introduces some of the techniques.

Second session: 15:00H

Rigorous analysis and numerical implementation of nudging data assimilation algorithms
Speaker: Prof. Dr. Edriss S. Titi
Affiliation: University of Cambridge. Texas A&M University. Weizmann Institute of Science

Abstract. In this talk, I will introduce downscaling data assimilation algorithms for weather and climate prediction based on discrete coarse spatial scale measurements of the state variables (or only part of them, depending on the underlying model). The algorithm is based on linear nudging of the coarse spatial scales in the algorithm’s solution toward the observed measurements of the coarse spatial scales of the unknown reference solution. The algorithm’s solution can be initialized arbitrarily and is shown to converge at an exponential rate toward the exact unknown reference solution. This indicates that the dynamics of the algorithm is globally stable (not chaotic) unlike the dynamics of the model that governs the unknown reference solution. Capitalizing on this fact, I will also demonstrate uniform in time error estimates of the numerical discretization of these algorithms, which makes them reliable upon implementation computationally. Furthermore, I will also present a recent improvement of this algorithm by employing nonlinear nudging, which yields a super exponential convergence rate toward the unknown exact reference solution.

You can find more details of these FAU MoD lectures at:

https://mod.fau.eu/fau-mod-lecture-series-special-november-2023/