From 5e3e3cefa5abf2f2727bd12454617e03d3a5a14a Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 00:25:45 -0700 Subject: [PATCH 1/3] Formalize Chomp three-opening reduction --- .../Paper/ChompThreeOpenings.lean | 106 ++++++++++++++++++ 1 file changed, 106 insertions(+) create mode 100644 FormalConjectures/Paper/ChompThreeOpenings.lean diff --git a/FormalConjectures/Paper/ChompThreeOpenings.lean b/FormalConjectures/Paper/ChompThreeOpenings.lean new file mode 100644 index 0000000000..b2a8a64396 --- /dev/null +++ b/FormalConjectures/Paper/ChompThreeOpenings.lean @@ -0,0 +1,106 @@ +/- +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 FormalConjecturesUtil + +/-! +# Three winning opening moves in Chomp + +This file gives an exact finite-game specification of rectangular Chomp and isolates the +three concrete losing-position obligations for the proposed `10 × 42` witness. + +*Reference:* +- [All the Winning Bites for a by b Chomp for a and b up to 14 and Two Computational + Challenges](https://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/chompc.html) + by S. B. Ekhad and D. Zeilberger. +-/ + +namespace ChompThreeOpenings + +/-- A Ferrers Chomp position, represented by row lengths from top to bottom. -/ +abbrev Position := List ℕ + +/-- Bite in `row`, leaving `keep` squares in that row and truncating every lower row. -/ +def bite (p : Position) (row keep : ℕ) : Position := + p.take row ++ (p.drop row).map (fun width => min width keep) + +/-- All legal Chomp options. The poisoned top-left square is never offered as a move. -/ +def options (p : Position) : List Position := + (List.range p.length).flatMap fun row => + match p.get? row with + | none => [] + | some width => + (List.range width).filterMap fun keep => + if row = 0 ∧ keep = 0 then none else some (bite p row keep) + +/-- Bounded normal-play outcome recursion. `true` means the player to move can force a win. -/ +def winningWithin : ℕ → Position → Bool + | 0, _ => false + | fuel + 1, p => (options p).any fun q => !(winningWithin fuel q) + +/-- Chomp outcome, using the number of remaining squares as a valid turn bound. -/ +def winning (p : Position) : Bool := + winningWithin p.sum p + +/-- A previous-player win (losing position for the player to move). -/ +def PPosition (p : Position) : Prop := + winning p = false + +/-- A winning opening is a legal move to a P-position. -/ +def WinningOpening (p q : Position) : Prop := + q ∈ options p ∧ PPosition q + +/-- The position is a rectangle with the specified number of rows and columns. -/ +def rectangle (rows columns : ℕ) : Position := + List.replicate rows columns + +/-- A position has at least three pairwise-distinct winning openings. -/ +def HasThreeWinningOpenings (p : Position) : Prop := + ∃ q₁ q₂ q₃, + q₁ ≠ q₂ ∧ q₁ ≠ q₃ ∧ q₂ ≠ q₃ ∧ + WinningOpening p q₁ ∧ WinningOpening p q₂ ∧ WinningOpening p q₃ + +/-- Residual position after biting row 5, column 36 (one-based coordinates). -/ +def root₁ : Position := [42, 42, 42, 42, 35, 35, 35, 35, 35, 35] + +/-- Residual position after biting row 7, column 30 (one-based coordinates). -/ +def root₂ : Position := [42, 42, 42, 42, 42, 42, 29, 29, 29, 29] + +/-- Residual position after biting row 8, column 26 (one-based coordinates). -/ +def root₃ : Position := [42, 42, 42, 42, 42, 42, 42, 25, 25, 25] + +/-- The three explicit bites are distinct legal options of the `10 × 42` rectangle. -/ +@[category test, AMS 5 91] +theorem roots_are_distinct_legal_options : + root₁ ∈ options (rectangle 10 42) ∧ + root₂ ∈ options (rectangle 10 42) ∧ + root₃ ∈ options (rectangle 10 42) ∧ + root₁ ≠ root₂ ∧ root₁ ≠ root₃ ∧ root₂ ≠ root₃ := by + decide + +/-- +The exact remaining proof boundary: once the three displayed residual positions are certified +as P-positions, the `10 × 42` rectangle has at least three winning first moves. +-/ +@[category API, AMS 5 91] +theorem hasThreeWinningOpenings_of_roots + (h₁ : PPosition root₁) (h₂ : PPosition root₂) (h₃ : PPosition root₃) : + HasThreeWinningOpenings (rectangle 10 42) := by + rcases roots_are_distinct_legal_options with ⟨hm₁, hm₂, hm₃, hne₁₂, hne₁₃, hne₂₃⟩ + exact ⟨root₁, root₂, root₃, hne₁₂, hne₁₃, hne₂₃, + ⟨hm₁, h₁⟩, ⟨hm₂, h₂⟩, ⟨hm₃, h₃⟩⟩ + +end ChompThreeOpenings From 4850d9d919c5ea66a6258049e59e0e319d9c6230 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 00:39:22 -0700 Subject: [PATCH 2/3] Use Formal Conjectures theorem naming conventions --- FormalConjectures/Paper/ChompThreeOpenings.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/Paper/ChompThreeOpenings.lean b/FormalConjectures/Paper/ChompThreeOpenings.lean index b2a8a64396..f025676d35 100644 --- a/FormalConjectures/Paper/ChompThreeOpenings.lean +++ b/FormalConjectures/Paper/ChompThreeOpenings.lean @@ -96,7 +96,7 @@ The exact remaining proof boundary: once the three displayed residual positions as P-positions, the `10 × 42` rectangle has at least three winning first moves. -/ @[category API, AMS 5 91] -theorem hasThreeWinningOpenings_of_roots +theorem has_three_winning_openings_of_roots (h₁ : PPosition root₁) (h₂ : PPosition root₂) (h₃ : PPosition root₃) : HasThreeWinningOpenings (rectangle 10 42) := by rcases roots_are_distinct_legal_options with ⟨hm₁, hm₂, hm₃, hne₁₂, hne₁₃, hne₂₃⟩ From 87170f5bc6ce3e2247a3940fc7ab837129ce6c5c Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Thu, 23 Jul 2026 00:46:07 -0700 Subject: [PATCH 3/3] Add OEIS reference for Chomp challenge --- FormalConjectures/Paper/ChompThreeOpenings.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/FormalConjectures/Paper/ChompThreeOpenings.lean b/FormalConjectures/Paper/ChompThreeOpenings.lean index f025676d35..d6eecff18e 100644 --- a/FormalConjectures/Paper/ChompThreeOpenings.lean +++ b/FormalConjectures/Paper/ChompThreeOpenings.lean @@ -22,10 +22,11 @@ import FormalConjecturesUtil This file gives an exact finite-game specification of rectangular Chomp and isolates the three concrete losing-position obligations for the proposed `10 × 42` witness. -*Reference:* +*References:* - [All the Winning Bites for a by b Chomp for a and b up to 14 and Two Computational Challenges](https://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/chompc.html) by S. B. Ekhad and D. Zeilberger. +- [OEIS A147983](https://oeis.org/A147983) -/ namespace ChompThreeOpenings