Repository files navigation

The purpose of this repository is to hold a Lean4 formalization of the proof of the Polynomial Freiman-Ruzsa (PFR) conjecture, recently proven inhttps://arxiv.org/abs/2311.05762 . The statement is as follows: if$A$ is a non-empty subset of${\bf F}_2^n$ such that$|A+A| \leq K|A|$, then$A$ can be covered by at most$2K^{12}$ cosets of a subspace$H$ of${\bf F}_2^n$ of cardinality at most$|A|$. The proof relies on the theory of Shannon entropy, so in particular development of the Shannon entropy inequalities will be needed.

Discussion of the project will be held on this Zulip stream:https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture

A blueprint of the proof will be developed athttps://teorth.github.io/pfr/blueprint

Documentation of the methods is athttps://teorth.github.io/pfr/docs

Additional discussion of the project may be found athttps://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton/