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/FiniteMeasureProd.lean
PFR/ForMathlib/FiniteRange/Defs.lean
PFR/ForMathlib/GroupQuot.lean
PFR/ForMathlib/MeasureReal.lean
PFR/ForMathlib/Pair.lean
PFR/ForMathlib/ZModModule.lean
PFR/Mathlib/Algebra/AddTorsor.lean
PFR/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
PFR/Mathlib/Analysis/SpecialFunctions/NegMulLog.lean
PFR/Mathlib/Data/Set/Pointwise/SMul.lean
PFR/Mathlib/LinearAlgebra/Basis/VectorSpace.lean
PFR/Mathlib/LinearAlgebra/Dimension/Finrank.lean
PFR/Mathlib/MeasureTheory/Constructions/Pi.lean
PFR/Mathlib/MeasureTheory/Integral/Lebesgue.lean
PFR/Mathlib/MeasureTheory/Integral/SetIntegral.lean
PFR/Mathlib/MeasureTheory/Measure/Prod.lean
PFR/Mathlib/Probability/ConditionalProbability.lean
PFR/Mathlib/Probability/Independence/Kernel.lean
PFR/Mathlib/Probability/UniformOn.lean
PFR/Mathlib/SetTheory/Cardinal/Finite.lean
PFR/Tactic/RPowSimp.lean
Source reference
[GGMT]
: https://arxiv.org/abs/2311.05762