Kernel-prove the classical Euler brick witness

.github/workflows/openai-euler-brick-witness-audit.yml

@@ -0,0 +1,57 @@
+name: OpenAI Euler brick witness audit
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - '.github/workflows/openai-euler-brick-witness-audit.yml'
+      - 'FormalConjectures/Wikipedia/EulerBrickProof.lean'
+
+permissions:
+  contents: read
+
+jobs:
+  audit:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@v6
+      - name: Install pinned 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: euler-brick-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}
+          restore-keys: euler-brick-${{ runner.os }}-${{ runner.arch }}-
+      - name: Fetch compiled dependencies
+        run: lake exe cache get
+      - name: Reject proof holes and trust escapes
+        run: |
+          set -euo pipefail
+          f=FormalConjectures/Wikipedia/EulerBrickProof.lean
+          ! grep -nE '\b(sorry|admit)\b|native_decide|decide \+native|unsafe|axiom |Lean\.ofReduce|Lean\.ofReduceBool|Lean\.trustCompiler' "$f"
+      - name: Compile exact registered proof module
+        run: |
+          set -o pipefail
+          lake build FormalConjectures.Wikipedia.EulerBrickProof 2>&1 | tee /tmp/euler-brick-build.log
+      - name: Audit exact theorem axioms
+        run: |
+          cat > /tmp/EulerBrickAxioms.lean <<'EOF'
+          import FormalConjectures.Wikipedia.EulerBrickProof
+          #print axioms EulerBrick.isEulerBrick_44_117_240_kernel
+          #print axioms EulerBrick.exists_euler_brick_kernel
+          EOF
+          lake env lean /tmp/EulerBrickAxioms.lean 2>&1 | tee /tmp/euler-brick-axioms.log
+          ! grep -E 'sorryAx|Lean\.ofReduce|Lean\.ofReduceBool|Lean\.trustCompiler' /tmp/euler-brick-axioms.log
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: euler-brick-${{ github.run_id }}
+          path: |
+            /tmp/euler-brick-build.log
+            /tmp/euler-brick-axioms.log
+          if-no-files-found: warn

FormalConjectures/Wikipedia/EulerBrickProof.lean

@@ -0,0 +1,54 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Wikipedia.EulerBrick
+
+/-!
+# Explicit Euler brick witness
+
+The classical cuboid with edges `44`, `117`, and `240` has integral face
+diagonals `125`, `244`, and `267`.
+-/
+
+namespace EulerBrick
+
+private def side44 : ℕ+ := ⟨44, by norm_num⟩
+private def side117 : ℕ+ := ⟨117, by norm_num⟩
+private def side240 : ℕ+ := ⟨240, by norm_num⟩
+
+/-- The classical integer cuboid `(44,117,240)` is an Euler brick. -/
+@[category test, AMS 11]
+theorem isEulerBrick_44_117_240_kernel : IsEulerBrick side44 side117 side240 := by
+  refine ⟨?_, ?_, ?_⟩
+  · refine ⟨125, ?_⟩
+    apply Subtype.ext
+    norm_num [side44, side117, pow_two]
+  · refine ⟨244, ?_⟩
+    apply Subtype.ext
+    norm_num [side44, side240, pow_two]
+  · refine ⟨267, ?_⟩
+    apply Subtype.ext
+    norm_num [side117, side240, pow_two]
+
+/-- Euler bricks exist in three dimensions. -/
+@[category test, AMS 11]
+theorem exists_euler_brick_kernel : ∃ a b c : ℕ+, IsEulerBrick a b c := by
+  exact ⟨side44, side117, side240, isEulerBrick_44_117_240_kernel⟩
+
+#print axioms isEulerBrick_44_117_240_kernel
+#print axioms exists_euler_brick_kernel
+
+end EulerBrick