[acl2/acl2] b7c01a: Added a proof generated fully automatically by Cla...

[MattKaufmann]

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

Changed paths:
M books/projects/set-theory/topology/compact-is-normal.lisp

Log Message:
-----------
Added a proof generated fully automatically by Claude Code (Opus 4.8, max effort), that a compact regular space is normal (and hence, based on an existing result, that a compact Hausdorff space is normal).

I've annotated compact-is-normal.lisp to make it clear which part was
written by Claude Code, which was essentialy all of it other than the
problem statement.

The proof takes advantage of a bug fix that I installed before my
preceding commit, which I forgot to report then. The bug was in the
definition of normal (really a typo; I had defined normal using the
appropriate notion, set-set-separable, but mistakenly used
point-set-separable instead. This bug came to my attention (before
the preceding commit) when Claude Code pointed it out to me.

The result is a standard, basic result in undergraduate topology, but
I'm impressed that Claude could lead ACL2 to a proof of it, without my
giving it any hints. There is a substantial amount of quantifier
reasoning involved that I'm happy not to have done myself.



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

[acl2buildserver]

Branch: refs/heads/testing