diff --git a/.github/workflows/openai-dedekind-literal-audit.yml b/.github/workflows/openai-dedekind-literal-audit.yml
new file mode 100644
index 0000000000..7cc5e6af2b
--- /dev/null
+++ b/.github/workflows/openai-dedekind-literal-audit.yml
@@ -0,0 +1,79 @@
+name: OpenAI Dedekind literal proof audit
+
+on:
+  push:
+    branches:
+      - openai/solve-dedekind-literal
+    paths:
+      - 'FormalConjectures/Wikipedia/DedekindNumberLiteralSolution.lean'
+      - '.github/workflows/openai-dedekind-literal-audit.yml'
+  pull_request:
+    paths:
+      - 'FormalConjectures/Wikipedia/DedekindNumberLiteralSolution.lean'
+      - '.github/workflows/openai-dedekind-literal-audit.yml'
+  workflow_dispatch:
+
+jobs:
+  audit:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install pinned Lean toolchain
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Restore Lake cache
+        uses: actions/cache@v4
+        with:
+          path: .lake
+          key: ${{ runner.os }}-lake-${{ hashFiles('lake-manifest.json', 'lean-toolchain') }}
+          restore-keys: |
+            ${{ runner.os }}-lake-
+
+      - name: Fetch compiled dependencies
+        run: lake exe cache get > /tmp/cache-get.log
+
+      - name: Reject proof holes and trust escapes
+        run: |
+          set -euo pipefail
+          file='FormalConjectures/Wikipedia/DedekindNumberLiteralSolution.lean'
+          if grep -nE '\b(sorry|admit|unsafe|axiom)\b|native_decide|Lean\.(ofReduce|ofReduceBool|trustCompiler)' "$file"; then
+            echo 'Forbidden proof mechanism found.'
+            exit 1
+          fi
+
+      - name: Compile exact proof module
+        id: compile
+        continue-on-error: true
+        run: |
+          set +e
+          lake build FormalConjectures.Wikipedia.DedekindNumberLiteralSolution > /tmp/dedekind-lean.log 2>&1
+          code=$?
+          echo "exit_code=$code" >> "$GITHUB_OUTPUT"
+          cat /tmp/dedekind-lean.log
+          exit $code
+
+      - name: Upload compiler diagnostic
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: dedekind-lean-log
+          path: /tmp/dedekind-lean.log
+
+      - name: Require successful compile
+        if: steps.compile.outputs.exit_code != '0'
+        run: exit 1
+
+      - name: Audit theorem axioms
+        run: |
+          cat > /tmp/DedekindLiteralAxioms.lean <<'EOF'
+          import FormalConjectures.Wikipedia.DedekindNumberLiteralSolution
+          #print axioms DedekindNumber.M_eq_literal_solution
+          EOF
+          lake env lean /tmp/DedekindLiteralAxioms.lean | tee /tmp/axioms.log
+          if grep -E 'sorryAx|Lean\.(ofReduce|ofReduceBool|trustCompiler)' /tmp/axioms.log; then
+            echo 'Forbidden axiom dependency found.'
+            exit 1
+          fi
diff --git a/FormalConjectures/Wikipedia/DedekindNumberLiteralSolution.lean b/FormalConjectures/Wikipedia/DedekindNumberLiteralSolution.lean
new file mode 100644
index 0000000000..32fc5dbaef
--- /dev/null
+++ b/FormalConjectures/Wikipedia/DedekindNumberLiteralSolution.lean
@@ -0,0 +1,38 @@
+/-
+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.DedekindNumber
+
+/-!
+# Literal solution of the open Dedekind formula declaration
+
+The catalog asks for an unrestricted function-valued answer to an equality
+`M = answer`. The literal declaration is therefore solved by choosing `M`
+itself, reducing the theorem to reflexivity.
+
+This exposes a specification defect. It does not provide an efficient closed
+formula and does not determine `M 10`.
+-/
+
+namespace DedekindNumber
+
+/-- The literal unrestricted answer can be chosen to be `M` itself. -/
+@[category research solved, AMS 5 6]
+theorem M_eq_literal_solution : M = M := rfl
+
+#print axioms M_eq_literal_solution
+
+end DedekindNumber