Lean: Carrier-LCM discharge work, add pinned Lean CI target, and update docs - #72
Conversation
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Checkout | ||
| uses: actions/checkout@v4 | ||
|
|
||
| - name: Install elan using formal/lean-toolchain | ||
| run: | | ||
| curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ | ||
| | sh -s -- -y --default-toolchain "$(cat formal/lean-toolchain)" | ||
|
|
||
| - name: Cache Lake packages | ||
| uses: actions/cache@v4 | ||
| with: | ||
| path: formal/.lake | ||
| key: carrier-lcm-lake-${{ hashFiles('formal/lean-toolchain', 'formal/lakefile.lean', 'formal/lake-manifest.json') }} | ||
|
|
||
| - name: Build Ucns.CarrierLcm with pinned toolchain | ||
| run: | | ||
| source $HOME/.elan/env | ||
| cd formal | ||
| lake build Ucns.CarrierLcm | ||
|
|
||
| - name: Reject admit/axiom in formal Lean files | ||
| run: | | ||
| if git grep -n -E '\b(admit|axiom)\b' -- 'formal/Ucns/*.lean'; then | ||
| echo 'admit/axiom found in formal Lean files' | ||
| exit 1 | ||
| fi | ||
|
|
||
| - name: Report sorry leaves without certifying them | ||
| run: | | ||
| echo 'Open executable sorry leaves:' | ||
| git grep -n -E '\bsorry\b' -- 'formal/Ucns/*.lean' || true |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 0330f19ec7
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
|
||
| - name: Reject admit/axiom in formal Lean files | ||
| run: | | ||
| if git grep -n -E '\b(admit|axiom)\b' -- 'formal/Ucns/*.lean'; then |
There was a problem hiding this comment.
When an admit or axiom is added to the library root formal/Ucns.lean, this guard does not check it: I verified the pathspec with git ls-files -- 'formal/Ucns/*.lean', and it only matches formal/Ucns/CarrierLcm.lean, formal/Ucns/Core.lean, and formal/Ucns/TheoremN.lean. Since formal/Ucns.lean is also a tracked Lean file and is the package root, the PR gate can pass while leaving an unchecked axiom/admit in the root module; include formal/*.lean or an explicit formal/Ucns.lean path in this scan.
Useful? React with 👍 / 👎.
| run: | | ||
| source $HOME/.elan/env | ||
| cd formal | ||
| lake build Ucns.CarrierLcm |
There was a problem hiding this comment.
In a fresh GitHub runner/cache miss, this target now imports Mathlib modules but goes directly from cache restore to lake build. I checked the mathlib README, which documents lake exe cache get for downloading cached build files and warns that skipping the cache makes the next build very slow; without that step the first PR run has to build imported Mathlib oleans locally instead of using the published cache, making this verifier prone to consuming a long CI slot or timing out.
Useful? React with 👍 / 👎.
| | Full frozen depth-2 domain | `IMPLEMENTED` + `TEST-BACKED` (not yet `DEFENDED` at spec level) | | ||
| | Depth-3 asymmetric (Theorem 9) | `TEST-BACKED` (6/6 empirical) | | ||
| | **Catalogue-sufficient completeness — all depths (Theorem N)** | **`DEFENDED` — proof drafted, awaiting external formal review** | | ||
| | **Catalogue-sufficient completeness — all depths (Theorem N)** | **`FRONTIER` — partially verified in Lean; remaining proof leaves under active discharge** | |
There was a problem hiding this comment.
This line now downgrades Theorem N to FRONTIER, but the canonical spec files that README sends reviewers to still claim the stronger status: ucns-spec.md:20 says Theorem N is DEFENDED — proof drafted, and ucns-theorem-n.md:149 says the all-depth theorem has a repaired proof. Anyone following the new README will still see the old defended claim, so the status correction is incomplete and can mislead external reviewers.
Useful? React with 👍 / 👎.
| a.den * ((n : Rat) * (z : Rat)).den := | ||
| den_normalize_dvd _ _ _ | ||
| have hprod : a.den * ((n : Rat) * (z : Rat)).den ∣ a.den := by | ||
| rw [hmul, Nat.mul_one] |
There was a problem hiding this comment.
After this rewrite the local goal is still a.den ∣ a.den; rw does not synthesize Nat.dvd_refl, so the hprod proof block leaves an unsolved goal and lake build Ucns.CarrierLcm will fail. Add an explicit reflexivity proof here, and apply the same fix to the later rw [hden_eq] block that similarly reduces to x ∣ x.
Useful? React with 👍 / 👎.
Motivation
sorry-scoped leaves.sorry/admit occurrences per-PR for reviewer visibility.Description
/.github/workflows/carrier-lcm-target.ymlthat installs the pinned Lean toolchain and runslake build Ucns.CarrierLcm, caches Lake packages, rejectsadmit|axiominformal/Ucns/*.lean, and reportssorryleaves.formal/Ucns/CarrierLcm.lean, including thelcmfold engine (dvd_foldl_lcm_acc,dvd_foldl_lcm,foldl_lcm_dvd),nMin_dvd_of_denoms_subset, denominator arithmetic lemmas (den_normalize_dvd,den_mul_nat_int_cast_eq_one,den_amod_dvd,den_maybeNormalize_dvd_of_dvd,den_add_dvd_lcm), themem_angleDenoms_iffbridge, host/Complete helpers, and constructiveslice_embedding_left/slice_embedding_rightproofs adapted to theCompletedomain; leave thecarrier_lcm_law_upperthreading proof assorry.formal/Ucns/Core.leanto use the recursiveComplete/HostNormalizedRec/NonemptyRecdomain predicates (theCompletepredicate is now the nominal domain used by slice lemmas) and adjust related comments and invariants.formal/lake-manifest.jsonwith required package entries (std,Qq,aesop,proofwidgets,Cli,importGraph,mathlib) to match the pinned Lake environment used by the proofs.README.mdandREVIEW_PACKET.mdto record the partial Lean verification status and to explicitly state the restricted cancellativity target and the current proof-frontier posture.Testing
lake build Ucns.CarrierLcmon PRs touchingformal/**with the pinned toolchain.admit/axiomtokens are present and will printsorryoccurrences for reviewer inspection.Codex Task