A Lean4 formalisation of the Furstenberg–Sárközy theorem First, I will be doing the Fourier-free proof by Green–Tao–Ziegler. After that, who knows.