teorth/PFR

Technical evidence

Versions, dependency locks, and provider build observations for Polynomial Freiman-Ruzsa project. The project page remains the canonical scholarly record.

222 GitHub starsApache-2.023 indexed versionsRepository Homepage

mathadditive-combinatoricsinformation-theory

Therefore source index

Exact indexed revision

a177b2e4abe4b31c8024b9afebe646bf6bb8f91b

Toolchain: leanprover/lean4:v4.33.0-rc1
Tag: v4.33.0-rc1
Declarations: 45
Mathlib revision: 79d0395a1825

External build observation

Exact commit and toolchain

Reservoir observed a successful build of commit a177b2e4abe4 with leanprover/lean4:v4.33.0-rc1 on 20 Jul 2026. Therefore did not run this build.

Reservoir build log

Pin this exact source in lakefile.lean

require PFR from git "https://github.com/teorth/pfr.git" @ "a177b2e4abe4b31c8024b9afebe646bf6bb8f91b"

Dependency graph

3 direct, 8 transitive

Direct dependencies

mathlib

79d0395a1825a6264ad5d269e35e60537518955e

git

AddCombi

3adf7853e9496af6d7b7175b70f3090a5d53ad41

git

checkdecls

3d425859e73fcfbef85b9638c2a91708ef4a22d4

git

Transitive dependencies

Resolved through the exact indexed manifest.

leanprover-community/plausible

b1c4a69a7e247ab7df20460212001673d74f08c0

git

leanprover-community/LeanSearchClient

c5d5b8fe6e5158def25cd28eb94e4141ad97c843

git

leanprover-community/importGraph

18a90119a5d316358fde6c86e0ca24e59212e32c

git

leanprover-community/proofwidgets

b1436dc749e722c9920036b52cdc43b3451d0b69

git

leanprover-community/aesop

57d3325be72a842920813bcb40f96a6f7393c185

git

leanprover-community/Qq

ee41917ae11d38479fb8fb24745f7ca4bf0a784d

git

leanprover-community/batteries

31a49105f960721073a9adfc82b261f5d0f2ce1e

git

leanprover/Cli

da07ca808b6718cb2aed14dba154e5a08b8f8ecf

git

Version history

23 Reservoir versions

Version records come from the cached Reservoir snapshot. The highlighted row is the exact revision used for Therefore's declaration index.

Show all 23 versions

v4.33.0-rc1Indexed

a177b2e4abe4b31c8024b9afebe646bf6bb8f91b

leanprover/lean4:v4.33.0-rc1

11 dependencies · 16 Jul 2026

v4.32.0

85d5879ae144170098815201491639f6e7d3c352

leanprover/lean4:v4.32.0

11 dependencies · 14 Jul 2026

v4.32.0-rc1

b56e834b18079e9ff756a0f5f2b7f392431c804e

leanprover/lean4:v4.32.0-rc1

11 dependencies · 3 Jul 2026

v4.31.0

38e94172b72c8ee8ad64b6365dfc22e559c62ebe

leanprover/lean4:v4.31.0

11 dependencies · 16 Jun 2026

v4.31.0-rc1

06a1af23d2a7efd895a930f8e9dc5c1c589dabe9

leanprover/lean4:v4.31.0-rc1

11 dependencies · 14 Jun 2026

v4.30.0

3c3c721ae15f22320769ddb146ac86992cd2d035

leanprover/lean4:v4.30.0

11 dependencies · 13 Jun 2026

v4.30.0-rc2

a7fec39013bafd7cb51e75907909c41ac3c88298

leanprover/lean4:v4.30.0-rc2

11 dependencies · 11 Jun 2026

v4.29.0

346ef5b0609538f3fb49dc36c8adc52a0b2db4bb

leanprover/lean4:v4.29.0

11 dependencies · 1 May 2026

v4.28.0

761a18c8d30f1c0ab88e6b04983d6021c8b24257

leanprover/lean4:v4.28.0

11 dependencies · 1 May 2026

v4.28.0-rc1

d91e467880100a96e1c728fcd1894e96f67a153e

leanprover/lean4:v4.28.0-rc1

11 dependencies · 10 Feb 2026

v4.27.0

251c9e214e6a46a1aacffe6774ae1481a5d4d41a

leanprover/lean4:v4.27.0

11 dependencies · 24 Jan 2026

