From 1fa1e7e4686756807030767c576d0e16bc93d348 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sun, 26 Jul 2026 10:36:47 -0700
Subject: [PATCH 1/2] ci: audit the immutable Erdos 1084 dimension-one proof

---
 .../workflows/openai-erdos1084-d1-audit.yml   | 80 +++++++++++++++++++
 1 file changed, 80 insertions(+)
 create mode 100644 .github/workflows/openai-erdos1084-d1-audit.yml

diff --git a/.github/workflows/openai-erdos1084-d1-audit.yml b/.github/workflows/openai-erdos1084-d1-audit.yml
new file mode 100644
index 0000000000..f1357222c7
--- /dev/null
+++ b/.github/workflows/openai-erdos1084-d1-audit.yml
@@ -0,0 +1,80 @@
+name: OpenAI Erdos 1084 dimension-one audit
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/openai-erdos1084-d1-audit.yml'
+
+permissions:
+  contents: read
+
+jobs:
+  audit:
+    runs-on: ubuntu-latest
+    timeout-minutes: 60
+    steps:
+      - uses: actions/checkout@v6
+      - name: Install pinned current Lean toolchain
+        run: |
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - uses: actions/cache@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: erdos1084-d1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: erdos1084-d1-${{ runner.os }}-${{ runner.arch }}-
+      - name: Fetch compiled dependencies
+        run: lake exe cache get
+      - name: Build current catalog module
+        run: lake build FormalConjectures.ErdosProblems.«1084»
+      - name: Generate immutable proof-only source
+        run: |
+          curl -fsSL 'https://raw.githubusercontent.com/Sanexxxx777/formal-conjectures/9e4f3845be122a8fa3190d38543ebdd0a6f25605/FormalConjectures/ErdosProblems/1084.lean' -o /tmp/Erdos1084Historical.lean
+          test "$(git hash-object /tmp/Erdos1084Historical.lean)" = '771c6c62762fa9e970dd3d3c52e984d18db216d5'
+          python3 - <<'PY'
+          from pathlib import Path
+          src = Path('/tmp/Erdos1084Historical.lean').read_text()
+          start = src.index('namespace upper_d1')
+          end = src.index('/-- It is easy to check that $f_2(n) < 3n$. -/')
+          body = src[start:end]
+          body = body.replace(
+              'theorem erdos_1084.variants.upper_d1',
+              'theorem erdos_1084.variants.upper_d1_kernel',
+              1,
+          )
+          out = '''import FormalConjectures.ErdosProblems.«1084»
+          open Finset Filter Metric Real
+          open scoped EuclideanGeometry
+          namespace Erdos1084
+          ''' + body + '\nend Erdos1084\n'
+          Path('/tmp/Erdos1084D1Proof.lean').write_text(out)
+          PY
+      - name: Reject proof holes and trust escapes
+        run: |
+          set -euo pipefail
+          ! grep -nE '\b(sorry|admit)\b|native_decide|decide \+native|unsafe|axiom |Lean\.ofReduce|Lean\.ofReduceBool|Lean\.trustCompiler' /tmp/Erdos1084D1Proof.lean
+      - name: Compile proof-only source
+        run: |
+          set -o pipefail
+          lake env lean /tmp/Erdos1084D1Proof.lean 2>&1 | tee /tmp/erdos1084-d1-build.log
+      - name: Audit exact theorem axioms
+        run: |
+          cp /tmp/Erdos1084D1Proof.lean /tmp/Erdos1084D1Axioms.lean
+          sed -i '$d' /tmp/Erdos1084D1Axioms.lean
+          cat >> /tmp/Erdos1084D1Axioms.lean <<'EOF'
+          #print axioms Erdos1084.erdos_1084.variants.upper_d1_kernel
+          end Erdos1084
+          EOF
+          lake env lean /tmp/Erdos1084D1Axioms.lean 2>&1 | tee /tmp/erdos1084-d1-axioms.log
+          ! grep -E 'sorryAx|Lean\.ofReduce|Lean\.ofReduceBool|Lean\.trustCompiler' /tmp/erdos1084-d1-axioms.log
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: erdos1084-d1-${{ github.run_id }}
+          path: |
+            /tmp/erdos1084-d1-build.log
+            /tmp/erdos1084-d1-axioms.log
+          if-no-files-found: warn

From 8bd9c48b60533cfbeb50c60d28e893a6c7ef3a9d Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sun, 26 Jul 2026 10:46:34 -0700
Subject: [PATCH 2/2] =?UTF-8?q?ci:=20preserve=20full=20scoped=20imports=20?=
 =?UTF-8?q?for=20Erd=C5=91s=201084=20replay?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/openai-erdos1084-d1-audit.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/openai-erdos1084-d1-audit.yml b/.github/workflows/openai-erdos1084-d1-audit.yml
index f1357222c7..7b32150277 100644
--- a/.github/workflows/openai-erdos1084-d1-audit.yml
+++ b/.github/workflows/openai-erdos1084-d1-audit.yml
@@ -46,8 +46,9 @@ jobs:
               1,
           )
           out = '''import FormalConjectures.ErdosProblems.«1084»
+          /-! Exact proof-only replay of the one-dimensional unit-distance value. -/
           open Finset Filter Metric Real
-          open scoped EuclideanGeometry
+          open scoped EuclideanGeometry ENNReal
           namespace Erdos1084
           ''' + body + '\nend Erdos1084\n'
           Path('/tmp/Erdos1084D1Proof.lean').write_text(out)
@@ -75,6 +76,7 @@ jobs:
         with:
           name: erdos1084-d1-${{ github.run_id }}
           path: |
+            /tmp/Erdos1084D1Proof.lean
             /tmp/erdos1084-d1-build.log
             /tmp/erdos1084-d1-axioms.log
           if-no-files-found: warn