Skip to content

check-proof-statements: flag asides in a theorem statement - #1368

Merged
d-morrison merged 1 commit into
mainfrom
claude/project-thread-5ek13a
Oct 30, 2026
Merged

d-morrison merged 1 commit into
mainfrom
claude/project-thread-5ek13a

Conversation

@d-morrison

Copy link
Copy Markdown
Collaborator

Requested by Ezra · project thread

Extends check-proof-statements so a statement also flags "without loss of generality", "moreover" and "furthermore", the asides Halmos says "do not belong in the statement of a theorem" ("How to Write Mathematics", 1970, section 10; text read). This is the check half of item 2 of psw#422; psw#426 already covers the reasoning words.

One regex alternation, same warn-only, diff-scoped engine, so no new action. Tests: three new cases (each aside flagged in a statement, an aside in the proof not flagged); suite 79 passed. Docs: reference page and a changelog fragment. No sweep.


Generated by Claude Code

Halmos says 'Without loss of generality' and 'Moreover' do not belong in
the statement of a theorem (psw#422 item 2).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019xfc9rJ1dxeJYK1Rqeo1rp
@github-actions

Copy link
Copy Markdown
Contributor

Claude finished review — View run


Review of PR #1368 at ac60a9fa65c64352bedf85140da1b369b0920d6c: Ready for merge, with no blocking findings. I read the PR live: it is open, not a draft, and its head is still that commit. I could not run the new tests because pytest isn't installed here, so the review is from reading the code and tests.

I could not check the Halmos quotation ("How to Write Mathematics", section 10). The project library at /mnt/project-files/books/ doesn't exist in this environment. A search of the Morrison-Lab/mlr books/ directory was denied. The changelog, docstring and message all rely on that quotation. If it matters, someone with access should confirm it, and the book should be added to the library and mlr if it is missing from either.

The change adds "without loss of generality", "moreover" and "furthermore" to REASONING_RE in check-proof-statements/check-proof-statements.py. The scan path is unchanged and the new tests match its output.

Minor, non-blocking:

  • A phrase wrapped across a line break is missed.
  • A double space inside the phrase appears verbatim in the message.

Verdict

Ready for merge

Structured Review Data (JSON)
{
  "schema_version": "1.1",
  "reviewer": "claude",
  "commit_sha": "ac60a9fa65c64352bedf85140da1b369b0920d6c",
  "verdict": "CLEAN",
  "findings": [],
  "detailed_assessment": "The REASONING_RE change in check-proof-statements.py adds three aside phrases and feeds the unchanged scan path; new parametrized tests match the lowercased group output.",
  "holistic_assessment": "Docs, changelog fragment and docstring agree with the behavior; the check stays warn-only and diff-scoped, so regression risk is low. Tests could not be run here because pytest is not installed."
}

Stopping Point: Not a clean stopping point / work remains queued: session not done; this is a review-only run, so the review is posted by the harness. The Halmos quotation is unchecked because the book library was unavailable and the mlr listing was denied.

Reviewed commit: ac60a9f

@github-actions

Copy link
Copy Markdown
Contributor

💰 Cost: $0.7808 (review) — run

@github-actions

github-actions Bot commented Oct 30, 2026 •

Copy link
Copy Markdown
Contributor
PR Preview Action v1.8.1
Preview removed because the pull request was closed.

2026-10-30 00:09 UTC

@d-morrison
d-morrison merged commit 010d187 into main Oct 30, 2026
144 checks passed
@d-morrison
d-morrison deleted the claude/project-thread-5ek13a branch October 30, 2026 00:09

Copy link
Copy Markdown
Collaborator Author

Merged as 010d187 under gha's standing merge grant: all 144 checks on head ac60a9f passed or were skipped (read from the paged check-runs endpoint), the review on that head was Ready for merge, and the PR was mergeable.

Two gates were not run. check-pr-fully-clean.py can't run in the cloud session, and no cross-harness reviewer was run on this head. The change is one regex alternation in a warn-only check.

The v3 tag has not slid; psw's new prose rule depends on it.


Generated by Claude Code

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants