From fec1e7c6c256f80db303524eae44808d63a7deab Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sat, 25 Jul 2026 18:23:43 -0700 Subject: [PATCH 1/4] =?UTF-8?q?ci:=20add=20Erd=C5=91s=20545=20counterexamp?= =?UTF-8?q?le=20audit?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/workflows/erdos545-counterexample.yml | 98 +++++++++++++++++++ 1 file changed, 98 insertions(+) create mode 100644 .github/workflows/erdos545-counterexample.yml diff --git a/.github/workflows/erdos545-counterexample.yml b/.github/workflows/erdos545-counterexample.yml new file mode 100644 index 00000000..41ab245e --- /dev/null +++ b/.github/workflows/erdos545-counterexample.yml @@ -0,0 +1,98 @@ +# 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: 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.log + if-no-files-found: warn From e7dcdc9b0079588bf4ebddf6cb1e6684cb2cfb76 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sat, 25 Jul 2026 18:23:56 -0700 Subject: [PATCH 2/4] =?UTF-8?q?docs:=20record=20Erd=C5=91s=20545=20audit?= =?UTF-8?q?=20target?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- audits/erdos545-counterexample.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 audits/erdos545-counterexample.md diff --git a/audits/erdos545-counterexample.md b/audits/erdos545-counterexample.md new file mode 100644 index 00000000..f279164c --- /dev/null +++ b/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. From 34f6bb732317223e13829288ce66e6fb37a0dac9 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sat, 25 Jul 2026 18:28:35 -0700 Subject: [PATCH 3/4] =?UTF-8?q?ci:=20build=20repository=20utility=20before?= =?UTF-8?q?=20Erd=C5=91s=20545=20audit?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/workflows/erdos545-counterexample.yml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/workflows/erdos545-counterexample.yml b/.github/workflows/erdos545-counterexample.yml index 41ab245e..fe54e072 100644 --- a/.github/workflows/erdos545-counterexample.yml +++ b/.github/workflows/erdos545-counterexample.yml @@ -72,6 +72,11 @@ jobs: exit 1 fi + - name: Build repository utility module + run: | + set -euo pipefail + "$HOME/.elan/bin/lake" build FormalConjecturesUtil + - name: Compile exact counterexample proof run: | set -o pipefail From 813c5e0794d75d88c695b2cb67c62990c97a16cd Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sat, 25 Jul 2026 18:32:04 -0700 Subject: [PATCH 4/4] =?UTF-8?q?ci:=20run=20full=20repository=20build=20bef?= =?UTF-8?q?ore=20Erd=C5=91s=20545=20audit?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/workflows/erdos545-counterexample.yml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/.github/workflows/erdos545-counterexample.yml b/.github/workflows/erdos545-counterexample.yml index fe54e072..42c28418 100644 --- a/.github/workflows/erdos545-counterexample.yml +++ b/.github/workflows/erdos545-counterexample.yml @@ -72,10 +72,11 @@ jobs: exit 1 fi - - name: Build repository utility module + - name: Build repository run: | - set -euo pipefail - "$HOME/.elan/bin/lake" build FormalConjecturesUtil + set -o pipefail + "$HOME/.elan/bin/lake" --wfail build \ + 2>&1 | tee "$RUNNER_TEMP/erdos545-build.log" - name: Compile exact counterexample proof run: | @@ -99,5 +100,6 @@ jobs: 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