Abstract: What are the "simplest" 3-manifolds? What are the "simplest" knots? One common answer is those with least hyperbolic volume. We will give a gentle introduction to hyperbolic geometry and mention some of the key questions in the field. Finally, we will discuss recent algorithmic answers to some of these questions. 

Abstract: Open books are natural generalizations of fibred knots to any dimension. Quinn showed that in all dimensions greater or equal to 5 open book structures exist if and only if an algebraic-topological obstruction, the so called asymmetric signature, vanishes. This invariant always vanishes in odd dimensions and is potentially non-trivial in even dimensions. The question of the existence in dimension 4 is still unsolved. While it is clear that the asymmetric signature remains an obstruction for the existence of an open book structure even in dimension 4, it is obvious that Quinns techniques to proof the existence break down. Together with Marc Kegel we analysed what can be salvaged and show that an open book with connected binding on S^3, i.e. a fibred knot, extends up to stabilisation to D^4 provided that the Seifert form has a Lagrangian. This is the first step in proving the existence of open books in dimension 4. On the other hand recent work by Kastenholz shows that there is no open book structure on the cartesian product of two hyperbolic surfaces, while the asymmetric signature of this space vanishes. So, like many other things, the story in dimension 4 remains mysterious.  

Abstract: A laser beam can be described by a complex-valued function that satisfies a certain differential equation. The zeros of these functions form curves in 3-dimensional space that can be knotted or linked: so-called optical vortex knots. In this talk, I will present a construction that creates for a given knot type a corresponding solution to the differential equation. The construction is based on braids and topological properties of complex polynomials.

Abstract: I will give a short introduction into Lean 4 - a proof assistant - and provide an overview of dependent type theory, which underlies its verification capabilities.  Apart from automatically verifying proofs, Lean allows mathematical work to be divided into small, verifiable components, making collaborative research more efficient. To support this process, we are developing tools that assist with proof translation, organization of formalized results, and workflow management. AI may be one component of these tools, helping to automate and streamline certain tasks.

I will also present an idea of a project to formalise knot theory in the smooth category in Lean 4. The theory of smooth knots seems to be particularly suited goal, since it will require to formalise fundamental theorems from differential topology and differential geometry.