Hilbert's Fifth Problem #
The actual formalization is in FormalConjectures.HilbertProblems.«5».
Hilbert's fifth problem asks whether every locally Euclidean topological group admits a Lie group structure. This was resolved affirmatively by Gleason, Montgomery, and Zippin in 1952.
References: