Data

Tools

Indexes

Applications

Experiments

Open Source Science

pfr

Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)

https://github.com/teorth/pfr

Science Score: 54.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ✓
    CITATION.cff file
    Found CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ○
    DOI references
  • ✓
    Academic publication links
    Links to: arxiv.org
  • ○
    Academic email domains
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (11.1%) to scientific vocabulary
Last synced: 6 months ago · JSON representation ·

Repository

Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)

Basic Info
Statistics
  • Stars: 185
  • Watchers: 6
  • Forks: 41
  • Open Issues: 1
  • Releases: 5
Created over 2 years ago · Last pushed 6 months ago
Metadata Files
Readme License Citation

README.md

The Polynomial Freiman-Ruzsa Conjecture

GitHub CI Gitpod Ready-to-Code

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 $A$ is a non-empty subset of ${\bf F}2^n$ such that $\lvert A+A\rvert \leq K\lvert A\rvert$, then $A$ can be covered by at most $2K^{12}$ cosets of a subspace $H$ of ${\bf F}2^n$ of cardinality at most $\lvert A\rvert$. 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 $12$ to $11$. 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 $9$.

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

Owner

  • Login: teorth
  • Kind: user

Citation (CITATION.cff) 

cff-version: 1.2.0
message: >
  If you use this project in your work, please cite it using the metadata below.
title: "Formalization of the Polynomial Freiman-Ruzsa Conjecture of Marton"
version: 0.1.0
date-released: Nov 12, 2023
authors:
  - family-names: Anderson
    given-names: Aaron
  - family-names: Bakšys
    given-names: Mantas
  - family-names: Bayer
    given-names: Jonas
  - family-names: Collares
    given-names: Mauricio
  - family-names: Degenne
    given-names: Rémy
  - family-names: Dillies
    given-names: Yaël
  - family-names: Eltschig
    given-names: Ben
  - family-names: Gouëzel
    given-names: Sébastien
  - family-names: Kytölä
    given-names: Kalle
  - family-names: Lewis
    given-names: Rob
  - family-names: Lez
    given-names: Paul
  - family-names: Lorenzo
    given-names: Luccioli
  - family-names: Macbeth
    given-names: Heather
  - family-names: Massot
    given-names: Patrick
  - family-names: Mellendijk
    given-names: Arend
  - family-names: Miller
    given-names: Kyle
  - family-names: Monticone
    given-names: Pietro
  - family-names: Morrison
    given-names: Kim
  - family-names: Nash
    given-names: Oliver
  - family-names: Song
    given-names: Utensil
  - family-names: Tao
    given-names: Terence
    orcid: https://orcid.org/0000-0002-0140-7641
  - family-names: van Doorn
    given-names: Floris
  - family-names: Wilshaw
    given-names: Sky
  - family-names: Wu
    given-names: Lawrence
repository-code: https://github.com/teorth/pfr
url: https://github.com/teorth/pfr
abstract: >
  A collaborative project to formalize the Polynomial Freiman-Ruzsa Conjecture of
  Katalin Marton, as well as related results, in the Lean4 proof assistant language.

  Organized by Yael Dillies and Terence Tao. Launched Nov 12, 2023.
keywords:
  - additive combinatorics
  - polynomial Freiman-Ruzsa conjecture
  - formalization project

GitHub Events

Total
  • Create event: 9
  • Commit comment event: 1
  • Release event: 7
  • Issues event: 2
  • Watch event: 40
  • Delete event: 3
  • Issue comment event: 26
  • Push event: 109
  • Pull request review event: 14
  • Pull request review comment event: 14
  • Pull request event: 47
  • Fork event: 5
Last Year
  • Create event: 9
  • Commit comment event: 1
  • Release event: 7
  • Issues event: 2
  • Watch event: 40
  • Delete event: 3
  • Issue comment event: 26
  • Push event: 109
  • Pull request review event: 14
  • Pull request review comment event: 14
  • Pull request event: 47
  • Fork event: 5