v4.27.0-rc1

feb4a47ae7ad4bdc4fb9cb10142f31f84652e484

leanprover/lean4:v4.27.0-rc1

11 dependencies · 24 Dec 2025

v4.26.0

c92c1284bfb1fabff9e77826c26a7cca7b34bdcf

leanprover/lean4:v4.26.0

11 dependencies · 14 Dec 2025

v4.26.0-rc2

2fb1cac9f6898a364a26e7a5c169e3434cc4f35b

leanprover/lean4:v4.26.0-rc2

11 dependencies · 29 Nov 2025

v4.25.0

e1095d58b7c6f10734988816f7764f2103b9bf29

leanprover/lean4:v4.25.0

10 dependencies · 17 Nov 2025

v4.24.0

7a3d5d49abc8b334bb7813bf253ab01299ef0b85

leanprover/lean4:v4.24.0

10 dependencies · 9 Nov 2025

v4.23.0

450f4d6e5e25d8742de5be6ec51c3b498ce8ad7f

leanprover/lean4:v4.23.0

10 dependencies · 15 Oct 2025

v4.22.0

9a587ebf08971d84f3be1f919cdcf8fc9162d045

leanprover/lean4:v4.22.0

10 dependencies · 22 Aug 2025

v4.21.0

a14e4b1042e0873ce98b9ea53734c1e669fa7c40

leanprover/lean4:v4.21.0

10 dependencies · 3 Jul 2025

v4.20.1

c750735b8622ff153b5f8769013316b7c247e369

leanprover/lean4:v4.20.1

10 dependencies · 6 Jun 2025

v4.19.0

859f6b23d5532de385cff18fc25381e715dba199

leanprover/lean4:v4.19.0

10 dependencies · 2 May 2025

v4.18.0

0010cb5c36c6605a2d0e957390ab4955e6c9e3ff

leanprover/lean4:v4.18.0

10 dependencies · 4 Apr 2025

v4.17.0

620466fdd591a5f19320a49cd296defd8c141728

leanprover/lean4:v4.17.0

10 dependencies · 5 Mar 2025

Version	Revision	Toolchain	Dependencies	Date
v4.33.0-rc1Indexed	a177b2e4abe4	leanprover/lean4:v4.33.0-rc1	11	16 Jul 2026
v4.32.0	85d5879ae144	leanprover/lean4:v4.32.0	11	14 Jul 2026
v4.32.0-rc1	b56e834b1807	leanprover/lean4:v4.32.0-rc1	11	3 Jul 2026
v4.31.0	38e94172b72c	leanprover/lean4:v4.31.0	11	16 Jun 2026
v4.31.0-rc1	06a1af23d2a7	leanprover/lean4:v4.31.0-rc1	11	14 Jun 2026
v4.30.0	3c3c721ae15f	leanprover/lean4:v4.30.0	11	13 Jun 2026
v4.30.0-rc2	a7fec39013ba	leanprover/lean4:v4.30.0-rc2	11	11 Jun 2026
v4.29.0	346ef5b06095	leanprover/lean4:v4.29.0	11	1 May 2026
v4.28.0	761a18c8d30f	leanprover/lean4:v4.28.0	11	1 May 2026
v4.28.0-rc1	d91e46788010	leanprover/lean4:v4.28.0-rc1	11	10 Feb 2026
v4.27.0	251c9e214e6a	leanprover/lean4:v4.27.0	11	24 Jan 2026
v4.27.0-rc1	feb4a47ae7ad	leanprover/lean4:v4.27.0-rc1	11	24 Dec 2025
v4.26.0	c92c1284bfb1	leanprover/lean4:v4.26.0	11	14 Dec 2025
v4.26.0-rc2	2fb1cac9f689	leanprover/lean4:v4.26.0-rc2	11	29 Nov 2025
v4.25.0	e1095d58b7c6	leanprover/lean4:v4.25.0	10	17 Nov 2025
v4.24.0	7a3d5d49abc8	leanprover/lean4:v4.24.0	10	9 Nov 2025
v4.23.0	450f4d6e5e25	leanprover/lean4:v4.23.0	10	15 Oct 2025
v4.22.0	9a587ebf0897	leanprover/lean4:v4.22.0	10	22 Aug 2025
v4.21.0	a14e4b1042e0	leanprover/lean4:v4.21.0	10	3 Jul 2025
v4.20.1	c750735b8622	leanprover/lean4:v4.20.1	10	6 Jun 2025
v4.19.0	859f6b23d553	leanprover/lean4:v4.19.0	10	2 May 2025
v4.18.0	0010cb5c36c6	leanprover/lean4:v4.18.0	10	4 Apr 2025
v4.17.0	620466fdd591	leanprover/lean4:v4.17.0	10	5 Mar 2025

