The purpose of this repository is to hold a Lean4 formalization of the proof of the Polynomial Freiman-Ruzsa (PFR) conjecture, recently proven in https://arxiv.org/abs/2311.05762 . The statement is as follows: if
Discussion of the project will be held on this Zulip stream: https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture
Additional discussion of the project may be found at https://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton/