Skip to content

fpvandoorn/pfr

 
 

Repository files navigation

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 $|A+A| \leq K|A|$, then $A$ can be covered by at most $2K^{12}$ cosets of a subspace $H$ of ${\bf F}_2^n$ of cardinality at most $|A|$. 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).

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
pip3 install invoke pandoc
cd .. # go to folder where you are happy clone git repos
git clone git@github.com:plastex/plastex
pip3 install ./plastex
git clone git@github.com:PatrickMassot/leanblueprint
pip3 install ./leanblueprint
cd sphere-eversion

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.

Source reference

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

About

No description, website, or topics provided.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Lean 77.3%
  • TeX 21.4%
  • Python 0.6%
  • CSS 0.3%
  • Shell 0.3%
  • Batchfile 0.1%