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: (GMT-06:00) Saskatchewan, Central America change

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