In this project, we formalise Fomin and Zelevinsky's celebrated Laurent phenomenon for cluster algebras