Abstract

The Freiman-Ruzsa theorem asserts that if a finite subset $A$ of an $m$-torsion group $G$ is of doubling at most $K$ in the sense that $|A+A| \leq K|A|$, then $A$ is covered by at most $m ^K2$ cosets of a subgroup $H$ of $G$ of cardinality at most $|A|$.  Marton’s Polynomial Freiman-Ruzsa conjecture asserted (in the $m=2$ case, at least) that the constant $m ^K2$ could be replaced by a polynomial in $K$.  In joint work with Timothy Gowers, Ben Green, and Freddie Manners, we establish this conjecture for $m=2$ with a bound of $2K^{$ (later improved to $2K}{11}$ by Jyun-Jie Liao by a modification of the method), and for arbitrary $m$ with a bound of $(2K)^{$.  Our proof proceeds by passing to an entropy-theoretic version of the problem, and then performing an iterative process to reduce a certain modification of the entropic doubling constant, taking advantage of the bounded torsion to obtain a contradiction when the (modified) doubling constant is non-trivial but cannot be significantly reduced.  By known implications, this result also provides polynomial bounds for inverse theorems for the $U}3$ Gowers uniformity norm, or for linearization of approximate homomorphisms. In a collaborative project with Yael Dillies and many other contributors, the proof of the $m=2$ result has been completely formalized in the proof assistant language Lean.  In this talk we will present both the original human-readable proof, and the process of formalizing it into Lean.