Acknowledgements

I am immensely grateful to Riccardo Brasca for his exceptional supervision throughout the entire formalisation project. His guidance was pivotal in the coordination and execution of this work.

I extend my deepest appreciation to my colleagues Sanyam Gupta, Omar Haddad, David Lowry-Duda, Lorenzo Luccioli, Alexis Saurin, and Florent Schaffhauser. Their collaboration was essential in addressing the challenges we faced.

Special thanks are due to Floris van Doorn, whose expertise in the foundations of the Lean programming language was invaluable in order to debug and optimise the code for some of the most challenging formal proofs.

I would also like to acknowledge the organisers of the conference Lean for the Curious Mathematician 2024. Their efforts provided us with a wonderful platform to share our work and insights, fostering further dialogue and collaboration in the community.

This project would not have been possible without the collective effort and support of all mentioned, for which I am profoundly thankful.