A few months ago, I decide to attempt to formalize one of my own papers using the Lean4 theorem prover. I will report on this experiment. (The Lean code can be found there: https://github.com/smorel394/TS1)