Build history

4 observations for the indexed commit

These are Reservoir provider observations. They never change a Therefore proof status and they are not independent rebuilds by Therefore.

Show provider build history

leanprover/lean4:v4.32.1

Build passed · Test not observed · 23 Jul 2026

Required lake update

Build log

leanprover/lean4:v4.33.0-rc1

Build passed · Test not observed · 20 Jul 2026

Build log

leanprover/lean4:v4.33.0-rc1

Build passed · Test not observed · 19 Jul 2026

Build log

leanprover/lean4:v4.33.0-rc1

Build passed · Test not observed · 17 Jul 2026

Build log

Selected source declarations

Selected declarations

Search within package

Showing 6 of 17 source-indexed declarations. The canonical project page and project search expose the full index.

Project-declaredLean 4.33.0-rc1

Approx hom pfr

approx_hom_pfr

Project documentation

An approximate-homomorphism theorem for finite elementary abelian $2$ -groups. Let $f:G\to G'$ and $K>0$ . If at least a proportion $K^{-1}$ of pairs $(x,y)\in G^2$ satisfy $f(x+y)=f(x)+f(y)$ , then there are an additive homomorphism $\varphi:G\to G'$ and a constant $c\in G'$ such that $f(x)=\varphi(x)+c$ for at least $|G|/(2^{144}K^{122})$ values of $x$ .

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record

Project-declaredLean 4.33.0-rc1

Better PFR conjecture

better_PFR_conjecture

Plain-language statement

If $A \subset {\bf F}_2^n$ is finite non-empty with $|A+A| \leq K|A|$ , then there exists a subgroup $H$ of ${\bf F}_2^n$ with $|H| \leq |A|$ such that $A$ can be covered by at most $2K^9$ translates of $H$ .

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record

Project-declaredLean 4.33.0-rc1

Better PFR conjecture

better_PFR_conjecture'

Project documentation

Polynomial Freiman-Ruzsa theorem with exponent $9$ , without a finite ambient-group assumption. Let $A$ be a nonempty finite subset of an elementary abelian $2$ -group. If $|A+A|\le K|A|$ , then there are a finite subspace $H$ and a finite set $c$ such that $A\subseteq c+H$ , $|c|<2K^9$ , and $|H|\le|A|$ .

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record

Project-declaredLean 4.33.0-rc1

Card of dual constrained

card_of_dual_constrained

Plain-language statement

In the ambient finite $\mathbb F_2$ -vector space, exactly half of the additive homomorphisms $\varphi:G\to\mathbb F_2$ take a fixed nonzero vector $x$ to $1$ : $2\,|\{\varphi:\varphi(x)=1\}|=|G|$ .

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record

Project-declaredLean 4.33.0-rc1

Card of slice

card_of_slice

Plain-language statement

For every set $A$ in the ambient finite $\mathbb F_2$ -vector space, some linear functional $\varphi:G\to\mathbb F_2$ has at least $(|A|-1)/2$ elements of $A$ in its $1$ -fiber.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record

Project-declaredLean 4.33.0-rc1

Cond multi Dist chain Rule

cond_multiDist_chainRule

Plain-language statement

A chain rule for conditional multidistance. Let $\pi:G\to H$ be a homomorphism, and suppose the pairs $(X_i,Y_i)$ are independent across the finite index set. Then $D[X\mid Y]=D[X\mid(\pi X,Y)]+D[\pi X\mid Y]+I\!\left[\sum_iX_i:(\pi X_i)_i\,\middle|\,\left(\pi\!\left(\sum_iX_i\right),(Y_i)_i\right)\right].$ The first term measures the remaining fiberwise multidistance after adjoining each image $\pi(X_i)$ to its conditioning data.

additive combinatoricsentropyprobability

Source project: Polynomial Freiman-Ruzsa project

Person-level attribution pending.

View proof record