Tim Gowers, Ben Green, Freddie Manners and I just uploaded a paper https://arxiv.org/abs/2311.05762 proving the Polynomial Freiman-Ruzsa conjecture. More details at https://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton/ .
I am planning to formalize this paper in #Lean4 also; more on this later.