From ba1f1ecedf0200984547699e06f4a7eda0452801 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 10:44:46 -0700 Subject: [PATCH 1/7] Add targeted A317940 initial-value audit --- .github/workflows/a317940-initial-values.yml | 54 ++++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100644 .github/workflows/a317940-initial-values.yml diff --git a/.github/workflows/a317940-initial-values.yml b/.github/workflows/a317940-initial-values.yml new file mode 100644 index 00000000..772df87e --- /dev/null +++ b/.github/workflows/a317940-initial-values.yml @@ -0,0 +1,54 @@ +name: A317940 initial values exact Lean audit + +on: + push: + branches: [main] + paths: ['.github/workflows/a317940-initial-values.yml'] + pull_request: + branches: [main] + paths: ['.github/workflows/a317940-initial-values.yml'] + +permissions: + contents: read + +jobs: + verify: + runs-on: ubuntu-latest + timeout-minutes: 45 + steps: + - uses: actions/checkout@v6 + with: + repository: DomTheDeveloper/formal-conjectures + ref: a0752c4e330dd7013f69dd07c06f5bae8449376d + fetch-depth: 1 + - name: Install Lean + 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: a317940-initial-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }} + restore-keys: a317940-initial-${{ runner.os }}- + - name: Get Mathlib cache + run: lake exe cache get + - name: Reject target placeholders and trust shortcuts + run: | + awk '/theorem a_1/,/theorem f_nonnegative/' FormalConjectures/OEIS/317940.lean > /tmp/a317940-targets.lean + ! grep -E '(^|[^A-Za-z])(sorry|admit|native_decide|unsafe|axiom)([^A-Za-z]|$)|decide[[:space:]]*\+native' /tmp/a317940-targets.lean + - name: Compile exact canonical file + run: lake env lean FormalConjectures/OEIS/317940.lean + - name: Audit theorem axioms + run: | + cat > /tmp/A317940InitialAxioms.lean <<'EOF' + import FormalConjectures.OEIS.«317940» + #print axioms OeisA317940.a_1 + #print axioms OeisA317940.a_2 + #print axioms OeisA317940.a_3 + #print axioms OeisA317940.a_4 + #print axioms OeisA317940.a_5 + EOF + lake env lean /tmp/A317940InitialAxioms.lean | tee /tmp/a317940-initial-axioms.log + ! grep -E 'sorryAx|Lean\.ofReduceBool|Lean\.trustCompiler' /tmp/a317940-initial-axioms.log From 195b4d4e1db4272435ee701b6e20fa00a36e5519 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 10:47:49 -0700 Subject: [PATCH 2/7] Upload targeted Lean compiler diagnostics --- .github/workflows/a317940-initial-values.yml | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/.github/workflows/a317940-initial-values.yml b/.github/workflows/a317940-initial-values.yml index 772df87e..825f2d59 100644 --- a/.github/workflows/a317940-initial-values.yml +++ b/.github/workflows/a317940-initial-values.yml @@ -39,8 +39,22 @@ jobs: awk '/theorem a_1/,/theorem f_nonnegative/' FormalConjectures/OEIS/317940.lean > /tmp/a317940-targets.lean ! grep -E '(^|[^A-Za-z])(sorry|admit|native_decide|unsafe|axiom)([^A-Za-z]|$)|decide[[:space:]]*\+native' /tmp/a317940-targets.lean - name: Compile exact canonical file - run: lake env lean FormalConjectures/OEIS/317940.lean + id: compile + continue-on-error: true + run: | + set -o pipefail + lake env lean FormalConjectures/OEIS/317940.lean 2>&1 | tee /tmp/a317940-compile.log + - name: Upload compiler log + if: always() + uses: actions/upload-artifact@v4 + with: + name: a317940-compile-log + path: /tmp/a317940-compile.log + - name: Fail on compiler error + if: steps.compile.outcome == 'failure' + run: exit 1 - name: Audit theorem axioms + if: steps.compile.outcome == 'success' run: | cat > /tmp/A317940InitialAxioms.lean <<'EOF' import FormalConjectures.OEIS.«317940» From 23480ff0bda531f4c9cb57ed30e09ab8721fd86e Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 10:51:41 -0700 Subject: [PATCH 3/7] Re-run A317940 audit after import fix --- .github/workflows/a317940-initial-values.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/a317940-initial-values.yml b/.github/workflows/a317940-initial-values.yml index 825f2d59..3d8ac3ff 100644 --- a/.github/workflows/a317940-initial-values.yml +++ b/.github/workflows/a317940-initial-values.yml @@ -19,7 +19,7 @@ jobs: - uses: actions/checkout@v6 with: repository: DomTheDeveloper/formal-conjectures - ref: a0752c4e330dd7013f69dd07c06f5bae8449376d + ref: 2e85f34e59caf25364f6aa06f639cc5021510fdc fetch-depth: 1 - name: Install Lean run: | From 4a57d7037945a8b7cc32732412b69e77e54f5aa7 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 10:55:37 -0700 Subject: [PATCH 4/7] Build the exact A317940 Lake module --- .github/workflows/a317940-initial-values.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/a317940-initial-values.yml b/.github/workflows/a317940-initial-values.yml index 3d8ac3ff..a86b275b 100644 --- a/.github/workflows/a317940-initial-values.yml +++ b/.github/workflows/a317940-initial-values.yml @@ -38,12 +38,12 @@ jobs: run: | awk '/theorem a_1/,/theorem f_nonnegative/' FormalConjectures/OEIS/317940.lean > /tmp/a317940-targets.lean ! grep -E '(^|[^A-Za-z])(sorry|admit|native_decide|unsafe|axiom)([^A-Za-z]|$)|decide[[:space:]]*\+native' /tmp/a317940-targets.lean - - name: Compile exact canonical file + - name: Compile exact canonical module id: compile continue-on-error: true run: | set -o pipefail - lake env lean FormalConjectures/OEIS/317940.lean 2>&1 | tee /tmp/a317940-compile.log + lake build 'FormalConjectures.OEIS.«317940»' 2>&1 | tee /tmp/a317940-compile.log - name: Upload compiler log if: always() uses: actions/upload-artifact@v4 From efa89edba49f423a70091bba84b00fcdc9dfe94c Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 11:01:26 -0700 Subject: [PATCH 5/7] Audit finite one-step A317940 proofs --- .github/workflows/a317940-initial-values.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/a317940-initial-values.yml b/.github/workflows/a317940-initial-values.yml index a86b275b..2f035ddb 100644 --- a/.github/workflows/a317940-initial-values.yml +++ b/.github/workflows/a317940-initial-values.yml @@ -19,7 +19,7 @@ jobs: - uses: actions/checkout@v6 with: repository: DomTheDeveloper/formal-conjectures - ref: 2e85f34e59caf25364f6aa06f639cc5021510fdc + ref: 5bde58f419e0b4022e515a3daf10304125ab138f fetch-depth: 1 - name: Install Lean run: | From b2268b728b2503c39ceadc6d9b274122a9661868 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 11:08:59 -0700 Subject: [PATCH 6/7] Audit exact A317940 divisor proof --- .github/workflows/a317940-initial-values.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/a317940-initial-values.yml b/.github/workflows/a317940-initial-values.yml index 2f035ddb..76dd4641 100644 --- a/.github/workflows/a317940-initial-values.yml +++ b/.github/workflows/a317940-initial-values.yml @@ -19,7 +19,7 @@ jobs: - uses: actions/checkout@v6 with: repository: DomTheDeveloper/formal-conjectures - ref: 5bde58f419e0b4022e515a3daf10304125ab138f + ref: 67e15bc35a4815fc5bff3a314db6d9b4e0ed8e4d fetch-depth: 1 - name: Install Lean run: | @@ -30,7 +30,7 @@ jobs: path: | .lake/packages .lake/build - key: a317940-initial-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }} + key: a317940-initial-v2-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }} restore-keys: a317940-initial-${{ runner.os }}- - name: Get Mathlib cache run: lake exe cache get From 622872c54306503fcc2a542ffc2bf7dee6020694 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 11:15:33 -0700 Subject: [PATCH 7/7] Audit final squashed A317940 commit --- .github/workflows/a317940-initial-values.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/a317940-initial-values.yml b/.github/workflows/a317940-initial-values.yml index 76dd4641..48abc7c7 100644 --- a/.github/workflows/a317940-initial-values.yml +++ b/.github/workflows/a317940-initial-values.yml @@ -19,7 +19,7 @@ jobs: - uses: actions/checkout@v6 with: repository: DomTheDeveloper/formal-conjectures - ref: 67e15bc35a4815fc5bff3a314db6d9b4e0ed8e4d + ref: 7f19c892cc0e328736c106d270444e4bfb0e1191 fetch-depth: 1 - name: Install Lean run: |