BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Marton's Polynomial Freiman-Ruzsa conjecture - Terence Tao (Univer
 sity of California\, Los Angeles)
DTSTART:20240412T143000Z
DTEND:20240412T153000Z
UID:TALK214051@talks.cam.ac.uk
DESCRIPTION: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^{K^4+1} K^2$ cosets 
 of a subgroup $H$ of $G$ of cardinality at most $|A|$.&nbsp\; Marton's Pol
 ynomial Freiman-Ruzsa conjecture asserted (in the $m=2$ case\, at least) t
 hat the constant $m^{K^4+1} K^2$ could be replaced by a polynomial in $K$.
 &nbsp\; In joint work with Timothy Gowers\, Ben Green\, and Freddie Manner
 s\, we establish this conjecture for $m=2$ with a bound of $2K^{12}$ (late
 r improved to $2K^{11}$ by Jyun-Jie Liao by a modification of the method)\
 , and for arbitrary $m$ with a bound of $(2K)^{O(m^3 \\log m)}$.&nbsp\; Ou
 r proof proceeds by passing to an entropy-theoretic version of the problem
 \, and then performing an iterative process to reduce a certain modificati
 on of the entropic doubling constant\, taking advantage of the bounded tor
 sion to obtain a contradiction when the (modified) doubling constant is no
 n-trivial but cannot be significantly reduced.&nbsp\; By known implication
 s\, this result also provides polynomial bounds for inverse theorems for t
 he $U^3$ Gowers uniformity norm\, or for linearization of approximate homo
 morphisms.\nIn a collaborative project with Yael Dillies and many other co
 ntributors\, the proof of the $m=2$ result has been completely formalized 
 in the proof assistant language Lean.&nbsp\; In this talk we will present 
 both the original human-readable proof\, and the process of formalizing it
  into Lean.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR