From a6915d45eadec8475c47d342a02f9c621bb4536f Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 10:35:05 -0700 Subject: [PATCH 1/2] ci: audit the immutable Erdos 100 witness proof --- .../openai-erdos100-piepmeyer-audit.yml | 73 +++++++++++++++++++ 1 file changed, 73 insertions(+) create mode 100644 .github/workflows/openai-erdos100-piepmeyer-audit.yml diff --git a/.github/workflows/openai-erdos100-piepmeyer-audit.yml b/.github/workflows/openai-erdos100-piepmeyer-audit.yml new file mode 100644 index 0000000000..c3a7684c31 --- /dev/null +++ b/.github/workflows/openai-erdos100-piepmeyer-audit.yml @@ -0,0 +1,73 @@ +name: OpenAI Erdos 100 Piepmeyer witness audit + +on: + pull_request: + branches: [main] + paths: + - '.github/workflows/openai-erdos100-piepmeyer-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: erdos100-piepmeyer-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }} + restore-keys: erdos100-piepmeyer-${{ runner.os }}-${{ runner.arch }}- + - name: Fetch compiled dependencies + run: lake exe cache get + - name: Build current catalog module + run: lake build FormalConjectures.ErdosProblems.«100» + - name: Generate immutable proof-only source + run: | + curl -fsSL 'https://raw.githubusercontent.com/theaustinhatfield/formal-conjectures/solve-erdos-100-piepmeyer/FormalConjectures/ErdosProblems/100.lean' -o /tmp/Erdos100Historical.lean + test "$(git hash-object /tmp/Erdos100Historical.lean)" = 'db773dd78975db6da5aed05c05c6eff1a26112b5' + cat > /tmp/Erdos100PiepmeyerProof.lean <<'EOF' + import FormalConjectures.ErdosProblems.«100» + open Set Metric Filter Real + open scoped EuclideanGeometry + namespace Erdos100 + EOF + sed -n '82,$p' /tmp/Erdos100Historical.lean \ + | sed '$d' \ + | sed 's/theorem erdos_100_piepmeyer/theorem erdos_100_piepmeyer_kernel/' \ + >> /tmp/Erdos100PiepmeyerProof.lean + echo 'end Erdos100' >> /tmp/Erdos100PiepmeyerProof.lean + - 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/Erdos100PiepmeyerProof.lean + - name: Compile proof-only source + run: | + set -o pipefail + lake env lean /tmp/Erdos100PiepmeyerProof.lean 2>&1 | tee /tmp/erdos100-piepmeyer-build.log + - name: Audit exact theorem axioms + run: | + cp /tmp/Erdos100PiepmeyerProof.lean /tmp/Erdos100PiepmeyerAxioms.lean + sed -i '$d' /tmp/Erdos100PiepmeyerAxioms.lean + cat >> /tmp/Erdos100PiepmeyerAxioms.lean <<'EOF' + #print axioms Erdos100.erdos_100_piepmeyer_kernel + end Erdos100 + EOF + lake env lean /tmp/Erdos100PiepmeyerAxioms.lean 2>&1 | tee /tmp/erdos100-piepmeyer-axioms.log + ! grep -E 'sorryAx|Lean\.ofReduce|Lean\.ofReduceBool|Lean\.trustCompiler' /tmp/erdos100-piepmeyer-axioms.log + - uses: actions/upload-artifact@v4 + if: always() + with: + name: erdos100-piepmeyer-${{ github.run_id }} + path: | + /tmp/erdos100-piepmeyer-build.log + /tmp/erdos100-piepmeyer-axioms.log + if-no-files-found: warn From ac6d0f804114149b70673549d2d8494eeab9195c Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 10:45:44 -0700 Subject: [PATCH 2/2] =?UTF-8?q?ci:=20extract=20Erd=C5=91s=20100=20proof=20?= =?UTF-8?q?by=20declaration=20markers?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../openai-erdos100-piepmeyer-audit.yml | 29 ++++++++++++++----- 1 file changed, 21 insertions(+), 8 deletions(-) diff --git a/.github/workflows/openai-erdos100-piepmeyer-audit.yml b/.github/workflows/openai-erdos100-piepmeyer-audit.yml index c3a7684c31..59ffdc564d 100644 --- a/.github/workflows/openai-erdos100-piepmeyer-audit.yml +++ b/.github/workflows/openai-erdos100-piepmeyer-audit.yml @@ -34,17 +34,29 @@ jobs: run: | curl -fsSL 'https://raw.githubusercontent.com/theaustinhatfield/formal-conjectures/solve-erdos-100-piepmeyer/FormalConjectures/ErdosProblems/100.lean' -o /tmp/Erdos100Historical.lean test "$(git hash-object /tmp/Erdos100Historical.lean)" = 'db773dd78975db6da5aed05c05c6eff1a26112b5' - cat > /tmp/Erdos100PiepmeyerProof.lean <<'EOF' - import FormalConjectures.ErdosProblems.«100» + python3 - <<'PY' + from pathlib import Path + src = Path('/tmp/Erdos100Historical.lean').read_text() + start = src.index('lemma dist_sq_eq_sum') + end = src.rindex('end Erdos100') + body = src[start:end] + body = body.replace( + 'theorem erdos_100_piepmeyer', + 'theorem erdos_100_piepmeyer_kernel', + 1, + ) + body = '\n'.join( + line for line in body.splitlines() + if 'category research formally solved' not in line + ) + out = '''import FormalConjectures.ErdosProblems.«100» + /-! Exact proof-only replay of the nine-point Piepmeyer construction. -/ open Set Metric Filter Real open scoped EuclideanGeometry namespace Erdos100 - EOF - sed -n '82,$p' /tmp/Erdos100Historical.lean \ - | sed '$d' \ - | sed 's/theorem erdos_100_piepmeyer/theorem erdos_100_piepmeyer_kernel/' \ - >> /tmp/Erdos100PiepmeyerProof.lean - echo 'end Erdos100' >> /tmp/Erdos100PiepmeyerProof.lean + ''' + body + '\nend Erdos100\n' + Path('/tmp/Erdos100PiepmeyerProof.lean').write_text(out) + PY - name: Reject proof holes and trust escapes run: | set -euo pipefail @@ -68,6 +80,7 @@ jobs: with: name: erdos100-piepmeyer-${{ github.run_id }} path: | + /tmp/Erdos100PiepmeyerProof.lean /tmp/erdos100-piepmeyer-build.log /tmp/erdos100-piepmeyer-axioms.log if-no-files-found: warn