From 26d68024ed82202cc0ef7eccc8371135326d5420 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 09:03:07 -0700 Subject: [PATCH 1/3] Add literal Lander-Parkin-Selfridge counterexample --- ...rParkinSelfridgeLiteralCounterexample.lean | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 FormalConjectures/Wikipedia/LanderParkinSelfridgeLiteralCounterexample.lean diff --git a/FormalConjectures/Wikipedia/LanderParkinSelfridgeLiteralCounterexample.lean b/FormalConjectures/Wikipedia/LanderParkinSelfridgeLiteralCounterexample.lean new file mode 100644 index 0000000000..3792d76824 --- /dev/null +++ b/FormalConjectures/Wikipedia/LanderParkinSelfridgeLiteralCounterexample.lean @@ -0,0 +1,34 @@ +import FormalConjectures.Wikipedia.LanderParkinAndSelfridgeConjecture + +/-! +# Counterexample to the literal Lander–Parkin–Selfridge declaration + +The catalog theorem quantifies over all natural numbers `n` and `m`, although its +prose requires positive numbers of summands. Taking both index types to be empty +makes the two power sums equal, while `k = 1` makes the claimed bound false. +-/ + +namespace LanderParkinSelfridge + +/-- The catalog declaration is false because it permits two empty sums. -/ +@[category research solved, AMS 11] +theorem lander_parkin_selfridge_false : + ¬ (∀ (k n m : ℕ) (x : Fin n → ℕ) (y : Fin m → ℕ), + (∀ i, 0 < x i) → (∀ j, 0 < y j) → + (∀ i j, x i ≠ y j) → + ∑ i, x i ^ k = ∑ j, y j ^ k → + k ≤ n + m) := by + intro h + have hbad : (1 : ℕ) ≤ 0 + 0 := + h 1 0 0 + (fun i => Fin.elim0 i) + (fun j => Fin.elim0 j) + (by intro i; exact Fin.elim0 i) + (by intro j; exact Fin.elim0 j) + (by intro i; exact Fin.elim0 i) + (by simp) + omega + +#print axioms lander_parkin_selfridge_false + +end LanderParkinSelfridge From 3f7a64688353707caac59e83a70751e96af16eaa Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 09:03:27 -0700 Subject: [PATCH 2/3] Add focused Lander-Parkin-Selfridge audit --- ...-lander-parkin-selfridge-literal-audit.yml | 54 +++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100644 .github/workflows/openai-lander-parkin-selfridge-literal-audit.yml diff --git a/.github/workflows/openai-lander-parkin-selfridge-literal-audit.yml b/.github/workflows/openai-lander-parkin-selfridge-literal-audit.yml new file mode 100644 index 0000000000..a1bfa20575 --- /dev/null +++ b/.github/workflows/openai-lander-parkin-selfridge-literal-audit.yml @@ -0,0 +1,54 @@ +name: OpenAI Lander-Parkin-Selfridge literal counterexample audit + +on: + push: + branches: + - openai/disprove-lander-parkin-selfridge-literal + paths: + - 'FormalConjectures/Wikipedia/LanderParkinSelfridgeLiteralCounterexample.lean' + - '.github/workflows/openai-lander-parkin-selfridge-literal-audit.yml' + pull_request: + paths: + - 'FormalConjectures/Wikipedia/LanderParkinSelfridgeLiteralCounterexample.lean' + - '.github/workflows/openai-lander-parkin-selfridge-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/LanderParkinSelfridgeLiteralCounterexample.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 counterexample module + run: lake build FormalConjectures.Wikipedia.LanderParkinSelfridgeLiteralCounterexample + - name: Audit theorem axioms + run: | + cat > /tmp/LanderLiteralAxioms.lean <<'EOF' + import FormalConjectures.Wikipedia.LanderParkinSelfridgeLiteralCounterexample + #print axioms LanderParkinSelfridge.lander_parkin_selfridge_false + EOF + lake env lean /tmp/LanderLiteralAxioms.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 From 2effc7170ff0bbf65af5cb01d6b7663532b3fff5 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 09:07:03 -0700 Subject: [PATCH 3/3] Add standard copyright header --- ...nderParkinSelfridgeLiteralCounterexample.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/FormalConjectures/Wikipedia/LanderParkinSelfridgeLiteralCounterexample.lean b/FormalConjectures/Wikipedia/LanderParkinSelfridgeLiteralCounterexample.lean index 3792d76824..a3addf489d 100644 --- a/FormalConjectures/Wikipedia/LanderParkinSelfridgeLiteralCounterexample.lean +++ b/FormalConjectures/Wikipedia/LanderParkinSelfridgeLiteralCounterexample.lean @@ -1,3 +1,19 @@ +/- +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.LanderParkinAndSelfridgeConjecture /-!