PFR conjecture formalization (Lean)
Statement
The Polynomial Freiman–Ruzsa (PFR) conjecture formalized in Lean. Converts complex additive combinatorics into axiomatic code. Part of the digital axiomatization program; demonstrates that number theory can be machine-verified.
Formula
PFR: structure of approximate subgroups
Proof sketch
Brasca, Tao, collaborators: formalization in Lean 4. PFR conjecture (additive combinatorics) proved and verified.
Source
teorth/pfr, 2024. Tao et al., On the polynomial Freiman–Ruzsa conjecture.
Domains
mathematics, computer-science