Audit A261865 proof commit 02688846

.github/workflows/a261865-proof-audit.yml

@@ -21,13 +21,17 @@ jobs:
   axle-foundations:
     name: AXLE foundation audit
     runs-on: ubuntu-slim
-    timeout-minutes: 20
+    timeout-minutes: 30
     steps:
-      - name: Checkout A261865 proof commit
+      - name: Checkout repaired A261865 proof commit
         uses: actions/checkout@v4
         with:
           repository: DomTheDeveloper/formal-conjectures
-          ref: 02688846b7a0d44e208cef7581bbdbb3978813c6
+          ref: f5d289e074dc692ab75eb6050128339ef95861c2
+
+      - name: Confirm immutable proof source
+        shell: bash
+        run: test "$(git rev-parse HEAD)" = "f5d289e074dc692ab75eb6050128339ef95861c2"
 
       - name: Check foundational Lean files with AXLE
         shell: bash
@@ -41,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:
@@ -59,26 +67,34 @@ 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))
+              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: 60
+    runs-on: macos-15
+    timeout-minutes: 120
     steps:
-      - name: Checkout A261865 proof commit
+      - name: Checkout repaired A261865 proof commit
         uses: actions/checkout@v4
         with:
           repository: DomTheDeveloper/formal-conjectures
-          ref: 02688846b7a0d44e208cef7581bbdbb3978813c6
+          ref: f5d289e074dc692ab75eb6050128339ef95861c2
+
+      - name: Confirm immutable proof source
+        shell: bash
+        run: test "$(git rev-parse HEAD)" = "f5d289e074dc692ab75eb6050128339ef95861c2"
 
       - name: Install pinned Lean toolchain
         shell: bash
@@ -112,7 +128,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 +137,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-f5d289e-kernel-transcript
+          path: a261865-kernel-audit.log
+          if-no-files-found: warn

audits/A261865.md

@@ -0,0 +1,3 @@
+# A261865 audit
+
+Target commit: 02688846b7a0d44e208cef7581bbdbb3978813c6

audits/README.md

@@ -0,0 +1 @@
+A261865 independent proof verification.

audits/a261865-final.trigger

@@ -0,0 +1 @@
+f5d289e074dc692ab75eb6050128339ef95861c2

audits/target.txt

@@ -0,0 +1,2 @@
+46ea24719cc7b65389fe432a7af484d63cfa541f
+runner: ubuntu-latest + ubuntu-slim AXLE