← All papers
Formalising Sharkovsky's Theorem (Proof Pearl)
cs.LO
Jan 16, 2023 · v1
TL;DR
Formalizes Sharkovsky's theorem on periodic points of continuous real functions in Lean/mathlib.
Abstract
This paper presents a formalization of Sharkovsky's theorem in Lean and mathlib. Sharkovsky's theorem states that if a continuous function on the real line has a periodic point of period n, then it has periodic points of all periods that follow n in Sharkovsky's ordering. The formalization includes the full theorem and provides a clean proof structure suitable for inclusion in mathlib.
Problem
Sharkovsky's theorem, which characterizes the possible periods of continuous functions on the real line through a specific ordering, had not been formalized in a proof assistant suitable for inclusion in mathlib.
Approach
The authors formalize Sharkovsky's theorem in Lean using mathlib. The theorem states that if a continuous function on the real line has a periodic point of period n, then it has periodic points of all periods that follow n in Sharkovsky's ordering. The formalization provides a clean proof structure designed for inclusion in mathlib.
Results
The full Sharkovsky theorem is formalized in Lean with a proof structure suitable for mathlib inclusion.