Gate proof leaves with Lean theorem signatures

.github/workflows/ci.yaml

@@ -43,6 +43,18 @@ jobs:
       - name: Check out
         uses: actions/checkout@v4
 
+      - name: Install pinned Lean toolchain
+        run: |
+          curl -sSf https://elan.lean-lang.org/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Restore mathlib cache and build Lean gate
+        run: |
+          lake update
+          lake exe cache get
+          lake build
+
       - name: Set up Python ${{ matrix.python-version }}
         uses: actions/setup-python@v5
         with:

.gitignore

@@ -7,3 +7,4 @@ __pycache__/
 .vscode/
 .DS_Store
 .coverage
+.lake/

KakeyaLeanGate.lean

@@ -0,0 +1 @@
+import KakeyaLeanGate.Prelude

KakeyaLeanGate/Prelude.lean

@@ -0,0 +1,9 @@
+import Mathlib
+
+/-!
+Minimal import target for AutoResearch theorem-signature validation.
+
+Generated signatures are compiled in temporary files importing this module.
+They may use `sorry` while their status is `FORMALIZED`; a proof obligation can
+only become `PROVED` after a separate no-sorry/no-axiom proof gate.
+-/

autoresearch/prefill/lean_gate.py

@@ -0,0 +1,122 @@
+"""Fail-closed Lean theorem-signature gate for proof obligations."""
+from __future__ import annotations
+
+import hashlib
+import re
+import subprocess
+import tempfile
+from dataclasses import dataclass
+from pathlib import Path
+
+
+_SIGNATURE_BLOCK = re.compile(
+    r"^### LEAN_SIGNATURE(?:\s+(\S+))?\s*$"
+    r"\s*```lean\s*(?P<source>.*?)```",
+    re.MULTILINE | re.DOTALL,
+)
+_FORBIDDEN = re.compile(
+    r"(^|\s)(?:import|axiom|opaque|unsafe|macro|syntax|elab|run_cmd|run_tac|"
+    r"set_option|def|abbrev|instance|structure|inductive|class|namespace|"
+    r"section|variable|open|attribute)\b|#(?:eval|check|print|reduce)|"
+    r"\b(?:IO|System|FilePath)\b",
+    re.MULTILINE,
+)
+
+
+@dataclass(frozen=True)
+class LeanSignatureResult:
+    source: str
+    signature_hash: str
+    ok: bool
+    error: str = ""
+
+
+def extract_lean_signature_blocks(text: str) -> list[tuple[str, str]]:
+    return [
+        ((match.group(1) or "").strip(), match.group("source").strip())
+        for match in _SIGNATURE_BLOCK.finditer(text)
+    ]
+
+
+def _signature_only(source: str) -> str:
+    match = re.search(r"\s*:=\s*by\b", source)
+    return source[:match.start()].strip() if match else source.strip()
+
+
+def validate_lean_signature(
+    source: str,
+    *,
+    project_root: Path,
+    timeout_s: float = 30.0,
+) -> LeanSignatureResult:
+    source = source.strip()
+    if not source:
+        return LeanSignatureResult("", "", False, "empty Lean signature")
+    if len(source) > 12_000:
+        return LeanSignatureResult("", "", False, "Lean signature too large")
+    if _FORBIDDEN.search(source):
+        return LeanSignatureResult(
+            source,
+            "",
+            False,
+            "forbidden Lean command in generated signature",
+        )
+    declarations = re.findall(r"^\s*theorem\s+([A-Za-z_][\w']*)", source, re.MULTILINE)
+    if len(declarations) != 1:
+        return LeanSignatureResult(
+            source,
+            "",
+            False,
+            "expected exactly one theorem declaration",
+        )
+    if not re.search(r"\s*:=\s*by\b", source):
+        return LeanSignatureResult(
+            source,
+            "",
+            False,
+            "theorem signature must end with `:= by` proof scaffold",
+        )
+    signature = " ".join(_signature_only(source).split())
+    signature_hash = hashlib.sha256(signature.encode()).hexdigest()
+    content = (
+        "import KakeyaLeanGate\n\n"
+        "set_option autoImplicit false\n\n"
+        + source
+        + "\n"
+    )
+    try:
+        with tempfile.NamedTemporaryFile(
+            mode="w",
+            suffix=".lean",
+            encoding="utf-8",
+            delete=False,
+        ) as handle:
+            handle.write(content)
+            path = Path(handle.name)
+        completed = subprocess.run(
+            ["lake", "env", "lean", str(path)],
+            cwd=project_root,
+            capture_output=True,
+            text=True,
+            timeout=timeout_s,
+            check=False,
+        )
+    except (OSError, subprocess.TimeoutExpired) as exc:
+        return LeanSignatureResult(
+            source,
+            signature_hash,
+            False,
+            f"Lean invocation failed: {type(exc).__name__}: {exc}",
+        )
+    finally:
+        if "path" in locals():
+            path.unlink(missing_ok=True)
+    if completed.returncode != 0:
+        error = (completed.stderr or completed.stdout).strip()
+        return LeanSignatureResult(
+            source,
+            signature_hash,
+            False,
+            f"Lean typecheck failed: {error[-2000:]}",
+        )
+    return LeanSignatureResult(source, signature_hash, True)

autoresearch/prefill/program.md

@@ -86,6 +86,13 @@ new assumption, narrower domain, or falsifiable conclusion. Existing semantic
 duplicates and all descendants beneath them are retained for audit but marked
 `REJECTED_DUPLICATE`; they are not pending leaves and do not reset stagnation.
 
+Every proposed minimum leaf must include one safe Lean theorem signature with
+explicit typed variables, hypotheses, and conclusion. The host compiles it
+against pinned Lean/mathlib before persistence and records `FORMALIZED` plus a
+signature hash. Missing, unsafe, ill-typed, or duplicate signatures reject the
+child. `FORMALIZED` is not `PROVED`: closure still requires a separate proof
+with no `sorry` and no added axioms.
+
 Do not optimize output wording, scores, prizes, or other proof-irrelevant
 content. Prefill performance is a tertiary objective after mathematical
 decomposition progress, while preserving the complete semantic contract.

lake-manifest.json

@@ -0,0 +1,96 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.32.0-rc1",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "f3f26cc72646205ca167117487c008ee1dafe816",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "41f407a8e85b0fdc00910633a8f14754139b63f4",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "e6518a674e62de322b8f79eebeda7bcae2a36bc3",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "954dbc9873f3b4534dc9896604593406d0383520",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.32.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "kakeya_lean_gate",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

lakefile.lean

@@ -0,0 +1,11 @@
+import Lake
+
+open Lake DSL
+
+package «kakeya_lean_gate»
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.32.0-rc1"
+
+@[default_target]
+lean_lib KakeyaLeanGate

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.32.0-rc1