Wikipedia · research solved · AMS 20
hardknown result, no worker yet
Gromov's theorem on groups of polynomial growth
Theorem · GromovPolynomialGrowthTheorem
**Gromov's Polynomial Growth Theorem** : A finitely generated group has polynomial growth if and only if it is virtually nilpotent.
Formal statement · Lean 4.lean
theorem GromovPolynomialGrowthTheorem [Group.FG G] :
HasPolynomialGrowth G ↔ Group.IsVirtuallyNilpotent G := by
sorryProof. sorry
Nobody has tried yet.