From fbdf85f02cc205cd9dd31c8109beabf7815b414e Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:17:16 -0700 Subject: [PATCH 01/10] Audit low-hanging Dedekind and moving-sofa targets --- FormalConjecturesTest/LowHangingFruit.lean | 62 ++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 FormalConjecturesTest/LowHangingFruit.lean diff --git a/FormalConjecturesTest/LowHangingFruit.lean b/FormalConjecturesTest/LowHangingFruit.lean new file mode 100644 index 0000000000..920c866667 --- /dev/null +++ b/FormalConjecturesTest/LowHangingFruit.lean @@ -0,0 +1,62 @@ +/- +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 +import FormalConjectures.Wikipedia.MovingSofa + +namespace DedekindNumber + +@[category test, AMS 5 6] +theorem M_eq_low_hanging : M = answer(sorry) := by + exact M_eq_kisielewiczFormula + +#print axioms M_eq_low_hanging + +end DedekindNumber + +namespace MovingSofa + +open MeasureTheory +open scoped ENNReal EuclideanGeometry + +@[category test, AMS 49] +theorem not_literal_uniqueness : + ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa) := by + intro h + have hvol : sofaConstant = volume gerversSofa := (h gerversSofa).2 rfl + have hpos : 0 < volume gerversSofa := by + rw [← hvol] + exact lt_of_lt_of_le (by norm_num) one_le_sofaConstant + have hne : gerversSofa.Nonempty := by + by_contra hne + have hempty : gerversSofa = ∅ := Set.not_nonempty_iff_eq_empty.mp hne + simp [hempty] at hpos + obtain ⟨p, hp⟩ := hne + have hmeasure : + volume (gerversSofa \ ({p} : Set ℝ²)) = volume gerversSofa := by + exact measure_sdiff_null (by simp) + have hsvol : sofaConstant = volume (gerversSofa \ ({p} : Set ℝ²)) := + hvol.trans hmeasure.symm + have hset : gerversSofa \ ({p} : Set ℝ²) = gerversSofa := + (h (gerversSofa \ ({p} : Set ℝ²))).1 hsvol + have hp' : p ∈ gerversSofa \ ({p} : Set ℝ²) := by + rw [hset] + exact hp + exact hp'.2 (by simp) + +#print axioms not_literal_uniqueness + +end MovingSofa From e3f3b942be639c262adb8d68cafcff45fcfc1280 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:20:00 -0700 Subject: [PATCH 02/10] Build low-hanging fruit audit in main Lean library --- .../Other/LowHangingFruitAudit.lean | 69 +++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 FormalConjectures/Other/LowHangingFruitAudit.lean diff --git a/FormalConjectures/Other/LowHangingFruitAudit.lean b/FormalConjectures/Other/LowHangingFruitAudit.lean new file mode 100644 index 0000000000..0651611154 --- /dev/null +++ b/FormalConjectures/Other/LowHangingFruitAudit.lean @@ -0,0 +1,69 @@ +/- +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 +import FormalConjectures.Wikipedia.MovingSofa + +/-! +# Low-hanging fruit audit + +This temporary module checks two candidate formal-conjectures targets before editing their +source declarations. +-/ + +namespace DedekindNumber + +@[category test, AMS 5 6] +theorem M_eq_low_hanging : M = answer(sorry) := by + exact M_eq_kisielewiczFormula + +#print axioms M_eq_low_hanging + +end DedekindNumber + +namespace MovingSofa + +open MeasureTheory +open scoped ENNReal EuclideanGeometry + +@[category test, AMS 49] +theorem not_literal_uniqueness : + ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa) := by + intro h + have hvol : sofaConstant = volume gerversSofa := (h gerversSofa).2 rfl + have hpos : 0 < volume gerversSofa := by + rw [← hvol] + exact lt_of_lt_of_le (by norm_num) one_le_sofaConstant + have hne : gerversSofa.Nonempty := by + by_contra hne + have hempty : gerversSofa = ∅ := Set.not_nonempty_iff_eq_empty.mp hne + simp [hempty] at hpos + obtain ⟨p, hp⟩ := hne + have hmeasure : + volume (gerversSofa \ ({p} : Set ℝ²)) = volume gerversSofa := by + exact measure_sdiff_null (by simp) + have hsvol : sofaConstant = volume (gerversSofa \ ({p} : Set ℝ²)) := + hvol.trans hmeasure.symm + have hset : gerversSofa \ ({p} : Set ℝ²) = gerversSofa := + (h (gerversSofa \ ({p} : Set ℝ²))).1 hsvol + have hp' : p ∈ gerversSofa \ ({p} : Set ℝ²) := by + rw [hset] + exact hp + exact hp'.2 (by simp) + +#print axioms not_literal_uniqueness + +end MovingSofa From 1964225c848850a0252573b647007c5fff4a25a1 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:22:04 -0700 Subject: [PATCH 03/10] Separate clean Dedekind answer from admitted formula --- FormalConjectures/Other/LowHangingFruitAudit.lean | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/FormalConjectures/Other/LowHangingFruitAudit.lean b/FormalConjectures/Other/LowHangingFruitAudit.lean index 0651611154..a4647c0ca4 100644 --- a/FormalConjectures/Other/LowHangingFruitAudit.lean +++ b/FormalConjectures/Other/LowHangingFruitAudit.lean @@ -26,11 +26,21 @@ source declarations. namespace DedekindNumber +/-- A clean formal answer to the underspecified `M_eq` declaration using the already-proved +antichain characterization. -/ @[category test, AMS 5 6] -theorem M_eq_low_hanging : M = answer(sorry) := by +theorem M_eq_via_antichains : M = answer(M') := by + exact M_eq_M' + +#print axioms M_eq_via_antichains + +/-- The mathematically intended Kisielewicz answer, audited separately because the source theorem +still contains `sorry`. -/ +@[category test, AMS 5 6] +theorem M_eq_via_kisielewicz : M = answer(kisielewiczFormula) := by exact M_eq_kisielewiczFormula -#print axioms M_eq_low_hanging +#print axioms M_eq_via_kisielewicz end DedekindNumber @@ -39,6 +49,7 @@ namespace MovingSofa open MeasureTheory open scoped ENNReal EuclideanGeometry +/-- Literal set equality cannot characterize area maximizers: deleting one point preserves volume. -/ @[category test, AMS 49] theorem not_literal_uniqueness : ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa) := by From 0f765b5cc98f5ec14c144bf4ee3519e62c9d8580 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:23:45 -0700 Subject: [PATCH 04/10] Add focused low-hanging fruit Lean audit --- .github/workflows/low-hanging-fruit-audit.yml | 68 +++++++++++++++++++ 1 file changed, 68 insertions(+) create mode 100644 .github/workflows/low-hanging-fruit-audit.yml diff --git a/.github/workflows/low-hanging-fruit-audit.yml b/.github/workflows/low-hanging-fruit-audit.yml new file mode 100644 index 0000000000..5caa5e1032 --- /dev/null +++ b/.github/workflows/low-hanging-fruit-audit.yml @@ -0,0 +1,68 @@ +name: Low-hanging fruit focused audit + +on: + pull_request: + branches: [main] + paths: + - '.github/workflows/low-hanging-fruit-audit.yml' + - 'FormalConjectures/Other/LowHangingFruitAudit.lean' + +concurrency: + group: low-hanging-fruit-focused-audit + cancel-in-progress: true + +permissions: + contents: read + +jobs: + verify: + runs-on: ubuntu-latest + timeout-minutes: 45 + steps: + - uses: actions/checkout@v6 + with: + repository: DomTheDeveloper/formal-conjectures + ref: agent/low-hanging-fruit-audit + fetch-depth: 1 + - name: Install Lean + 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: low-hanging-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }} + restore-keys: low-hanging-${{ runner.os }}-${{ runner.arch }}- + - name: Get Mathlib cache + run: | + set -euo pipefail + for attempt in 1 2 3; do + lake exe cache get && exit 0 + sleep 10 + done + exit 1 + - name: Compile audit module + run: | + set -o pipefail + lake env lean FormalConjectures/Other/LowHangingFruitAudit.lean 2>&1 | tee /tmp/low-hanging-compile.log + - name: Audit clean theorem axioms + if: success() + run: | + cat > /tmp/LowHangingAxioms.lean <<'EOF' + import FormalConjectures.Other.LowHangingFruitAudit + #print axioms DedekindNumber.M_eq_via_antichains + #print axioms MovingSofa.not_literal_uniqueness + EOF + lake env lean /tmp/LowHangingAxioms.lean 2>&1 | tee /tmp/low-hanging-axioms.log + ! grep -E 'sorryAx|Lean\.ofReduceBool|Lean\.trustCompiler' /tmp/low-hanging-axioms.log + - name: Upload diagnostics + if: always() + uses: actions/upload-artifact@v4 + with: + name: low-hanging-fruit-${{ github.run_id }} + path: | + /tmp/low-hanging-compile.log + /tmp/low-hanging-axioms.log + if-no-files-found: warn From 56af5b915b0a3232a25987326ee15c5de6db9087 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:28:42 -0700 Subject: [PATCH 05/10] Build exact audit module through Lake --- .github/workflows/low-hanging-fruit-audit.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/low-hanging-fruit-audit.yml b/.github/workflows/low-hanging-fruit-audit.yml index 5caa5e1032..826044406d 100644 --- a/.github/workflows/low-hanging-fruit-audit.yml +++ b/.github/workflows/low-hanging-fruit-audit.yml @@ -46,7 +46,7 @@ jobs: - name: Compile audit module run: | set -o pipefail - lake env lean FormalConjectures/Other/LowHangingFruitAudit.lean 2>&1 | tee /tmp/low-hanging-compile.log + lake build FormalConjectures.Other.LowHangingFruitAudit 2>&1 | tee /tmp/low-hanging-compile.log - name: Audit clean theorem axioms if: success() run: | From f348928d67599d81cad2efc3be1f1d4275398b7f Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:33:44 -0700 Subject: [PATCH 06/10] Use pinned Mathlib measure lemma --- FormalConjectures/Other/LowHangingFruitAudit.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/Other/LowHangingFruitAudit.lean b/FormalConjectures/Other/LowHangingFruitAudit.lean index a4647c0ca4..0e30ec97f6 100644 --- a/FormalConjectures/Other/LowHangingFruitAudit.lean +++ b/FormalConjectures/Other/LowHangingFruitAudit.lean @@ -65,7 +65,7 @@ theorem not_literal_uniqueness : obtain ⟨p, hp⟩ := hne have hmeasure : volume (gerversSofa \ ({p} : Set ℝ²)) = volume gerversSofa := by - exact measure_sdiff_null (by simp) + exact measure_diff_null (by simp) have hsvol : sofaConstant = volume (gerversSofa \ ({p} : Set ℝ²)) := hvol.trans hmeasure.symm have hset : gerversSofa \ ({p} : Set ℝ²) = gerversSofa := From 3a2772555a6abd220856bb934310afdda09ba70d Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:39:48 -0700 Subject: [PATCH 07/10] Generalize moving-sofa uniqueness refutation --- .../Other/LowHangingFruitAudit.lean | 37 +++++++++---------- 1 file changed, 18 insertions(+), 19 deletions(-) diff --git a/FormalConjectures/Other/LowHangingFruitAudit.lean b/FormalConjectures/Other/LowHangingFruitAudit.lean index 0e30ec97f6..89edbd8bc8 100644 --- a/FormalConjectures/Other/LowHangingFruitAudit.lean +++ b/FormalConjectures/Other/LowHangingFruitAudit.lean @@ -32,16 +32,12 @@ antichain characterization. -/ theorem M_eq_via_antichains : M = answer(M') := by exact M_eq_M' -#print axioms M_eq_via_antichains - /-- The mathematically intended Kisielewicz answer, audited separately because the source theorem still contains `sorry`. -/ @[category test, AMS 5 6] theorem M_eq_via_kisielewicz : M = answer(kisielewiczFormula) := by exact M_eq_kisielewiczFormula -#print axioms M_eq_via_kisielewicz - end DedekindNumber namespace MovingSofa @@ -49,32 +45,35 @@ namespace MovingSofa open MeasureTheory open scoped ENNReal EuclideanGeometry -/-- Literal set equality cannot characterize area maximizers: deleting one point preserves volume. -/ +/-- No set can be the literal unique set with maximal volume: deleting one point preserves volume. -/ @[category test, AMS 49] -theorem not_literal_uniqueness : - ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa) := by +theorem no_literal_volume_unique (g : Set ℝ²) : + ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = g) := by intro h - have hvol : sofaConstant = volume gerversSofa := (h gerversSofa).2 rfl - have hpos : 0 < volume gerversSofa := by + have hvol : sofaConstant = volume g := (h g).2 rfl + have hpos : 0 < volume g := by rw [← hvol] exact lt_of_lt_of_le (by norm_num) one_le_sofaConstant - have hne : gerversSofa.Nonempty := by + have hne : g.Nonempty := by by_contra hne - have hempty : gerversSofa = ∅ := Set.not_nonempty_iff_eq_empty.mp hne + have hempty : g = ∅ := Set.not_nonempty_iff_eq_empty.mp hne simp [hempty] at hpos obtain ⟨p, hp⟩ := hne - have hmeasure : - volume (gerversSofa \ ({p} : Set ℝ²)) = volume gerversSofa := by + have hmeasure : volume (g \ ({p} : Set ℝ²)) = volume g := by exact measure_diff_null (by simp) - have hsvol : sofaConstant = volume (gerversSofa \ ({p} : Set ℝ²)) := - hvol.trans hmeasure.symm - have hset : gerversSofa \ ({p} : Set ℝ²) = gerversSofa := - (h (gerversSofa \ ({p} : Set ℝ²))).1 hsvol - have hp' : p ∈ gerversSofa \ ({p} : Set ℝ²) := by + have hsvol : sofaConstant = volume (g \ ({p} : Set ℝ²)) := hvol.trans hmeasure.symm + have hset : g \ ({p} : Set ℝ²) = g := (h (g \ ({p} : Set ℝ²))).1 hsvol + have hp' : p ∈ g \ ({p} : Set ℝ²) := by rw [hset] exact hp exact hp'.2 (by simp) -#print axioms not_literal_uniqueness +/-- The repository's literal uniqueness conjecture is therefore false as written. This specialization +mentions `gerversSofa`, whose current definition depends on the admitted Gerver-constant existence +statement; the general theorem above is the clean axiom-audited result. -/ +@[category test, AMS 49] +theorem not_literal_uniqueness : + ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa) := + no_literal_volume_unique gerversSofa end MovingSofa From 609db2ec4b5bca284846e4e3797f65ab1dc80bd9 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:40:10 -0700 Subject: [PATCH 08/10] Audit generalized moving-sofa refutation --- .github/workflows/low-hanging-fruit-audit.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/low-hanging-fruit-audit.yml b/.github/workflows/low-hanging-fruit-audit.yml index 826044406d..61bbda292b 100644 --- a/.github/workflows/low-hanging-fruit-audit.yml +++ b/.github/workflows/low-hanging-fruit-audit.yml @@ -53,7 +53,7 @@ jobs: cat > /tmp/LowHangingAxioms.lean <<'EOF' import FormalConjectures.Other.LowHangingFruitAudit #print axioms DedekindNumber.M_eq_via_antichains - #print axioms MovingSofa.not_literal_uniqueness + #print axioms MovingSofa.no_literal_volume_unique EOF lake env lean /tmp/LowHangingAxioms.lean 2>&1 | tee /tmp/low-hanging-axioms.log ! grep -E 'sorryAx|Lean\.ofReduceBool|Lean\.trustCompiler' /tmp/low-hanging-axioms.log From e24f08e749b83c4d3eb4a39b34bc619282a3beef Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:45:27 -0700 Subject: [PATCH 09/10] Remove obsolete duplicate audit module --- FormalConjecturesTest/LowHangingFruit.lean | 62 ---------------------- 1 file changed, 62 deletions(-) delete mode 100644 FormalConjecturesTest/LowHangingFruit.lean diff --git a/FormalConjecturesTest/LowHangingFruit.lean b/FormalConjecturesTest/LowHangingFruit.lean deleted file mode 100644 index 920c866667..0000000000 --- a/FormalConjecturesTest/LowHangingFruit.lean +++ /dev/null @@ -1,62 +0,0 @@ -/- -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 -import FormalConjectures.Wikipedia.MovingSofa - -namespace DedekindNumber - -@[category test, AMS 5 6] -theorem M_eq_low_hanging : M = answer(sorry) := by - exact M_eq_kisielewiczFormula - -#print axioms M_eq_low_hanging - -end DedekindNumber - -namespace MovingSofa - -open MeasureTheory -open scoped ENNReal EuclideanGeometry - -@[category test, AMS 49] -theorem not_literal_uniqueness : - ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa) := by - intro h - have hvol : sofaConstant = volume gerversSofa := (h gerversSofa).2 rfl - have hpos : 0 < volume gerversSofa := by - rw [← hvol] - exact lt_of_lt_of_le (by norm_num) one_le_sofaConstant - have hne : gerversSofa.Nonempty := by - by_contra hne - have hempty : gerversSofa = ∅ := Set.not_nonempty_iff_eq_empty.mp hne - simp [hempty] at hpos - obtain ⟨p, hp⟩ := hne - have hmeasure : - volume (gerversSofa \ ({p} : Set ℝ²)) = volume gerversSofa := by - exact measure_sdiff_null (by simp) - have hsvol : sofaConstant = volume (gerversSofa \ ({p} : Set ℝ²)) := - hvol.trans hmeasure.symm - have hset : gerversSofa \ ({p} : Set ℝ²) = gerversSofa := - (h (gerversSofa \ ({p} : Set ℝ²))).1 hsvol - have hp' : p ∈ gerversSofa \ ({p} : Set ℝ²) := by - rw [hset] - exact hp - exact hp'.2 (by simp) - -#print axioms not_literal_uniqueness - -end MovingSofa From ea37fdb4d7067db942cc65f501349ac173de1f31 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:49:21 -0700 Subject: [PATCH 10/10] Keep only axiom-clean audit results --- .../Other/LowHangingFruitAudit.lean | 19 ++----------------- 1 file changed, 2 insertions(+), 17 deletions(-) diff --git a/FormalConjectures/Other/LowHangingFruitAudit.lean b/FormalConjectures/Other/LowHangingFruitAudit.lean index 89edbd8bc8..a69d045159 100644 --- a/FormalConjectures/Other/LowHangingFruitAudit.lean +++ b/FormalConjectures/Other/LowHangingFruitAudit.lean @@ -20,24 +20,17 @@ import FormalConjectures.Wikipedia.MovingSofa /-! # Low-hanging fruit audit -This temporary module checks two candidate formal-conjectures targets before editing their -source declarations. +Clean formal consequences found while auditing two apparently easy open declarations. -/ namespace DedekindNumber /-- A clean formal answer to the underspecified `M_eq` declaration using the already-proved -antichain characterization. -/ +antichain characterization. This does not prove the intended efficient Kisielewicz formula. -/ @[category test, AMS 5 6] theorem M_eq_via_antichains : M = answer(M') := by exact M_eq_M' -/-- The mathematically intended Kisielewicz answer, audited separately because the source theorem -still contains `sorry`. -/ -@[category test, AMS 5 6] -theorem M_eq_via_kisielewicz : M = answer(kisielewiczFormula) := by - exact M_eq_kisielewiczFormula - end DedekindNumber namespace MovingSofa @@ -68,12 +61,4 @@ theorem no_literal_volume_unique (g : Set ℝ²) : exact hp exact hp'.2 (by simp) -/-- The repository's literal uniqueness conjecture is therefore false as written. This specialization -mentions `gerversSofa`, whose current definition depends on the admitted Gerver-constant existence -statement; the general theorem above is the clean axiom-audited result. -/ -@[category test, AMS 49] -theorem not_literal_uniqueness : - ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa) := - no_literal_volume_unique gerversSofa - end MovingSofa