Compact-range Vietoris powers: from to all countable ordinals above
Question 1 on page 11 of Christopher Caruvana and Jared Holshouser, An Adaptation of the Vietoris Topology for Ordered Compact Sets (arXiv:2507.17936v3), asks whether is -compact or Lindelöf for , explicitly singling out . Here the carrier consists of arbitrary functions with actual compact image, equipped with the paper’s Vietoris-power topology; for countable ordinals the default index is .
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI co-developed
- Method
- Argument
- Field
- General topology; covering and selection properties
- Posed by
- Christopher Caruvana and Jared Holshouser, Question 1, p. 11, An Adaptation of the Vietoris Topology for Ordered Compact Sets, arXiv:2507.17936v3
- Year posed
- 2025
- Years open
- 1y
- Solved
- 2026
- Model
- ChatGPT Astra
- Vendor
- OpenAI
- Collaborators
- Lucas Alves de Almeida
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 12 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
First, On the Vietoris Power of a Convergent Sequence settles the highlighted case : the space is second-countable and Lindelöf, but not -compact. Compact families of surjections have finite bounds on where each isolated value occurs; a delayed diagonal defeats every countable compact cover.
The stronger manuscript proves, for every , second countability and Lindelöfness, together with failure of both -compactness and the Menger property. It combines a countable-base argument, transfer through a closed copy of , and a direct fixed-compact-image diagonal. Explicit increasing open covers and the same diagonal defeat all finite selections, proving non-Mengerness.
Thus the original question has a positive answer for Lindelöfness and a negative answer for -compactness. “Proved” refers to this classification theorem.
What the AI did
According to the manuscripts’ AI disclosures, ChatGPT Astra contributed substantive new mathematics, as well as the Lean formalization and manuscript preparation, under Lucas Alves de Almeida’s direction. In the first stage, concerning , Astra performed almost all of the mathematical development, formalization and preparation, with Lucas checking and editing. In the stronger countable-ordinal work, Lucas proposed and guided the extension, directed the delayed-diagonal investigation, and requested the closed-subspace presentation; Astra developed the main general argument and performed the primary mathematical development, formalization, verification and manuscript preparation. The methods include a countable-base argument, finite coordinate bounds on compact families, a delayed diagonal, transfer through closed embeddings, and explicit open covers witnessing failure of the Menger property. The AI contribution was proof development, not merely formalization of an already known human result. “AI co-developed” is selected conservatively to reflect the human-directed workflow.
Verification
Updated 5 October 2026: Lucas Alves de Almeida supplied a screenshot of an email from Christopher Caruvana dated 3 October 2026. Caruvana writes: "I have finally taken a careful look at the documents and I agree with the conclusions." Lucas identifies the reviewed documents as covering both omega+1 and the general countable-ordinal case. The visible email discusses second countability, the closed non-sigma-compact surjection family, transfer to K(alpha,ord), and the Menger argument; it asks that the maximum index in that argument be taken from the E sets. This records human review and agreement with the written conclusions by a coauthor of the paper posing the question. It is private correspondence reported with a screenshot, not a published referee report, and does not establish that Caruvana audited the Lean code. Curator review of the verification tier and a change from Candidate to Resolved have been requested. Separately, the 30 September recheck of d2e73e4 compiled all eight original modules and FullAudit with Lean 4.19.0 and pinned mathlib. All six axiom lists contain only propext, Classical.choice and Quot.sound. Fresh project outputs and unchanged sources were checked; compiled dependencies were reused. The direct diagonal formally proves the general result, including non-Mengerness. Abstract closed-subspace transfer is not separately formalized. Full logs and scope remain linked below.
Sources
- PaperFirst stage: On the Vietoris Power of a Convergent Sequence
- Lean proofProof manuscript on GitHub with reproducible Lean 4 formalizationRepository and reproducible Lean verificationEarlier omega+1 repositoryComplete modular Lean recheck: report, logs and hashes (30 September 2026)
- Lean statementPrincipal formal theorem: ordinal_full
- Problem recordOriginal Question 1, page 11 (arXiv v3)
- OtherLean verification certificate and scopeFormalization scope and reproduction instructions
Submitted by StormyGander827 on
Request to the curators: please reassess Candidate (review pending) and consider marking this result Resolved, and update the human-verification classification. Christopher Caruvana, coauthor of the paper posing Question 1, wrote to Lucas Alves de Almeida on 3 October 2026 that he had carefully examined the documents and agreed with the conclusions. Lucas supplied a screenshot and confirms the documents cover both the omega+1 and general countable-ordinal cases. The email discusses the closed-subspace transfer and the Menger argument, including taking the maximum index from the E sets. This is human review of the written mathematical conclusions; it is not claimed to be a Lean-code audit or journal peer review. The existing complete modular Lean recheck and its evidence remain linked in the entry.