Hilbert–Smith conjecture claimed by OpenAI, Lean-checked by a separate AI proof
Awaiting review
Importance: historic (5 of 5)The takeaway
A manuscript in OpenAI’s 6 Oct 2026 math release (family 304, dated 23 Sept) claims the Hilbert–Smith conjecture, the manifold-action form of Hilbert’s fifth problem, in every dimension. Only dimensions up to three were known (Pardon, 2013). OpenAI’s paper has no Lean proof. On 8 Oct a GitHub author posted a separate 17-page proof written by ‘A. Dabrowski’s AI agents’, with a Lean 4 formalization that the Palomar registry lists since 16 Oct. We found no public expert assessment of either proof as of 29 Oct.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Historic (5 of 5)
- Last verified
- 29 October 2026
Your AI and this story
- GPT-6 Astra159 days after its cutoff
- Claude Opus 5.598 days after its cutoff
- Gemini 4 Argon189 days after its cutoff
- Grok 4.7128 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 98 days before it.
Key facts
- Claim (abstract, verbatim): ‘We prove the Hilbert–Smith conjecture in every finite dimension: every locally compact second-countable Hausdorff group acting faithfully and jointly continuously on a connected Hausdorff second-countable finite-dimensional topological manifold without boundary is a Lie group.’
- Mechanism (Theorem 1.2 of the paper): every jointly continuous action of the p-adic integers ℤ_p on such a manifold has nonzero kernel; the classical reduction (Gleason, Montgomery–Zippin, Yamabe, Newman) turns this into the group statement
- Prior state, as the paper recounts it: one- and two-manifolds classical; Pardon proved dimension three (J. Amer. Math. Soc., 2013); Repovš–Ščepin (1997) the Lipschitz case and Martin (1999) the quasiconformal case in all dimensions
- Release status: manuscript only, no Lean scope note for family 304; no withdrawal or revision in history.md
- Separate proof: ‘Integral tail signatures and the Hilbert–Smith conjecture’, A. Dabrowski’s AI agents, 8 Oct 2026 (github.com/adbrw/HS_proof). Its AI disclosure: ‘Critical construction steps were developed jointly by Opus 5.5 and GPT 6.1’, with a Lean formalization ‘completed in Lean 4 by Opus 5.5 and verified with Comparator and SafeVerify’; ‘This work was carried out as an independent research project.’ It does not cite OpenAI’s manuscript
- Palomar registry (published 16 Oct, 02:19 UTC): ‘Hilbert–Smith and p-adic exclusion with second countability’, theorem hilbert_smith, trust level ‘high’. The repo README lists only propext, Classical.choice and Quot.sound as axioms. Wikipedia’s Hilbert–Smith article now cites both the OpenAI manuscript and the Palomar entry
- Formal Conjectures issue #6914 (opened 7 Oct, still open on 29 Oct) proposes marking hilbert_smith_conjecture solved on the basis of OpenAI’s paper, noting that the Formal Conjectures statements drop second countability and the reduction must be checked
- Other checks: an AI-assisted ‘reverse-verification’ by Alan J. Coppola (github.com/ajjcoppola/hilberts-5th-oai) found only ‘places for experts in certain areas to look further’ (his MathOverflow question, closed as off-topic); an in-progress Lean blueprint of OpenAI’s proof (Deicyde/hilbert-smith, developed with facebookresearch’s AutoformBot)
What happened
Hilbert’s fifth problem asked how much smoothness can be dropped from the theory of continuous transformation groups. For groups that are themselves locally Euclidean it was solved in 1952 (Gleason, Montgomery–Zippin). The Hilbert–Smith conjecture asks the same for groups that only act faithfully on a manifold. It reduces to one question: can the p-adic integers act faithfully on a manifold? The answer was known to be no only in dimensions up to three (John Pardon, 2013) and for Lipschitz or quasiconformal actions.
OpenAI’s 6 Oct release contains a manuscript claiming the conjecture in every finite dimension, through an obstruction built from sheaf categories, Witt localization and signatures. It has no Lean formalization. Two days later a GitHub user posted a different 17-page argument (an “integer signature tail”) credited to “A. Dabrowski’s AI agents”, built with Opus 5.5 and GPT 6.1. A Lean 4 formalization of it is registered on Palomar, the Lean FRO’s registry of machine-checked results. That proof assumes second countability, as OpenAI’s statement does. It does not cite OpenAI’s paper and calls itself an independent research project.
Why it matters
If either proof is right, a conjecture open beyond dimension three since the 1940s is settled. A Lean proof shifts the remaining question from “is the argument correct?” to “does the formal statement say what the conjecture says?”. Nobody has published an answer to that yet. The Formal Conjectures issue that would mark the problem solved was still open on 29 Oct, and we found no public comment by a topologist on either proof.
What is disputed or not yet verified
| Verification | OpenAI manuscript unrefereed and unformalized; the separate proof has a Lean 4 formalization registered on Palomar (statement faithfulness not independently assessed) |
|---|
Sources
8 sources from 4 sites. Numbers match the chips in the text.
8 sources: 4 primary, 4 reactions
Primary
- OpenAI: The Hilbert–Smith conjecture in every finite dimension (23 Sept 2026, PDF)github.com, paper
- adbrw/HS_proof: Integral tail signatures and the Hilbert–Smith conjecture, with Lean 4 proofgithub.com, code
- Palomar registry: PALOMAR-2026-10-16-000006 (Hilbert–Smith and p-adic exclusion with second countability)palomar-registry.org, code
- Deicyde/hilbert-smith: Lean 4 blueprint of OpenAI’s proof (in progress)github.com, code
Reactions
- Formal Conjectures issue #6914: the Hilbert–Smith conjecture is truegithub.com, discussion
- oai-math-revised: community notes on the Hilbert–Smith manuscriptgithub.com, discussion
- MathOverflow: How to complete an AI generated verification of an OpenAI proof for the Hilbert-Smith Conjecture (closed)mathoverflow.net, discussion
- Terence Tao (2011): The Hilbert-Smith conjecture (background)terrytao.wordpress.com, discussion
Changes
- Filed (families 251–378; manuscript, CONTENTS, oai-math-revised notes, adbrw/HS_proof paper and README, Palomar API, Formal Conjectures #6914, MathOverflow API)