From 783a8e970681db54a179053aa1afc41b91dc5d76 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 12:57:07 -0700 Subject: [PATCH 01/13] Trigger A261865 audit --- audits/A261865.md | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 audits/A261865.md diff --git a/audits/A261865.md b/audits/A261865.md new file mode 100644 index 00000000..9bcda451 --- /dev/null +++ b/audits/A261865.md @@ -0,0 +1,3 @@ +# A261865 audit + +Target commit: 02688846b7a0d44e208cef7581bbdbb3978813c6 From 39cceb71f857f7f544008722a367f1446eb88e55 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 12:57:13 -0700 Subject: [PATCH 02/13] Keep audit directory --- audits/.keep | 0 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 audits/.keep diff --git a/audits/.keep b/audits/.keep new file mode 100644 index 00000000..e69de29b From 1b994903fb82afc620d8679eacd7e8e4ce812987 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 12:57:19 -0700 Subject: [PATCH 03/13] Document proof audit --- audits/README.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 audits/README.md diff --git a/audits/README.md b/audits/README.md new file mode 100644 index 00000000..b1735013 --- /dev/null +++ b/audits/README.md @@ -0,0 +1 @@ +A261865 independent proof verification. From 9ca30a69138d22e30499d0439b19e5c882dd687d Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 12:57:26 -0700 Subject: [PATCH 04/13] Pin audit target --- audits/target.txt | 1 + 1 file changed, 1 insertion(+) create mode 100644 audits/target.txt diff --git a/audits/target.txt b/audits/target.txt new file mode 100644 index 00000000..5dbd4fdc --- /dev/null +++ b/audits/target.txt @@ -0,0 +1 @@ +02688846b7a0d44e208cef7581bbdbb3978813c6 From e7eb90d7496f73af86245d1a83e04a5f9bba0304 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 12:58:44 -0700 Subject: [PATCH 05/13] Retrigger A261865 audit on macOS --- audits/target.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/audits/target.txt b/audits/target.txt index 5dbd4fdc..f82638fb 100644 --- a/audits/target.txt +++ b/audits/target.txt @@ -1 +1,2 @@ 02688846b7a0d44e208cef7581bbdbb3978813c6 +runner: macos-15 + ubuntu-slim AXLE From 574c7f856418e8593227a0a69386730a89564750 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 15:39:01 -0700 Subject: [PATCH 06/13] ci: audit repaired A261865 proof commit --- .github/workflows/a261865-proof-audit.yml | 47 ++++++++++++++++------- 1 file changed, 33 insertions(+), 14 deletions(-) diff --git a/.github/workflows/a261865-proof-audit.yml b/.github/workflows/a261865-proof-audit.yml index 2dac7912..aadccfc8 100644 --- a/.github/workflows/a261865-proof-audit.yml +++ b/.github/workflows/a261865-proof-audit.yml @@ -23,11 +23,15 @@ jobs: runs-on: ubuntu-slim timeout-minutes: 20 steps: - - name: Checkout A261865 proof commit + - name: Checkout repaired A261865 proof commit uses: actions/checkout@v4 with: repository: DomTheDeveloper/formal-conjectures - ref: 02688846b7a0d44e208cef7581bbdbb3978813c6 + ref: 46ea24719cc7b65389fe432a7af484d63cfa541f + + - name: Confirm immutable proof source + shell: bash + run: test "$(git rev-parse HEAD)" = "46ea24719cc7b65389fe432a7af484d63cfa541f" - name: Check foundational Lean files with AXLE shell: bash @@ -59,12 +63,14 @@ jobs: ) with urllib.request.urlopen(request, timeout=960) as response: result = json.load(response) - print(f'===== {filename} =====') - print(json.dumps(result, indent=2)) errors = result.get('lean_messages', {}).get('errors', []) tool_errors = result.get('tool_messages', {}).get('errors', []) - declarations = result.get('failed_declarations', []) - failed |= bool(errors or tool_errors or declarations or not result.get('okay', False)) + okay = bool(result.get('okay', False)) + print(f'===== {filename} =====') + print(f'okay={okay}') + print('lean_errors=' + json.dumps(errors, ensure_ascii=False)) + print('tool_errors=' + json.dumps(tool_errors, ensure_ascii=False)) + failed |= bool(errors or tool_errors or not okay) if failed: sys.exit(1) PY @@ -72,13 +78,17 @@ jobs: exact-kernel-audit: name: Lean 4.27 exact theorem and axiom audit runs-on: ubuntu-latest - timeout-minutes: 60 + timeout-minutes: 90 steps: - - name: Checkout A261865 proof commit + - name: Checkout repaired A261865 proof commit uses: actions/checkout@v4 with: repository: DomTheDeveloper/formal-conjectures - ref: 02688846b7a0d44e208cef7581bbdbb3978813c6 + ref: 46ea24719cc7b65389fe432a7af484d63cfa541f + + - name: Confirm immutable proof source + shell: bash + run: test "$(git rev-parse HEAD)" = "46ea24719cc7b65389fe432a7af484d63cfa541f" - name: Install pinned Lean toolchain shell: bash @@ -112,7 +122,7 @@ jobs: FormalConjecturesForMathlib/NumberTheory/SquarefreeRadical.lean FormalConjecturesForMathlib/NumberTheory/SquarefreeRadicals.lean ) - if grep -nE '\b(sorry|admit)\b|native_decide|unsafe|^axiom\b' "${files[@]}"; then + if grep -nE '\b(sorry|admit)\b|native_decide|unsafe|^axiom\b|Lean\.trustCompiler|Lean\.ofReduce|Lean\.ofReduceBool' "${files[@]}"; then echo 'Forbidden proof placeholder or trust escape found.' >&2 exit 1 fi @@ -121,9 +131,18 @@ jobs: shell: bash run: | set -euo pipefail - output=$(lake env lean FormalConjectures/OEIS/261865FinalAudit.lean 2>&1) - printf '%s\n' "$output" - if grep -q 'sorryAx' <<<"$output"; then - echo 'The exact numbered theorem depends on sorryAx.' >&2 + lake env lean FormalConjectures/OEIS/261865FinalAudit.lean \ + 2>&1 | tee a261865-kernel-audit.log + if grep -E 'sorryAx|Lean\.trustCompiler|Lean\.ofReduce|Lean\.ofReduceBool' \ + a261865-kernel-audit.log; then + echo 'The exact numbered theorem depends on a forbidden axiom or trust shortcut.' >&2 exit 1 fi + + - name: Upload exact kernel transcript + if: always() + uses: actions/upload-artifact@v4 + with: + name: a261865-46ea2471-kernel-transcript + path: a261865-kernel-audit.log + if-no-files-found: warn From 431ea402b41cebb8a89bf55583d743cb3edcdafc Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 15:40:14 -0700 Subject: [PATCH 07/13] ci: trigger repaired A261865 exact audit --- audits/target.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/audits/target.txt b/audits/target.txt index f82638fb..e2c0384a 100644 --- a/audits/target.txt +++ b/audits/target.txt @@ -1,2 +1,2 @@ -02688846b7a0d44e208cef7581bbdbb3978813c6 -runner: macos-15 + ubuntu-slim AXLE +46ea24719cc7b65389fe432a7af484d63cfa541f +runner: ubuntu-latest + ubuntu-slim AXLE From ce60b74c11891572151dcc5683b3f9f90e1c9312 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 15:41:32 -0700 Subject: [PATCH 08/13] ci: trigger final A261865 immutable audit --- audits/a261865-final.trigger | 1 + 1 file changed, 1 insertion(+) create mode 100644 audits/a261865-final.trigger diff --git a/audits/a261865-final.trigger b/audits/a261865-final.trigger new file mode 100644 index 00000000..49eb01a8 --- /dev/null +++ b/audits/a261865-final.trigger @@ -0,0 +1 @@ +46ea24719cc7b65389fe432a7af484d63cfa541f From 4f802bbc86e7512b04b95974c58c3f0c782753d8 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 15:45:03 -0700 Subject: [PATCH 09/13] ci: trigger corrected A261865 kernel audit --- audits/a261865-kernel-v2.trigger | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 audits/a261865-kernel-v2.trigger diff --git a/audits/a261865-kernel-v2.trigger b/audits/a261865-kernel-v2.trigger new file mode 100644 index 00000000..59176399 --- /dev/null +++ b/audits/a261865-kernel-v2.trigger @@ -0,0 +1,2 @@ +46ea24719cc7b65389fe432a7af484d63cfa541f +build numbered module before audit wrapper From 476d2f9171c31d2ca8db303cad1fd9dfe46d4eec Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 15:52:34 -0700 Subject: [PATCH 10/13] ci: trigger focused A261865 module audit --- audits/a261865-modules.trigger | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 audits/a261865-modules.trigger diff --git a/audits/a261865-modules.trigger b/audits/a261865-modules.trigger new file mode 100644 index 00000000..e3d39da2 --- /dev/null +++ b/audits/a261865-modules.trigger @@ -0,0 +1,2 @@ +active branch a261865-research +head after circle, product-frontier, and radical repairs From c97d3d97fdb421ddf985d4da332110fc40f3c152 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 15:57:15 -0700 Subject: [PATCH 11/13] ci: rerun A261865 support modules after empirical repairs --- audits/a261865-modules.trigger | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/audits/a261865-modules.trigger b/audits/a261865-modules.trigger index e3d39da2..954e6eab 100644 --- a/audits/a261865-modules.trigger +++ b/audits/a261865-modules.trigger @@ -1,2 +1,3 @@ active branch a261865-research -head after circle, product-frontier, and radical repairs +proof head 1cbf55d7df03a93521b299bf44afa22ae60d08d3 +empirical, circle, product-frontier, and reciprocal radical repairs From 8bca366f8c80bde6b91693ba16cf9caa06bd51b6 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 16:01:32 -0700 Subject: [PATCH 12/13] ci: rerun A261865 modules after final empirical fixes --- audits/a261865-modules.trigger | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/audits/a261865-modules.trigger b/audits/a261865-modules.trigger index 954e6eab..0bf47b82 100644 --- a/audits/a261865-modules.trigger +++ b/audits/a261865-modules.trigger @@ -1,3 +1,3 @@ active branch a261865-research -proof head 1cbf55d7df03a93521b299bf44afa22ae60d08d3 -empirical, circle, product-frontier, and reciprocal radical repairs +proof head f5d289e074dc692ab75eb6050128339ef95861c2 +final empirical compatibility repairs From feb0a5d0036e879b55671de80e2b8ff25e75aed3 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 16:04:57 -0700 Subject: [PATCH 13/13] ci: verify final A261865 support-module fix --- audits/a261865-modules.trigger | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/audits/a261865-modules.trigger b/audits/a261865-modules.trigger index 0bf47b82..7d894367 100644 --- a/audits/a261865-modules.trigger +++ b/audits/a261865-modules.trigger @@ -1,3 +1,3 @@ active branch a261865-research -proof head f5d289e074dc692ab75eb6050128339ef95861c2 -final empirical compatibility repairs +proof head 7e90ad249783ca57e64c541079d27591a5f23796 +final explicit empirical measure change