From 783a8e970681db54a179053aa1afc41b91dc5d76 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 12:57:07 -0700 Subject: [PATCH 1/9] 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 2/9] 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 3/9] 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 4/9] 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 5/9] 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 6/9] 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 7/9] 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 cc5cd6dac135e605e012ba817413ace9dd531a89 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 16:01:43 -0700 Subject: [PATCH 8/9] audit: pin A261865 checker to current repaired head --- .github/workflows/a261865-proof-audit.yml | 24 ++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/.github/workflows/a261865-proof-audit.yml b/.github/workflows/a261865-proof-audit.yml index aadccfc8..e746f184 100644 --- a/.github/workflows/a261865-proof-audit.yml +++ b/.github/workflows/a261865-proof-audit.yml @@ -21,17 +21,17 @@ jobs: axle-foundations: name: AXLE foundation audit runs-on: ubuntu-slim - timeout-minutes: 20 + timeout-minutes: 30 steps: - name: Checkout repaired A261865 proof commit uses: actions/checkout@v4 with: repository: DomTheDeveloper/formal-conjectures - ref: 46ea24719cc7b65389fe432a7af484d63cfa541f + ref: f5d289e074dc692ab75eb6050128339ef95861c2 - name: Confirm immutable proof source shell: bash - run: test "$(git rev-parse HEAD)" = "46ea24719cc7b65389fe432a7af484d63cfa541f" + run: test "$(git rev-parse HEAD)" = "f5d289e074dc692ab75eb6050128339ef95861c2" - name: Check foundational Lean files with AXLE shell: bash @@ -45,6 +45,10 @@ jobs: files = [ 'FormalConjecturesForMathlib/Analysis/Equidistribution/UnitAddTorus.lean', 'FormalConjecturesForMathlib/NumberTheory/SquarefreeRadical.lean', + 'FormalConjecturesForMathlib/MeasureTheory/Group/UnitAddCircleArc.lean', + 'FormalConjecturesForMathlib/MeasureTheory/Probability/PiContinuitySet.lean', + 'FormalConjecturesForMathlib/MeasureTheory/Probability/Empirical.lean', + 'FormalConjecturesForMathlib/NumberTheory/SquarefreeRadicals.lean', ] failed = False for filename in files: @@ -65,30 +69,32 @@ jobs: result = json.load(response) errors = result.get('lean_messages', {}).get('errors', []) tool_errors = result.get('tool_messages', {}).get('errors', []) + declarations = result.get('failed_declarations', []) 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) + print('failed_declarations=' + json.dumps(declarations, ensure_ascii=False)) + failed |= bool(errors or tool_errors or declarations or not okay) if failed: sys.exit(1) PY exact-kernel-audit: name: Lean 4.27 exact theorem and axiom audit - runs-on: ubuntu-latest - timeout-minutes: 90 + runs-on: macos-15 + timeout-minutes: 120 steps: - name: Checkout repaired A261865 proof commit uses: actions/checkout@v4 with: repository: DomTheDeveloper/formal-conjectures - ref: 46ea24719cc7b65389fe432a7af484d63cfa541f + ref: f5d289e074dc692ab75eb6050128339ef95861c2 - name: Confirm immutable proof source shell: bash - run: test "$(git rev-parse HEAD)" = "46ea24719cc7b65389fe432a7af484d63cfa541f" + run: test "$(git rev-parse HEAD)" = "f5d289e074dc692ab75eb6050128339ef95861c2" - name: Install pinned Lean toolchain shell: bash @@ -143,6 +149,6 @@ jobs: if: always() uses: actions/upload-artifact@v4 with: - name: a261865-46ea2471-kernel-transcript + name: a261865-f5d289e-kernel-transcript path: a261865-kernel-audit.log if-no-files-found: warn From 953ec2e1a3310d6c4236bb99f80367ee38f37d8e Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Wed, 22 Jul 2026 16:02:36 -0700 Subject: [PATCH 9/9] audit: trigger repaired A261865 verification --- 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..aa8f8665 --- /dev/null +++ b/audits/a261865-final.trigger @@ -0,0 +1 @@ +f5d289e074dc692ab75eb6050128339ef95861c2