docs: retire issue-intake fallback copy after cutoff

.github/ISSUE_TEMPLATE/config.yml

@@ -2,10 +2,7 @@ blank_issues_enabled: true
 contact_links:
   - name: Submit a benchmark solution
     url: https://lean-lang.org/eval/submit/
-    about: Primary authenticated submission path from 2026-09-02T06:57:10Z.
-  - name: Submission issue fallback
-    url: https://github.com/leanprover/lean-eval-submissions/issues/new?template=submit.yml
-    about: Available through at least 2026-09-30T06:57:10Z and possibly longer.
+    about: Supported authenticated submission path.
   - name: Discussion on Zulip
     url: https://leanprover.zulipchat.com/#narrow/channel/583341-Model-comparisons-for-Lean/topic/LeanEval/with/594108910
     about: General questions and discussion about lean-eval happen in the #Model-comparisons-for-Lean > LeanEval topic on the Lean Zulip.

.github/ISSUE_TEMPLATE/problem-report.yml

@@ -13,12 +13,8 @@ body:
         is unprovable as stated, imports are missing, or the intended
         interpretation is ambiguous.
 
-        For submission instructions, use the primary authenticated path at
-        https://lean-lang.org/eval/submit/. The launch overlap starts at
-        2026-09-02T06:57:10Z. Issue intake remains available as a fallback through
-        at least 2026-09-30T06:57:10Z, no earlier than four weeks after the
-        overlap begins, and may stay open longer. Any closure will be announced
-        at least two weeks in advance.
+        For submission instructions, use the supported authenticated path at
+        https://lean-lang.org/eval/submit/.
 
         Scheduled release is recommended for authenticated intake, while you
         may keep accepted source private instead. Once selected, scheduled

.github/ISSUE_TEMPLATE/submit.yml

@@ -12,12 +12,7 @@ body:
 
         **https://lean-lang.org/eval/submit/**
 
-        That page is the primary authenticated submission path from
-        2026-09-02T06:57:10Z. Issue intake remains available as a fallback through
-        at least 2026-09-30T06:57:10Z, no earlier than four weeks after the
-        overlap begins, and may stay open longer:
-
-        **https://github.com/leanprover/lean-eval-submissions/issues/new?template=submit.yml**
+        That page is the supported authenticated submission path.
 
         Scheduled release is recommended for authenticated intake, while you
         may keep accepted source private instead. Once selected, scheduled
@@ -28,12 +23,12 @@ body:
 
         Nothing filed here will be evaluated or recorded on the leaderboard.
 
-        You can close this draft and follow one of the links above; there is
+        You can close this draft and follow the stable page above; there is
         nothing more to do in this repository.
   - type: checkboxes
     id: ack
     attributes:
       label: Acknowledgement
       options:
-        - label: I understand this repository does not accept submissions and I should follow the stable LeanEval submission page or its documented issue-intake fallback instead.
+        - label: I understand this repository does not accept submissions and I should follow the stable LeanEval submission page instead.
           required: true

README.md

@@ -295,20 +295,10 @@ For current instructions to **submit a solution**, start at the stable page:
 
 > **[lean-lang.org/eval/submit/](https://lean-lang.org/eval/submit/)**
 
-That page is the primary authenticated submission path from
-`2026-09-02T06:57:10Z`. The application itself is at
+That page is the supported authenticated submission path. The application itself is at
 `https://lean-eval-submission-server.lean-eval.workers.dev/`; this change of
 origin is expected.
 
-[Submission issue
-intake](https://github.com/leanprover/lean-eval-submissions/issues/new?template=submit.yml)
-remains available as a fallback through at least `2026-09-30T06:57:10Z`, four
-weeks after the overlap began. Conditional on stable operation, adequate
-adoption, no unresolved severity-high incident, and a reconciled final corpus,
-that is the planned retirement time. This notice was issued at
-`2026-09-02T23:06:35Z`, more than two weeks in advance. Retirement will be
-postponed if any gate is not satisfied.
-
 Scheduled release is recommended for authenticated intake, while submitters
 may keep accepted source private instead. Once selected, scheduled release
 cannot be changed back to private. Accepted source is published under the

SECURITY.md

@@ -6,7 +6,7 @@ untrusted submitter Lean code. This document explains the sandbox
 invariants, the comparator trust model, and the pinned-dependency policy
 that the whole evaluation pipeline rests on.
 
-The **submission pipeline** itself — issue intake, fetching submission
+The **submission pipeline** itself — authenticated intake, fetching submission
 source, the evaluation workflow, recording results, and the overall
 adversarial-submission threat model — lives in the submissions
 repository and is documented there:
@@ -33,7 +33,7 @@ The adversary is a submitter who controls a `Submission.lean` (and files
 under `Submission/`). The goal we resist here: **untrusted submitter Lean
 escaping comparator's sandbox, or comparator accepting a Solution that
 does not actually prove the Challenge.** The pipeline-level framing of
-the same adversary (issue intake, token handling, confidentiality) is in
+the same adversary (server intake, token handling, confidentiality) is in
 the submissions repo's `SECURITY.md`.
 
 The submitter does not control `Challenge.lean`, `Solution.lean`,

tests/python/test_issue_templates.py

@@ -0,0 +1,33 @@
+from __future__ import annotations
+
+import pathlib
+import unittest
+
+
+ROOT = pathlib.Path(__file__).resolve().parents[2]
+TEMPLATES = (
+    ROOT / ".github/ISSUE_TEMPLATE/config.yml",
+    ROOT / ".github/ISSUE_TEMPLATE/submit.yml",
+    ROOT / ".github/ISSUE_TEMPLATE/problem-report.yml",
+)
+
+
+class IssueTemplateTests(unittest.TestCase):
+    def test_submission_redirects_are_server_only(self) -> None:
+        for template in TEMPLATES:
+            with self.subTest(template=template.name):
+                text = template.read_text(encoding="utf-8")
+                self.assertIn("https://lean-lang.org/eval/submit/", text)
+                for retired_copy in (
+                    "lean-eval-submissions/issues/new",
+                    "issue intake",
+                    "issue-intake",
+                    "2026-09-02T06:57:10Z",
+                    "2026-09-30T06:57:10Z",
+                    "fallback through",
+                ):
+                    self.assertNotIn(retired_copy, text.lower())
+
+
+if __name__ == "__main__":
+    unittest.main()