View source for 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 ([https://github.com/openai/math 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'' &ge; 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-Hilbert-Smith-conjecture-in-every-finite-dimension-September-23-2026 ''The Hilbert–Smith conjecture in every finite dimension''], dated 23 September 2026 (repository commit <code>1581d4c</code>).
* '''Formalization.''' The repository has no Lean scope note for this family (checked 16 October 2026).

== Related work by others ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 16 October 2026)
|-
| 2026-10-07 || [https://github.com/google-deepmind/formal-conjectures/issues/6914 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 || [https://github.com/adbrw/HS_proof 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: <code>Challenge.lean</code> 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, [https://github.com/ajjcoppola/hilberts-5th-oai 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 || [https://github.com/Deicyde/hilbert-smith 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.
|}

== 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.

[[Category:OpenAI results]]