Computer-assisted proofs, proof assistants and visualization in dynamical systems - 19 giugno 2024

The scope of this workshop is to foster interactions between researchers working in the field of dynamical systems and ergodic theory, and who use, or want to use, rigorous computational methods. We want to deal with three different, complementary aspects: computer-assisted proofs, formal verification of proofs (proof assistants), and visualization tools. If the last aspect has a long history and was at the origin of important discoveries, computer-assisted proofs are much less developed, whereas the use of proof assistants is in its infancy. The workshop “Statistical and Computational Aspects of Dynamics” held in 2022 at the Centro de Giorgi has some aspects in common with the present one, but the project proposed here is significantly different because of the theme of proof assistants.

Oscar Bandtlow, Explicit resolvent bounds for transfer operators 00:00
Mark Pollicott, Estimates on Lyapunov exponents via the pressure function 57:34
Jerome Buzzi, Computing and visualizing measures with maximum entropy and other equilibrium states 1:58:18