This Sunday we're hosting Aaron Hill to present his Lean formalization of Gromov's theorem on groups of polynomial growth. Proved in 1981, the theorem gives information about the global structure of a group based only on the behavior of a finite set of generators. The original paper states it in one line:
If a finitely generated group Γ has polynomial growth then Γ contains a nilpotent subgroup of finite index.
Gromov builds on earlier work of Wolf, Bass, and Guivarc'h, who by 1973 had proved the converse: a nilpotent subgroup of finite index implies polynomial growth. The theorem is a founding result of geometric group theory, where it finds applications in the classification of expanding maps, the analysis of random walks, and the topology of Riemannian manifolds.
Aaron's formalization follows the proof Terence Tao presented on his blog in 2010, based on Kleiner's 2007 work and substantially more elementary than the proofs that came before:
The argument requires four separate ingredients. The first is the existence of non-trivial Lipschitz harmonic functions… The second is that there are not too many such harmonic functions… The third ingredient is that Gromov's theorem is true in the compact linear Lie group case… The final ingredient is that Gromov's theorem is inductively true once one can locate an infinite cyclic quotient.
The formal proof totals 28,000 lines of Lean, with its target theorem drawn from the Formal Conjectures library. Come hear how the pieces fit together at his talk this Sunday, August 30.