Formalising Sharkovsky's Theorem (Proof Pearl)

on YouTube ↗28m

" summary

Formalisation of Sharkovsky's theorem and its converse appears in the Lean theorem prover, giving a machine-checked characterization of which minimal periods continuous interval maps can have and a constructive family of examples. Proof uses the intermediate value theorem, a short fixed-point lemma, cycle↔orbit bookkeeping, a subtle double induction and a small gcd/divisibility lemma; awkward parts cost ~120–260 lines of code while a missing number‑theory fact takes 14 lines. The realization builds a tent map family parameterized to realize every admissible upper set of the Sharkovsky order.

AI-written summary · about

" chapters (16)

1. 0:00Introduction
2. 1:01Periodic points
3. 2:47A non-standard ordering
4. 4:03Sharkovsky's theorem
5. 4:37Sharkovsky's ordering
6. 6:00Key ingredients
7. 7:25Stating the theorem
8. 9:18Double-checking the order
9. 9:52Proof ingredients
10. 10:59Forcing proof idea
11. 12:41First four parts
12. 19:46Final statement
13. 21:28Key properties of the tent maps
14. 23:10Joining the dots
15. 24:04The hard part
16. 25:14Conclusion