The Hilbert–Smith conjecture

The Hilbert–Smith conjecture asks whether a locally compact group acting faithfully and continuously on a connected topological manifold must be a Lie group. By the classical reduction, it is equivalent to the statement that for no prime p does the additive group of p-adic integers act faithfully and continuously on a connected manifold. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the conjecture in every finite dimension. A parallel claim by other means, accompanied by a Lean formalization, was posted on GitHub on 7–8 October 2026. This page summarizes the published claims and lists related public work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the manuscript's introduction: Hilbert's fifth problem asked how far differentiability assumptions could be removed from the theory of continuous transformation groups. Gleason and Montgomery–Zippin resolved its formulation for locally Euclidean groups in 1952, and Yamabe extended the structure theory to locally compact groups. The reduction of the Hilbert–Smith conjecture to actions of the p-adic integers combines this structure theory with rigidity of periodic transformations (Newman's theorem). The cases of one- and two-dimensional manifolds were classical, and Pardon proved the three-dimensional case in 2013. Other work assumes regularity of the action: the differentiable case (Bochner–Montgomery), the Lipschitz case (Repovš–Ščepin), Hölder actions with large exponent (Maleshich) and the quasiconformal case (Martin), connected with the dimension-raising theory of Yang and of Bredon, Raymond and Williams.

The original result

• Claim. For every n ≥ 1, a locally compact second-countable Hausdorff group acting faithfully and jointly continuously on a connected Hausdorff second-countable topological n-manifold without boundary is a Lie group. The mechanism is p-adic exclusion: every jointly continuous action of the p-adic integers on such a manifold has nonzero kernel. The manuscript also records the dynamical consequence that some positive iterate of an almost periodic homeomorphism of such a manifold lies on a continuous one-parameter flow.
• Source. The manuscript The Hilbert–Smith conjecture in every finite dimension, dated 23 September 2026 (repository commit 1581d4c).
• Formalization. The repository has no Lean scope note for this family (checked 16 October 2026).

Related work by others

Date	Work	Relation	Public claim	Public status (checked 16 October 2026)
2026-10-07	Formal Conjectures issue 6914, HilbertProblems/5: the Hilbert–Smith conjecture is true	Catalogue proposal	Proposes formal statements of the conjecture for Google DeepMind's Formal Conjectures catalogue.	Open issue.
2026-10-07	adbrw/HS_proof (GitHub; paper Integral tail signatures and the Hilbert–Smith conjecture, dated 8 October 2026, by "A. Dabrowski's AI agents")	Parallel claim with formalization	p-adic exclusion and the Hilbert–Smith conjecture by a different route: an integer signature tail in quadratic L-theory is shown to be eventually divisible by p, while an effective action of the p-adic integers produces a class with signature tail 1. The repository contains a Lean 4 / Mathlib formalization: Challenge.lean states the conjecture importing only Mathlib, and a 239-module development proves it; the README states that it uses only Lean's three standard axioms and also proves the two variants proposed in issue 6914.	GitHub repository; it includes a Comparator record for the Formal Conjectures variants (commit of 10 October 2026).
2026-10-07	Alan Coppola, ajjcoppola/hilberts-5th-oai (GitHub)	Audit	"Reverse verification" audits of both preprints, describing them as one family of arguments (integrality versus p-divisibility of a signature or Witt invariant) with different packaging. No load-bearing lemma is graded as failing in either; several steps are graded as weak.	GitHub repository; the author line credits Cursor (Opus 5.5/Grok) driven by Alan Coppola. The audit states that it did not rerun the Lean certificate of the parallel claim.
2026-10-13	Deicyde/hilbert-smith (GitHub)	Formalization (in progress)	A Lean 4 formalization of the manuscript's proof, developed with Meta's AutoformBot, with a blueprint site.	GitHub repository; a work in progress whose latest commit (14 October 2026) documents remaining gaps.
2026-10-16	Palomar registry entry PALOMAR-2026-10-16-000006 (version 1), Hilbert–Smith and p-adic exclusion with second countability, for adbrw/HS_proof at commit b75523f	Registration of the parallel formalization	The registered theorem is hilbert_smith of Challenge.lean, in which the manifold and the acting group are both assumed second countable, with only Lean's three standard axioms permitted. The registered commit, on a review branch, migrates the files to Lean's module system; the project's metadata states that the migration keeps every original declaration and proof and drops no hypothesis.	Registry entry. The record reports a mechanical verification on 15 October 2026 (UTC) with the Comparator configuration of the repository and the kernel checkers nanoda and con-ron. The project's metadata states that no independent human mathematical review is asserted.

Notes

• Dates are those shown by GitHub, the papers and the manuscript. The list covers sources found up to the date above; it makes no priority or completeness claim.