Formalising prime orbit theorem for shifts of finite type in LEAN4
Title
Formalising prime orbit theorem for shifts of finite type in LEAN4
Subject
Formalisation of mathematics
Creator
Akira Corr
Abstract
This project is about the prime orbit theorem for shifts of finite type and my attempt to logically verify the theorem using the LEAN proof assistant.
Files
Citation
Akira Corr, “Formalising prime orbit theorem for shifts of finite type in LEAN4,” URSS SHOWCASE, accessed September 7, 2026, https://linen-dog.lnx.warwick.ac.uk/items/show/1063.