## The Polynomial Freiman-Ruzsa Conjecture

The original purpose of this repository is to hold a Lean4 formalization of the proof of the Polynomial Freiman-Ruzsa (PFR) conjecture of Katalin Marton (see also this blog post). The statement is as follows: if

After the primary purpose of the project was completed, a second stage of the project developed several consequences of PFR, as well as an argument of Jyun-Jie Liao that reduced the exponent

Currently, the project is obtaining an extension of PFR to other bounded torsion groups, as well as formalizing a further refinement of Jyun-Jie Liao that improves the exponent further to

- 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

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

To build the project, run `lake exe cache get`

and then `lake build`

.

### 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 uninstall -y leanblueprint
pip install -r blueprint/requirements.txt
```

To actually build the blueprint, run

```
lake exe cache get
lake build
inv all
```

To view the web-version of the blueprint locally, run `inv serve`

and navigate to
`http://localhost:8000/`

in your favorite browser.

Or you can just run `inv dev`

instead of `inv all`

and `inv serve`

, after each edit to the LaTeX,
it will automatically rebuild the blueprint, you just need to refresh the web page to see the rendered result.

Note: If you have something wrong in your LaTeX file, and the LaTeX compilation fails,
LaTeX will stuck and ask for commands, you'll need to type `X`

then return to exit LaTeX,
then fix the LaTeX error, and run `inv dev`

again.

### Moving material to mathlib

As the first two phases of the project are completed, we are currently working towards stabilising the new results and contributing them to mathlib.

### Source reference

`[GGMT]`

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

`[L]`

: https://arxiv.org/abs/2404.09639

`[GGMT2]`

: https://arxiv.org/abs/2404.02244