[Here](https://arxiv.org/abs/1907.01449) is a Lean formalisation of a 2017 Annals of Mathematics paper.