Geodesic flow and decay of traces on hyperbolic surfaces

• Speaker: Antoine Gansemer

We will attempt to give an accessible, graduate level exposition of some recent work in a preprint on the “decay of traces on a hyperbolic surface under geodesic flow”.  We will motivate the spectral theoretical problem with visuals provided, we will give some ideas on the tools used including pseudodifferential operators on hyperbolic surfaces and decay of correlations estimates for hyperbolic dynamical systems.

Perturbations and the motion of the Earth

• Speaker: Nicholas Bohlsen

Historically, the problem of calculating the motion of the planets in the solar system using Newtonian physics was one of great mathematical interest. Its study led to the development of numerous mathematical tools such as chaos theory but also topology itself, through Poincare for whom it was a motivating problem. In this talk I will introduce the Canonical Perturbation Theory which allows us to approximate the orbits of Hamiltonian dynamical systems which are close to integrable (exactly-solvable) systems. I will then demonstrate the use of this theory to solve for the motion of the Earth around the sun under the perturbation from Jupiter's gravity.

The classical Hawking-Penrose singularity theorem

• Speaker: Qiyu Zhou

Abstract: One of the most important predictions of the general theory of relativity (GR) is that the physical spacetime admits at least one singularity. There are three singularity theorems proven by Stephen Hawking and Roger Penrose, one of which is known as the classical Hawking-Penrose singularity theorem. It has general and physically reasonable conditions imposed on the spacetime and predicts different types of singularities, including "black hole" and "big bang" singularities. In this talk, we discuss the classical Hawking-Penrose singularity theorem.

An Introduction to the Lean Theorem Prover

• Speaker: Lucas Allen

Lean 4 is a powerful theorem prover/programming language based on dependent type theory and the calculus of inductive constructions. In this talk we will give an extremely brief introduction to what Lean is and why it is useful before moving on to a demonstration involving some actual theorem proving. If time permits, we'll also look at some basic programming functionality.