Write a Blog >>
Tue 21 Jan 2020 16:50 - 17:12 at Maurepas - Formalized mathematics 2 Chair(s): Tobias Nipkow

The Poincaré-Bendixson theorem is a classical result in the study of (continuous) dynamical systems. Colloquially, it restricts the possible behaviors of planar dynamical systems: such systems cannot be chaotic. In practice, it is a useful tool for proving the existence of (limiting) periodic behavior in planar systems. The theorem is an interesting and challenging benchmark for formalized mathematics because proofs in the literature rely on geometric sketches and only hint at symmetric cases. It also requires a substantial background of mathematical theories, e.g., the Jordan curve theorem, real analysis, ordinary differential equations, and limiting (long-term) behavior of dynamical systems.

We present a proof of the theorem in Isabelle/HOL and highlight the main challenges, which include: i) combining large and independently developed mathematical libraries, namely the Jordan curve theorem and ordinary differential equations, ii) formalizing fundamental concepts for the study of dynamical systems, namely the α, ω-limit sets, and periodic orbits, iii) providing formally rigorous arguments for the geometric sketches paramount in the literature, and iv) managing the complexity of our formalization throughout the proof, e.g., appropriately handling symmetric cases.

Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change

16:50 - 17:56: Formalized mathematics 2CPP at Maurepas
Chair(s): Tobias NipkowTechnische Universität München
16:50 - 17:12
Talk
CPP
Fabian ImmlerCarnegie Mellon University, Yong Kiam TanCarnegie Mellon University, USA
DOI Pre-print Media Attached
17:12 - 17:34
Talk
CPP
Jesse Michael HanUniversity of Pittsburgh, Floris van DoornUniversity of Pittsburgh
DOI Pre-print Media Attached
17:34 - 17:56
Talk
CPP
DOI Pre-print Media Attached File Attached