Formalizing the Proof of Polynomial Freiman-Ruzsa in Lean4 | Heykuki News