# 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.

- Discussion of the project on Zulip
- Blueprint of the proof
- Documentation of the methods
- A quick “tour” of the project
- Some example Lean code to illustrate the results in the project
- An (automatically generated) list of contributors to the project

## 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:

`PFR/ForMathlib/Elementary.lean`

`PFR/ForMathlib/FiniteMeasureProd.lean`

`PFR/ForMathlib/Graph.lean`

`PFR/ForMathlib/Pair.lean`

`PFR/ForMathlib/Summable.lean`

`PFR/Mathlib/Algebra/BigOperators/Basic.lean`

`PFR/Mathlib/Algebra/Group/Hom/Basic.lean`

`PFR/Mathlib/Algebra/Group/Subgroup/Pointwise.lean`

`PFR/Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean`

`PFR/Mathlib/Data/ENNReal/Basic.lean`

`PFR/Mathlib/Data/Fin/Basic.lean`

`PFR/Mathlib/Data/Fin/VecNotation.lean`

`PFR/Mathlib/Data/Finset/Sigma.lean`

`PFR/Mathlib/Data/Fintype/Card.lean`

`PFR/Mathlib/Data/Fintype/Lattice.lean`

`PFR/Mathlib/Data/Fintype/Sigma.lean`

`PFR/Mathlib/Data/Real/Ennreal.lean`

`PFR/Mathlib/Data/Set/Image.lean`

`PFR/Mathlib/Data/Set/Pointwise/SMul.lean`

`PFR/Mathlib/Data/Set/Sigma.lean`

`PFR/Mathlib/GroupTheory/Subgroup/Pointwise.lean`

`PFR/Mathlib/GroupTheory/Torsion.lean`

`PFR/Mathlib/LinearAlgebra/Basis/VectorSpace.lean`

`PFR/Mathlib/MeasureTheory/Constructions/Pi.lean`

`PFR/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean`

`PFR/Mathlib/MeasureTheory/Integral/Bochner.lean`

`PFR/Mathlib/MeasureTheory/Integral/Lebesgue.lean`

`PFR/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean`

`PFR/Mathlib/MeasureTheory/Measure/MeasureSpace.lean`

`PFR/Mathlib/MeasureTheory/Measure/NullMeasurable.lean`

`PFR/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean`

`PFR/Mathlib/MeasureTheory/Measure/Typeclasses.lean`

`PFR/Mathlib/Probability/Kernel/MeasureCompProd.lean`

`PFR/Mathlib/SetTheory/Cardinal/Finite.lean`

`PFR/Tactic/Finiteness/Attr.lean`

`PFR/Tactic/RPowSimp.lean`

## Source reference

`[GGMT]`

: https://arxiv.org/abs/2311.05762