[acl2/acl2] e22f08: Added proof by Claude Code that a closed subspace ...

[MattKaufmann]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: e22f084640f11e94babe7971565e9e71b555350d
https://github.com/acl2/acl2/commit/e22f084640f11e94babe7971565e9e71b555350d
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-06-28 (Sun, 28 Jun 2026)

Changed paths:
A books/projects/set-theory/closed-subspace-is-compact.lisp

Log Message:
-----------
Added proof by Claude Code that a closed subspace of a compact topological space is compact.

Here is all that I gave to Claude Code Opus 4.8, max effort; it did
the rest automatically.

- the following two commands, in auto-mode; and
- the book shown below.

> Modify the ACL2 book ~/claude-code/acl2-mcp/work/csc/closed-subspace-is-compact.lisp so that it certifies, by adding supporting events and adding :props to the final event.

> Very nicely done! Now please attempt to clean up by removing hypotheses, members of :props, and lemmas.

Below is the book I gave to Claude. I could have changed the
include-book forms at the end since the new book is in the
projects/set-theory/topology/ directory, but I wanted to leave the
file exactly as it was produced by Claude.

; Copyright (C) 2026, Matt Kaufmann
; Written by Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.

(in-package "ZF")

(include-book "projects/set-theory/topology/subspace" :dir :system)
(include-book "projects/set-theory/topology/compact" :dir :system)

(defthmz closed-subspace-is-compact
(implies (and (tpp tp)
(compact tp)
(closed s tp))
(compact (subspace s tp))))



To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/testing