[codex] Remove PrimeCert bookkeeping

NOTICE

@@ -116,9 +116,6 @@ MIT permission notice that follows them.
   LeanPool/PolyaEnumerationTheorem   https://github.com/Luka-O/polya-enumeration-theorem
       Copyright (c) 2024 Luka-O
 
-  LeanPool/PrimeCert                 https://github.com/b-mehta/PrimeCert
-      Copyright (c) 2026 Bhavik Mehta
-
   LeanPool/QuasiBorelSpaces          https://github.com/YellPika/quasi-borel-spaces
       Copyright (c) 2025 Anthony Vandikas, Kiarash Sotoudeh
 

candidates/README.md

@@ -233,7 +233,6 @@ Do not edit the autogenerated section by hand.
 | 11 | [WuProver/MonomialOrderedPolynomial](https://github.com/WuProver/MonomialOrderedPolynomial) | Monomial ordered polynomial implementation in Lean4 | Apache-2.0 | v4.29.0-rc8 | 4,816 | 2026-04-10 | ✗ |  |
 | 11 | [Zetetic-Dhruv/formal-learning-theory-kernel](https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel) | Lean4 kernel for synthetic formalization and discovery of statistical learning theory. First and complete formalization… |  | v4.29.0-rc6 | 31,925 | 2026-04-29 | – | ✓ |
 | 11 | [znssong/SetTheory](https://github.com/znssong/SetTheory) | A formalization project of set theory and elementary embeddings in Lean 4. Includes a proof of Kunen's inconsistency th… | Apache-2.0 | v4.29.0-rc4 | 2,860 | 2026-05-10 | – | ✓ |
-| 10 | [b-mehta/PrimeCert](https://github.com/b-mehta/PrimeCert) | Formal prime certificates in Lean 4 | MIT | v4.32.0-rc1 | 1,936 | 2026-06-17 | ✓ | ✓ |
 | 10 | [Brunn-Minkowski-in-Lean/BrunnMinkowski](https://github.com/Brunn-Minkowski-in-Lean/BrunnMinkowski) |  |  | v4.19.0-rc2 | 1,731 | 2026-05-10 | – |  |
 | 10 | [calcu16/lean_complexity](https://github.com/calcu16/lean_complexity) | Complexity analysis in Lean |  | v4.5.0-rc1 | 5,595 | 2025-02-04 | – |  |
 | 10 | [DavePearce/LeanEVM](https://github.com/DavePearce/LeanEVM) | A toy implementation of the EVM in Lean4. | Apache-2.0 | v4.8.0-rc2 | 818 | 2024-05-29 | ✗ |  |

candidates/decisions.jsonl

@@ -407,7 +407,7 @@
 {"repo":"argumentcomputer/lurk","include":false,"category":"tool","confidence":"high","rationale":"Lean implementation of the Lurk language: parser, evaluator, CLI, scalar/Poseidon hashing — runtime/interpreter, no absorbable theorems."}
 {"repo":"argumentcomputer/yatimastdlib","include":false,"category":"tool","confidence":"medium","rationale":"Auxiliary stdlib for Yatima Inc tooling: hashmaps, byte arrays, FFI, string interner, polynomial benchmarks; utility infrastructure, not theorems."}
 {"repo":"axiommath/ramanujan-tau-misses-primes","include":true,"category":"mathlib","confidence":"high","rationale":"~5.8k LOC formalization accompanying paper on ABC implying Ramanujan tau misses primes; substantive number theory built on Mathlib."}
-{"repo":"b-mehta/primecert","include":true,"category":"mathlib","confidence":"high","rationale":"~1.9k LOC of Pocklington/Wieferich primality certificates with formal proofs over Mathlib; reusable number-theoretic lemmas plus elaborator."}
+{"repo":"b-mehta/primecert","include":false,"category":"mathlib","confidence":"high","rationale":"Substantive number-theory project, but upstream is actively maintained, so lean-pool should not vendor a duplicate copy."}
 {"repo":"beneficial-ai-foundation/floatspec","include":true,"category":"mathlib","confidence":"medium","rationale":"Lean 4 port of Coq Flocq: IEEE 754 floating-point spec with ~2200 defs/lemmas; 388 sorries but substantive completed proofs in Calc/Operations, Sqrt, Core."}
 {"repo":"cameronfreer/exchangeability","include":true,"category":"mathlib","confidence":"high","rationale":"de Finetti-Ryll-Nardzewski theorem formalization with 3 distinct proofs (martingale/L2/Koopman); 774 declarations, only 15 sorries; probability theory."}
 {"repo":"enricozb/logic","include":false,"category":"educational","confidence":"high","rationale":"Follow-along of textbook 'A Concise Introduction to Mathematical Logic'; status notes 'currently formalizing chapter 1 section 5'; learning project."}

candidates/manual.txt

@@ -117,7 +117,6 @@ https://github.com/AydenLamp/FinDFA
 https://github.com/ayhon/iris-loogle
 https://github.com/b-mehta/ExponentialRamsey
 https://github.com/b-mehta/HighlyAbundant
-https://github.com/b-mehta/PrimeCert
 https://github.com/badly-drawn-wizards/impdf
 https://github.com/badly-drawn-wizards/noperthedron
 https://github.com/badly-drawn-wizards/sqlean
@@ -454,7 +453,6 @@ https://github.com/katydid/symbolic-automatic-derivatives
 https://github.com/katzenpost/lean-ffi
 https://github.com/kbuzzard/IISc-experiments
 https://github.com/kbuzzard/MweSkeletons
-https://github.com/kckennylau/PrimeCert
 https://github.com/kencyke/quantum-system
 https://github.com/kevinsullivan/cs2120f24
 https://github.com/Kha/do-supplement

python/lean_pool/pr_advisory.py

@@ -322,6 +322,13 @@ def update_pr_advisory(
     rows = advisory_rows_for_pr(
         repo_full_name, pr_number, metadata_cache=metadata_cache
     )
+    if not rows:
+        if dry_run:
+            print(
+                "[dry-run] Would skip advisory comment on "
+                f"PR #{pr_number}: no project metadata changes"
+            )
+        return "skipped"
     return post_sticky_comment(
         repo_full_name,
         pr_number,

python/tests/test_pr_advisory.py

@@ -19,6 +19,7 @@
     post_sticky_comment,
     project_changes,
     render_comment,
+    update_pr_advisory,
 )
 
 
@@ -193,3 +194,33 @@ def fake_run_gh(*args: str, stdin: str | None = None) -> str:
     assert action == "updated"
     assert calls[1][0][:3] == ("api", "-X", "PATCH")
     assert json.loads(calls[1][1] or "{}")["body"].endswith("new")
+
+
+def test_update_pr_advisory_skips_pr_without_project_changes(
+    monkeypatch: pytest.MonkeyPatch,
+) -> None:
+    """PRs without project metadata changes do not need a sticky comment."""
+    posted = False
+
+    def fake_rows(
+        repo_full_name: str,
+        pr_number: int,
+        *,
+        metadata_cache: dict[str, UpstreamMetadata] | None = None,
+    ) -> list[AdvisoryRow]:
+        assert repo_full_name == "acme/pool"
+        assert pr_number == 7
+        return []
+
+    def fake_post(*args: object, **kwargs: object) -> str:
+        nonlocal posted
+        posted = True
+        return "created"
+
+    monkeypatch.setattr(pr_advisory, "advisory_rows_for_pr", fake_rows)
+    monkeypatch.setattr(pr_advisory, "post_sticky_comment", fake_post)
+
+    action = update_pr_advisory("acme/pool", 7)
+
+    assert action == "skipped"
+    assert not posted