FormalConjectures/Wikipedia/HilbertFifthProblem.lean
0 declarations, 0 contain sorry, 0 declared as axioms
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:
No declarations listed.