From 1b5d57bed3290865b77e9fa8f84dd6a0d559e000 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Sat, 4 Jul 2026 10:20:45 -0500
Subject: [PATCH] chore(container): rebuilt silver-autoproof with 5-check
 pipeline

- Containerfile: COPY prove.py, verify_lean.py, frozen_template/ into image
- Systemd service: targets ComplexProjectiveSpace.lean (2 sorries)
- verify_lean.py: scoped banned keyword check (target module only, not entire formal/)
---
 Containerfile | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 Containerfile

diff --git a/Containerfile b/Containerfile
new file mode 100644
index 00000000..58a10a10
--- /dev/null
+++ b/Containerfile
@@ -0,0 +1,26 @@
+FROM docker.io/runpod/autoresearch:1.0.7-cuda1281-ubuntu2204
+
+# Install Lean 4 toolchain
+RUN curl -sSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh && \
+    sh /tmp/elan-init.sh -y --default-toolchain none && \
+    rm /tmp/elan-init.sh
+
+ENV ELAN_HOME=/root/.elan
+ENV PATH=$ELAN_HOME/bin:$PATH
+
+# Install SilverSight toolchain
+COPY SilverSight/lean-toolchain /tmp/lean-toolchain
+RUN elan toolchain install $(cat /tmp/lean-toolchain) && \
+    elan default $(cat /tmp/lean-toolchain) && \
+    rm /tmp/lean-toolchain
+
+# Copy autoresearch scripts (prove.py with 5-check pipeline, verify_lean.py)
+COPY autoresearch/prove.py /opt/autoresearch/prove.py
+COPY autoresearch/verify_lean.py /opt/autoresearch/verify_lean.py
+COPY autoresearch/frozen_template/ /opt/autoresearch/frozen_template/
+
+# Install Python deps
+RUN pip install requests 2>/dev/null || true
+
+WORKDIR /root/SilverSight
+ENTRYPOINT ["/bin/bash", "-c"]