Audit Erdős 545 literal counterexamples

.github/workflows/erdos545-counterexample.yml

@@ -0,0 +1,105 @@
+# Copyright 2026 Dominic Dabish
+# Licensed under the Apache License, Version 2.0.
+
+name: Erdős 545 counterexample audit
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/erdos545-counterexample.yml'
+      - 'audits/erdos545-counterexample.md'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  verify:
+    name: kernel build and axiom audit
+    runs-on: ubuntu-latest
+    timeout-minutes: 90
+    steps:
+      - name: Checkout exact proof source
+        uses: actions/checkout@v6
+        with:
+          repository: DomTheDeveloper/formal-conjectures
+          ref: 30c256a6e19a7fe32976f675ffe6fbb9c743af0f
+          fetch-depth: 1
+
+      - name: Record exact commit
+        run: git rev-parse HEAD | tee "$RUNNER_TEMP/resolved-sha.txt"
+
+      - name: Install repository-pinned Lean
+        run: |
+          set -euo pipefail
+          curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Restore reusable Lean cache
+        id: lean-cache
+        uses: actions/cache/restore@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: erdos545-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: |
+            erdos545-${{ runner.os }}-
+
+      - name: Restore pinned Mathlib cache
+        if: steps.lean-cache.outputs.cache-matched-key == ''
+        run: |
+          set -euo pipefail
+          "$HOME/.elan/bin/lake" exe cache unpack || true
+          "$HOME/.elan/bin/lake" exe cache get
+
+      - name: Save reusable Lean cache
+        if: steps.lean-cache.outputs.cache-matched-key == ''
+        uses: actions/cache/save@v4
+        with:
+          path: |
+            .lake/packages
+            .lake/build
+          key: erdos545-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+
+      - name: Reject placeholders and trust shortcuts
+        run: |
+          set -euo pipefail
+          if grep -nE '\b(sorry|admit|native_decide|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|Lean\.(trustCompiler|ofReduce|ofReduceBool)' Scratch/Erdos545Counterexample.lean; then
+            echo 'Forbidden placeholder or trust shortcut found.' >&2
+            exit 1
+          fi
+
+      - name: Build repository
+        run: |
+          set -o pipefail
+          "$HOME/.elan/bin/lake" --wfail build \
+            2>&1 | tee "$RUNNER_TEMP/erdos545-build.log"
+
+      - name: Compile exact counterexample proof
+        run: |
+          set -o pipefail
+          : > "$RUNNER_TEMP/erdos545.log"
+          "$HOME/.elan/bin/lake" env lean Scratch/Erdos545Counterexample.lean \
+            2>&1 | tee "$RUNNER_TEMP/erdos545.log"
+
+      - name: Enforce axiom policy
+        run: |
+          set -euo pipefail
+          if grep -E 'sorryAx|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/erdos545.log"; then
+            echo 'Forbidden axiom or compiler-trust dependency detected.' >&2
+            exit 1
+          fi
+
+      - name: Upload Lean transcript
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos545-counterexample-${{ github.run_id }}
+          path: |
+            ${{ runner.temp }}/resolved-sha.txt
+            ${{ runner.temp }}/erdos545-build.log
+            ${{ runner.temp }}/erdos545.log
+          if-no-files-found: warn

audits/erdos545-counterexample.md

@@ -0,0 +1,15 @@
+# Erdős Problem 545 literal-counterexample audit
+
+This gate checks commit `30c256a6e19a7fe32976f675ffe6fbb9c743af0f` in
+`DomTheDeveloper/formal-conjectures`.
+
+The checked Lean file proves the specialized formula
+
+`R(K₂ ⊔ rK₁) = r + 2`
+
+for ordinary non-induced monochromatic graph copies, and derives the two
+isolated-vertex counterexamples to the statement in Formal Conjectures issue
+#782.
+
+The workflow rejects `sorry`, `admit`, `native_decide`, `unsafe`, custom axioms,
+and compiler-trust shortcuts, then runs `#print axioms` on the final theorems.