HilbertSmith roadmap

A Lean 4 formalization of the OpenAI proof of the Hilbert--Smith conjecture in every finite dimension. The book states the main theorems, builds a sheaf-theoretic signature invariant with a fixed integral lattice, prepares local tests from a hypothetical faithful \(p\)-adic action, and derives a contradiction from equal character parts.

Chapters

• Main theorems
• Background prerequisites
• Sheaf categories and homotopy invariance
• Localization, germs, and dense subcategories
• A bounded lattice on the test sphere
• Preparing local tests
• Character classes and the contradiction