Dow–Tkachuk Question 4.8: pseudocomplete countable closures in force to be a -space
Dow and Tkachuk asked (Question 4.8): assume that the closure of is pseudocomplete for every countable . Must the Tychonoff space be a -space? Here is the space of continuous real-valued functions on with the topology of pointwise convergence, pseudocompleteness is in Oxtoby's sense (a sequence of -bases along which every closure-nested choice has nonempty intersection), and a -space is one in which every set is open.
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-assisted
- Method
- Argument
- Field
- General topology; $C_p$-theory
- Posed by
- Alan Dow and Vladimir V. Tkachuk, "Reflecting topological properties in closed separable subspaces", European Journal of Mathematics 11 (2025), Question 4.8
- Year posed
- 2025
- Years open
- 1y
- Solved
- 2026-10-12
- Model
- ChatGPT Astra (proof); Claude Opus 5.5 (Lean formalization)
- Vendor
- OpenAI; Anthropic
- Collaborators
- Lucas Alves de Almeida
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 8 / 100
- Disclosed cost
- $0
- Wikipedia
- No dedicated article
What was actually shown
Yes, in ZFC. The paper proves a stronger statement: if a Tychonoff space is not a -space, then contains a closed, separable, metrizable linear subspace that is not pseudocomplete. A closed separable subspace is the closure of a countable subset, so if all such closures are pseudocomplete, must be a -space. Dow and Tkachuk had shown this under the extra assumption that is functionally countable (their Theorem 3.10); the result removes that assumption. The companion Question 4.9 (whether must also be functionally countable) is not addressed.
What the AI did
The main idea came from the author, Lucas Alves de Almeida: instead of arguing directly from the hypothesis on countable closures, prove the stronger statement that if is not a -space, then contains a closed separable metrizable linear subspace which is not pseudocomplete. ChatGPT Astra (OpenAI) worked out the details and completed the argument. The author edited the manuscript and checked the literature. Claude Opus 5.5 (Anthropic) helped review the proof and typeset the paper, and produced the Lean 4 / Mathlib formalization. The repository's disclosure classifies the work as AI-assisted.
Verification
No independent mathematician has checked this yet. Checked by this site on 15 October 2026, not rebuilt. Question 4.8 was read in the open-access Dow-Tkachuk paper (Eur. J. Math. 11 (2025), Art. 5) and the statement matches; their paper assumes all spaces Tychonoff and defines pseudocompleteness by Oxtoby's sequences of pi-bases, with no extra regularity clause. The Lean headline question_4_8 in Question48.lean (commit 8b4c7d0, SHA-256 matching the repository's certificate) was read with its definitions: Cp X is the continuous functions as a subspace of the product X -> R (pointwise, not Mathlib's compact-open C(X, R)), closure is taken in Cp X, Pseudocomplete is exactly the paper's definition, and IsPSpace says countable intersections of open sets are open, equivalent to every G-delta being open. The hypothesis is CompletelyRegularSpace, weaker than Tychonoff, so the formal statement is if anything stronger. A grep of the file found no sorry, admit, axiom, native_decide, unsafe, opaque or implemented_by; the axiom list (propext, Classical.choice, Quot.sound) is the author's build output, not re-run here. The paper's short proof was also read and no gap was found; that is not an expert review. The formal statement was written in the same workflow as the proof and is not independently anchored.
Sources
- PaperPaper (PDF)
- Lean proofLean 4 formalization (Question48.lean)
- Problem recordDow and Tkachuk, Reflecting topological properties in closed separable subspaces (Question 4.8)
- DiscussionGitHub
Submitted by StormyGander827 on