talks

Proof assistants like Lean 4 are often described as machines that verify proofs. While that description is true, it misses a central aspect: what makes Lean usable is a logical calculus rich enough to tell the user, at every line, what has been constructed so far and what remains to be constructed. From the perspective of a mathematician, I will discuss why proof assistants are built on dependent type theory rather than first-order logic, and what it is like to write and read a proof under these conditions.

The central claim is that proving with a tool like Lean 4 is not one activity but three:

• the direct practice of closing a goal;
• the upward practice of engineering a proof into an ecosystem, making it usable for a community with its conventions, expectations, and shared abstractions;
• the downward practice of confirming that the formal theorem means what one intended, which draws in questions of consistency, semantics, implementation, and translation between foundations.

Each of these has its own notion of what it means for a proof to be surveyable, and they do not always agree. I will illustrate this with short live examples, with recent cases in which a machine-checked proof turned out to prove less than it appeared to, or nothing at all, and with the current debate about AI-generated proofs, in which all three practices are under pressure at once.

This is joint work with T. Jäger and C. Liu. We study the multivariate notions of diam-mean m-equicontinuity and the corresponding dual notion of diam-mean m-sensitivity for m>1. To formalise this duality, we establish an Auslander-Yorke type dichotomy: every minimal system is either diam-mean m-equicontinuous or diam-mean m-sensitive. The main focus of the talk is a local characterisation of multivariate mean sensitivity in terms of weakly mean sensitive tuples. We show that, in transitive systems, diam-mean m-sensitivity is equivalent to the existence of an essential weakly mean sensitive m-tuple, thereby providing a local description of this global dynamical property.

In this talk, I discuss a recent work in which we introduce and investigate multivariate versions of frequent stability and diam-mean equicontinuity called “frequent m-stability” and “diam-mean m-equicontinuity”, where m > 1 is a natural number. Systems whose factor map to the maximal equicontinuous factor (MEF) is finite-to-one for a residual set — “almost finite-to-one extensions” — or a set of full measure — “almost surely finite-to-one extensions” — are characterised by multivariate frequent stability and multivariate diam-mean m-equicontinuity respectively. Assume that the acting group is second countable, locally compact and abelian. A minimal system is frequently $(m+1)$-stable if and only if it is an almost $m$-to-one extension of its MEF. Similarly, a minimal system is diam-mean $(m+1)$-equicontinuous if and only if it is an almost surely $m$-to-one extension of its MEF. In my talk I will present the proof and the methods used to explore this multivariate hierarchy.

Topological dynamical systems with measure theoretically discrete spectrum can be organized into a hierarchy. This is done by the invertibility properties of their continuous factor maps to their maximal equicontinuous factor (MEF). Many such invertibility properties correspond to equivalent intrinsic dynamical rigidity properties. One of those is mean equicontinuity, which can be described in various ways. Its corresponding invertibility property is that the continuous factor map to the MEF is measure theoretically an isomorphism. Outside of the hierarchy lie systems like the Thue-Morse subshift whose continuous factor map to the MEF is measure theoretically 2:1. Other examples of such a form are given by Iwanik and Lacroix or by Williams. They exhibit rich spectral properties such as a singularly continuous part of the spectrum and thus do not fall into the aforementioned hierarchy. Our aim is to extend the hierarchy to also handle m:1 extensions. In the past few years those classes of systems have been studied under the viewpoint of multivariate forms of mean sensitivity, as for example by Li, Ye, Yu (2021). We propose a notion of multivariate mean equicontinuity called mean m-equicontinuity, which satisfies an Auslander-Yorke type dichotomy to the aforementioned multivariate mean sensitivities. We call a continuous extension of another system that is measure theoretically m:1 an m:1-topomorphic extension and conjecture an equivalence between mean m-equicontinuity and being an m:1-topomorphic extension of the MEF. We prove that m:1-topomorphic extensions of equicontinuous systems are mean m-equicontinuous and provide some ideas for the converse direction. This is joint work with J. Breitenbücher and T. Jäger.

This is joint work with Tobias Jäger. Due to a result by Glasner and Downarowicz, it is known that a minimal system is mean equicontinuous if and only if it is an isomorphic extension of its maximal equicontinuous factor (MEF). The majority of well-known examples of this type are in addition almost automorphic, that is, the factor map to the MEF is almost one-to-one. The only cases of isomorphic extensions which are not almost automorphic are again due to Glasner and Downarowicz, who in the same article construct such systems in a rather general and abstract setting. In this talk I present a construction using the Anosov-Katok method which provides an alternative way to produce such examples, and to obtain as a byproduct that these can be realised as smooth torus diffeomorphisms.

This talk will give an introduction to the method of studying a topological dynamical system via its so-called maximal equicontinuous factor. It is based on my master’s thesis, which provides a collective overview of the current state of knowledge. A topological dynamical system with continuous dependence of all states on the initial conditions is called equicontinuous. Equicontinuous dynamical systems are in many ways non-chaotic. For example, they have zero entropy. Further, minimal equicontinuous systems can be classified as rotations of compact groups. It is well-known that any (compact) topological dynamical system has an equicontinuous factor maximal among all equicontinuous factors. The invertibility properties as well as other regularity properties of the factor map onto this maximal equicontinuous factor (MEF) can tell us how far a system is away from the simple equicontinuous case. In fact, the literature offers a variety of equivalences between dynamical properties on the one hand and the invertibility properties of the factor map to the MEF on the other hand. Those invertibility properties can be put into a canonical hierarchy starting from homeomorphy. Via those aforementioned equivalences, a parallel hierarchy of dynamical properties starting with equicontinuity emerges. In the realm of measure preserving dynamics those with discrete spectrum are considered most simple. The well-known Halmos-von Neumann theorem states that for ergodic systems with discrete spectra the following holds:

1. Two ergodic systems with discrete spectrum are isomorphic if and only if their spectra coincide.
2. Any countable subgroup of the circle can be realized as a spectrum of an ergodic system with discrete spectrum.
3. Any ergodic system with discrete spectrum is isomorphic to a rotation on a compact group. Consider a topological dynamical system which has discrete spectrum if viewed as a measure preserving one. On the one hand the MEF of that system is topologically conjugate to a group rotation. On the other hand the system is measure theoretically isomorphic to a group rotation. Here we study the case in which both group rotations coincide. One can understand the aforementioned hierarchy as a description of the landscape of topological models of a measure preserving system with discrete spectrum.