View on GitHub

Formalization of multiperiodic words in Isabelle and Lean

Code related to the chapter by Štěpán Holub in CANT 2025

E-mail: holub@karlin.mff.cuni.cz

Introduction

This is a page accompanying the chapter Formalization of combinatorics of finite words with Isabelle and Lean published in the book CANT 2025.

Setup

Getting the files:
- Clone the repository from GitHub (see the link on the top of the page). This assumes git is installed on your system.
- Alternatively, it is possible to just download the zipped folder, and unpack.
Install the current release of Isabelle
Install the Lean 4 proof assistant (including and via VS Code and its Lean extension)

Isabelle code

The Isabelle code is located in the isabelle folder. The main file is Multiperiodic.thy. Run Isabelle, and in the jEdit editor, open the file.

The folder contains a standalone collection of theories. Note that possibly slightly different version of background theories is included in the folder are also part of the Archive of Formal Proofs.

Lean code

The Lean code is located in the lean/CANT2025 folder. The theory is divided into three files. The files depend on Mathlib, the standard library for Lean formalizations.

Open Multiperiodic.lean and agree with restarting the Lean server.
Missing packages are then installed in the folder lean/CANT2025/.lake. This may take around 15 minutes and the final size of the folder is about 1.2 GB.
If an error is reported, it may be caused by the antivirus software. Pausing the antivirus software during installation may help.