// the find
teorth/pfr
Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)
A Lean4 formalization of Terence Tao, Marton, and collaborators' proof of the Polynomial Freiman-Ruzsa conjecture over F_2^n, later extended to bounded-torsion groups and tighter exponents. This is for people doing formal verification of research mathematics, not for application developers — it's a proof artifact, not a library you import.
Uses the leanblueprint workflow, so the LaTeX proof outline links directly to the Lean declarations that implement each step — you can actually trace a textbook proof step to code, which most formalization repos skip. The 'Palomar' Challenge/Solution split is a genuinely good idea: it restates the six headline theorems in Lean-core-and-Mathlib-only terms with a sorry, then proves each from the main development, giving an auditable check that the formalization matches what the papers claim rather than something subtly weaker. Active, multi-year project that already shipped the original PFR proof and has since tightened the exponent from 12 to 9 and generalized to other torsion groups — this isn't a one-shot formalization stunt, it's a maintained research artifact with CI on every push.
Zero onboarding beyond a link to the generic Lean install guide — no explanation of the namespace layout (ForMathlib/Entropy/Kernel/...), the dependency order between files, or which results are load-bearing versus auxiliary. The README states only the Challenge.lean file contains deliberate sorrys but offers no CI badge or script proving the rest of 150+ files are sorry-free and axiom-clean; you'd have to grep it yourself. It's pinned hard to a specific mathlib commit via lake-manifest.json, and since the project is actively extending the proof (bounded torsion, exponent 9), the codebase is a moving target rather than something you can clone and expect to still build in six months without updating the toolchain and manifest.