---
id: "2026-10-06-openai-hilbert-smith-conjecture-claim"
url: "https://postcutoff.com/e/2026-10-06-openai-hilbert-smith-conjecture-claim/"
as_of: "2026-10-30T13:42:00+01:00"
date: "2026-10-06"
date_precision: day
category: science
importance: 5
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 8
editor: human editor
human_review: null
version: "2026-10-29"
---

As of: 2026-10-30 13:42 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-06-openai-hilbert-smith-conjecture-claim/

# Hilbert–Smith conjecture claimed by OpenAI, Lean-checked by a separate AI proof

Full title: OpenAI's release claims the Hilbert–Smith conjecture in every dimension; a separate AI-agent proof of the same conjecture is Lean-checked and registered on Palomar

"The Hilbert–Smith conjecture in every finite dimension" (OpenAI, 23 Sept 2026, released 6 Oct, family 304) claims that every locally compact second-countable group acting faithfully and continuously on a connected finite-dimensional manifold is a Lie group, by excluding faithful actions of the p-adic integers. Known before: dimensions ≤ 3 (Pardon 2013 for three-manifolds) and Lipschitz or quasiconformal actions. No Lean proof is in the release. Separately, GitHub user adbrw posted "Integral tail signatures and the Hilbert–Smith conjecture" by "A. Dabrowski's AI agents" (8 Oct, 17 pages, written with Opus 5.5 and GPT 6.1), with a Lean 4 proof registered on Palomar (PALOMAR-2026-10-16-000006). No published expert assessment of either.

## 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)

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 159 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 98 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 189 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 128 days after its cutoff

## Sources

1. [OpenAI: The Hilbert–Smith conjecture in every finite dimension (23 Sept 2026, PDF)](https://github.com/openai/math/blob/main/preprints/The-Hilbert-Smith-conjecture-in-every-finite-dimension-September-23-2026/paper.pdf) (github.com, paper)
2. [adbrw/HS_proof: Integral tail signatures and the Hilbert–Smith conjecture, with Lean 4 proof](https://github.com/adbrw/HS_proof) (github.com, code)
3. [Palomar registry: PALOMAR-2026-10-16-000006 (Hilbert–Smith and p-adic exclusion with second countability)](https://palomar-registry.org/entry?id=PALOMAR-2026-10-16-000006&version=1) (palomar-registry.org, code)
4. [Deicyde/hilbert-smith: Lean 4 blueprint of OpenAI's proof (in progress)](https://github.com/Deicyde/hilbert-smith) (github.com, code)
5. [Formal Conjectures issue #6914: the Hilbert–Smith conjecture is true](https://github.com/google-deepmind/formal-conjectures/issues/6914) (github.com, discussion)
6. [oai-math-revised: community notes on the Hilbert–Smith manuscript](https://github.com/mathcommunity/oai-math-revised/blob/main/preprints/The-Hilbert-Smith-conjecture-in-every-finite-dimension-September-23-2026/AGENT_NOTES.md) (github.com, discussion)
7. [MathOverflow: How to complete an AI generated verification of an OpenAI proof for the Hilbert-Smith Conjecture (closed)](https://mathoverflow.net/questions/515824) (mathoverflow.net, discussion)
8. [Terence Tao (2011): The Hilbert-Smith conjecture (background)](https://terrytao.wordpress.com/2011/08/13/the-hilbert-smith-conjecture/) (terrytao.wordpress.com, discussion)

## Changes

- 2026-10-29 (filed): Created (families 251–378; manuscript, CONTENTS, oai-math-revised notes, adbrw/HS_proof paper and README, Palomar API, Formal Conjectures #6914, MathOverflow API)

## Related

- 2026-10-24: [oai-math-revised: mathematicians launch a community hub to revise OpenAI's AI-written math manuscripts (guest post on Tao's blog)](https://postcutoff.com/e/2026-10-24-oai-math-revised-community-hub/index.md)
- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)
- 2026-08-18: [Palomar launches: a registry of Lean-verified mathematics to curb misrepresented AI proof claims](https://postcutoff.com/e/2026-08-18-palomar-lean-registry/index.md)
- People: [Terence Tao](https://postcutoff.com/person/terence-tao/)