# Infinite Words and Morphic Languages Formalized in Isabelle/HOL

arXiv: https://arxiv.org/abs/2303.11445 · HTML: https://mlsanity.com/paper/2303.11445/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Mar 2023.

## Built on by (most cited first, 1 of 1)

- [LAMP: Lean-based Agentic framework with MCP and Proof Repair](https://mlsanity.com/paper/2606.28841/) (2026)

## Abstract (arXiv)

We present a formalization of basics related to infinite words in the generic proof assistant Isabelle/HOL. Furthermore, we present a formalization of purely morphic and morphic languages. Finally, we present a formalized definition of Sturmian words as lower mechanical words and prove some very elementary facts. The formalization is based on an ongoing larger project of formalization of combinatorics on words.