Formalization of symbolic dynamics in Lean 4.

• Shift spaces, subshifts
• Sliding block codes
• The Curtis-Hedlund-Lyndon theorem
• Prodiscrete topology
• Subshifts of finite type

Work in progress:

• Curtis-Hedlund-Lyndon variant for uniform structures
• Formal language of a subshift
• Subshifts of Sofic type

References:

1. "Cellular automata and groups" by Ceccherini-Silberstein and Coornaert (2010) https://doi.org/10.1007/978-3-642-14034-1