The Polynomial Freiman-Ruzsa Conjecture

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

Build the Lean files

To build the Lean files of this project, you need to have a working version of Lean. See the installation instructions (under Regular install). Alternatively, click on the button below to open a Gitpod workspace containing the project.

In either case, run lake exe cache get and then lake build to build the project.

Build the blueprint

To build the web version of the blueprint, you need a working LaTeX installation. Furthermore, you need some packages:

sudo apt install graphviz libgraphviz-dev
pip install -r blueprint/requirements.txt

To actually build the blueprint, run

lake exe cache get
lake build
inv all

Moving material to mathlib

The project is now over. As such, we are currently working towards stabilising the new results and contributing them to mathlib.

Here is the list of files that do not depend on any other PFR file, indicating they are good candidates for upstreaming to mathlib:

Source reference

[GGMT]: https://arxiv.org/abs/2311.05762