From 272177a0abb78f7789c23b7b7b1608a426e34a17 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sun, 26 Jul 2026 11:05:37 -0700
Subject: [PATCH 1/5] feat: prove the classical Euler brick witness

---
 .../Wikipedia/EulerBrickProof.lean            | 44 +++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 FormalConjectures/Wikipedia/EulerBrickProof.lean

diff --git a/FormalConjectures/Wikipedia/EulerBrickProof.lean b/FormalConjectures/Wikipedia/EulerBrickProof.lean
new file mode 100644
index 0000000000..e484bce82d
--- /dev/null
+++ b/FormalConjectures/Wikipedia/EulerBrickProof.lean
@@ -0,0 +1,44 @@
+/-
+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
+
+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, ?_⟩
+    norm_num [side44, side117]
+  · refine ⟨244, ?_⟩
+    norm_num [side44, side240]
+  · refine ⟨267, ?_⟩
+    norm_num [side117, side240]
+
+/-- 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

From 958251a39190911f26f0517cb95a04d615b2a83c Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sun, 26 Jul 2026 11:05:54 -0700
Subject: [PATCH 2/5] ci: audit the classical Euler brick witness

---
 .../openai-euler-brick-witness-audit.yml      | 57 +++++++++++++++++++
 1 file changed, 57 insertions(+)
 create mode 100644 .github/workflows/openai-euler-brick-witness-audit.yml

diff --git a/.github/workflows/openai-euler-brick-witness-audit.yml b/.github/workflows/openai-euler-brick-witness-audit.yml
new file mode 100644
index 0000000000..7d7b50d327
--- /dev/null
+++ b/.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

From fc02bf123dc36c49d913e01691fb300922bff499 Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sun, 26 Jul 2026 11:12:40 -0700
Subject: [PATCH 3/5] fix: normalize the Euler brick square identities

---
 FormalConjectures/Wikipedia/EulerBrickProof.lean | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/FormalConjectures/Wikipedia/EulerBrickProof.lean b/FormalConjectures/Wikipedia/EulerBrickProof.lean
index e484bce82d..41431d0654 100644
--- a/FormalConjectures/Wikipedia/EulerBrickProof.lean
+++ b/FormalConjectures/Wikipedia/EulerBrickProof.lean
@@ -16,6 +16,13 @@ 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⟩
@@ -27,11 +34,11 @@ private def side240 : ℕ+ := ⟨240, by norm_num⟩
 theorem isEulerBrick_44_117_240_kernel : IsEulerBrick side44 side117 side240 := by
   refine ⟨?_, ?_, ?_⟩
   · refine ⟨125, ?_⟩
-    norm_num [side44, side117]
+    norm_num [side44, side117, pow_two]
   · refine ⟨244, ?_⟩
-    norm_num [side44, side240]
+    norm_num [side44, side240, pow_two]
   · refine ⟨267, ?_⟩
-    norm_num [side117, side240]
+    norm_num [side117, side240, pow_two]
 
 /-- Euler bricks exist in three dimensions. -/
 @[category test, AMS 11]

From 9cdf7bb603e6cb60c036ea0353cf2ff4e81a741e Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sun, 26 Jul 2026 11:18:11 -0700
Subject: [PATCH 4/5] fix: kernel-decide the Euler brick arithmetic

---
 FormalConjectures/Wikipedia/EulerBrickProof.lean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/FormalConjectures/Wikipedia/EulerBrickProof.lean b/FormalConjectures/Wikipedia/EulerBrickProof.lean
index 41431d0654..1bd52f0c31 100644
--- a/FormalConjectures/Wikipedia/EulerBrickProof.lean
+++ b/FormalConjectures/Wikipedia/EulerBrickProof.lean
@@ -34,11 +34,14 @@ private def side240 : ℕ+ := ⟨240, by norm_num⟩
 theorem isEulerBrick_44_117_240_kernel : IsEulerBrick side44 side117 side240 := by
   refine ⟨?_, ?_, ?_⟩
   · refine ⟨125, ?_⟩
-    norm_num [side44, side117, pow_two]
+    change (44 : ℕ) * 44 + 117 * 117 = 125 * 125
+    decide
   · refine ⟨244, ?_⟩
-    norm_num [side44, side240, pow_two]
+    change (44 : ℕ) * 44 + 240 * 240 = 244 * 244
+    decide
   · refine ⟨267, ?_⟩
-    norm_num [side117, side240, pow_two]
+    change (117 : ℕ) * 117 + 240 * 240 = 267 * 267
+    decide
 
 /-- Euler bricks exist in three dimensions. -/
 @[category test, AMS 11]

From 2242a14d59b40ec335408e0ad4f0f9636553d83f Mon Sep 17 00:00:00 2001
From: DomTheDeveloper <DomTheDeveloper@users.noreply.github.com>
Date: Sun, 26 Jul 2026 11:23:50 -0700
Subject: [PATCH 5/5] fix: prove Euler brick equalities by positive-natural
 extensionality

---
 FormalConjectures/Wikipedia/EulerBrickProof.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/FormalConjectures/Wikipedia/EulerBrickProof.lean b/FormalConjectures/Wikipedia/EulerBrickProof.lean
index 1bd52f0c31..1b46f038f8 100644
--- a/FormalConjectures/Wikipedia/EulerBrickProof.lean
+++ b/FormalConjectures/Wikipedia/EulerBrickProof.lean
@@ -34,14 +34,14 @@ private def side240 : ℕ+ := ⟨240, by norm_num⟩
 theorem isEulerBrick_44_117_240_kernel : IsEulerBrick side44 side117 side240 := by
   refine ⟨?_, ?_, ?_⟩
   · refine ⟨125, ?_⟩
-    change (44 : ℕ) * 44 + 117 * 117 = 125 * 125
-    decide
+    apply Subtype.ext
+    norm_num [side44, side117, pow_two]
   · refine ⟨244, ?_⟩
-    change (44 : ℕ) * 44 + 240 * 240 = 244 * 244
-    decide
+    apply Subtype.ext
+    norm_num [side44, side240, pow_two]
   · refine ⟨267, ?_⟩
-    change (117 : ℕ) * 117 + 240 * 240 = 267 * 267
-    decide
+    apply Subtype.ext
+    norm_num [side117, side240, pow_two]
 
 /-- Euler bricks exist in three dimensions. -/
 @[category test, AMS 11]