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 is a non-empty subset of such that , then can be covered by at most cosets of a subspace of of cardinality at most . The proof relies on the theory of Shannon entropy, so in particular development of the Shannon entropy inequalities was needed.

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 to . This second stage has also been completed.

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

See instructions at https://github.com/PatrickMassot/leanblueprint/.

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