Add Python CI + Theorem N (Lean) formalization scaffold - #42
Merged
Merged
Conversation
…formalization Add a minimal GitHub Actions workflow that runs the ucns_recursive unittest suite on Python 3.11, path-scoped to Python sources so it does not trigger on front-end/HTML work. Add a Lean 4 scaffold under formal/ with sorry-backed stub statements for the Theorem N family. https://claude.ai/code/session_01Dz9UKMLXExfvk3XCY6mG7W
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Two independent additions:
1. Python CI workflow (
.github/workflows/ci.yml)A minimal GitHub Actions workflow: checkout, set up Python 3.11,
python -m pip install -e .[dev](thedevextra exists inpyproject.toml), thenpython -m unittest discover ucns_recursive/tests/ -v.It is path-scoped to Python sources via
paths:on bothpushandpull_request(ucns/**,ucns_recursive/**,tests/**,pyproject.toml, and the workflow file itself). It will not run on theexamples/visualizationfront-end/HTML work, so it won't collide with the separate Codex visualizer effort.2. Theorem N formalization scaffold (
formal/)A Lean 4 scaffold for eventually machine-checking the UCNS completeness results:
formal/README.md— status, layout, and the proof-status non-transfer discipline.formal/lean-toolchain— pinsleanprover/lean4:v4.7.0.formal/lakefile.lean— minimal Lake packageUcns.formal/Ucns/TheoremN.lean— stub statements (eachtheorem ... := sorry, with docstrings) for depth-1 restricted completeness, the depth-2 oracle result (Lemma 7), and catalogue-sufficient completeness (Theorem N). Claims are drawn fromucns-theorem-n.md.The formal scaffold is
sorry-backed and proves nothing yet. Per the non-transfer discipline documented informal/README.md, asorry-backed statement confers no DEFENDED status to any consumer repository; status is FRONTIER / awaiting external formal review.Constraints honored
README.mduntouched.examples/touched..gitignorechanges were needed.https://claude.ai/code/session_01Dz9UKMLXExfvk3XCY6mG7W
Generated by Claude Code