In this project, we formalise in Lean 4 the claim that the sequence of maximums of values of (Coxeter) frieze patterns is the Fibonacci sequence.
A Latex file with the exact statements is available i) on the blueprint (here: https://antoine-dsg.github.io/frieze_patterns/blueprint/), and ii) in the note "On upper bounds in frieze patterns" (here: https://arxiv.org/pdf/2407.16717).

Contributions (in alphabetical order) by:
Akselai
Jon Cheah
Bockman Cheung
Eaton Liu
Antoine de Saint Germain