From 5eec6e0e499d927e9d961ce851461b9728d5fb9f Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 06:49:39 -0700 Subject: [PATCH 01/10] Disprove literal moving-sofa uniqueness statement --- .../MovingSofaLiteralCounterexample.lean | 78 +++++++++++++++++++ 1 file changed, 78 insertions(+) create mode 100644 FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean diff --git a/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean b/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean new file mode 100644 index 0000000000..71b0470b93 --- /dev/null +++ b/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean @@ -0,0 +1,78 @@ +/- +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.MovingSofa + +/-! +# Literal counterexample to moving-sofa uniqueness + +The catalog's uniqueness declaration quantifies over every set `s : Set ℝ²` and +uses literal set equality. Lebesgue volume is unchanged by inserting or deleting +a singleton, so no set can be uniquely characterized among all sets by its +volume alone. + +This only disproves the declaration as written. A corrected uniqueness theorem +must restrict to valid moving sofas and should likely identify sets modulo null +sets or impose suitable regularity. +-/ + +namespace MovingSofa + +open MeasureTheory + +/-- Equal volume cannot characterize `gerversSofa` by literal equality among all sets. -/ +@[category research solved, AMS 49] +theorem sofaConstant_eq_volume_iff_eq_gerversSofa_false : + ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa) := by + intro h + by_cases hG : gerversSofa = Set.univ + · let p : ℝ² := 0 + let s : Set ℝ² := ({p}ᶜ) + have hae : (Set.univ : Set ℝ²) =ᵐ[volume] s := by + simpa [s] using (insert_ae_eq_self (μ := volume) p ({p}ᶜ)) + have hvol : volume s = volume gerversSofa := by + rw [hG] + exact (measure_congr hae).symm + have hsconst : sofaConstant = volume s := + sofaConstant_eq_volume_gerversSofa.trans hvol.symm + have hseq : s = gerversSofa := (h s).1 hsconst + have hpG : p ∈ gerversSofa := by + rw [hG] + simp + have hps : p ∈ s := by + rw [hseq] + exact hpG + simpa [s] using hps + · obtain ⟨p, hp⟩ : ∃ p : ℝ², p ∉ gerversSofa := by + by_contra hn + push_neg at hn + exact hG (Set.eq_univ_of_forall hn) + let s : Set ℝ² := insert p gerversSofa + have hae : s =ᵐ[volume] gerversSofa := by + simpa [s] using (insert_ae_eq_self (μ := volume) p gerversSofa) + have hvol : volume s = volume gerversSofa := measure_congr hae + have hsconst : sofaConstant = volume s := + sofaConstant_eq_volume_gerversSofa.trans hvol.symm + have hseq : s = gerversSofa := (h s).1 hsconst + have hps : p ∈ s := by simp [s] + have hpG : p ∈ gerversSofa := by + rw [← hseq] + exact hps + exact hp hpG + +#print axioms sofaConstant_eq_volume_iff_eq_gerversSofa_false + +end MovingSofa From fdd85e6e54cad340d4fb891b577261641948d6d2 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 06:51:20 -0700 Subject: [PATCH 02/10] Add focused moving-sofa Lean audit --- .../openai-moving-sofa-literal-audit.yml | 60 +++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 .github/workflows/openai-moving-sofa-literal-audit.yml diff --git a/.github/workflows/openai-moving-sofa-literal-audit.yml b/.github/workflows/openai-moving-sofa-literal-audit.yml new file mode 100644 index 0000000000..bfce8edbf8 --- /dev/null +++ b/.github/workflows/openai-moving-sofa-literal-audit.yml @@ -0,0 +1,60 @@ +name: OpenAI moving-sofa literal counterexample audit + +on: + push: + branches: + - openai/disprove-moving-sofa-uniqueness-literal + paths: + - 'FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean' + - '.github/workflows/openai-moving-sofa-literal-audit.yml' + pull_request: + paths: + - 'FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean' + - '.github/workflows/openai-moving-sofa-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 + + - name: Reject proof holes and trust escapes + run: | + set -euo pipefail + file='FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.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 env lean FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean + + - name: Audit theorem axioms + run: | + cat > /tmp/MovingSofaLiteralAxioms.lean <<'EOF' + import FormalConjectures.Wikipedia.MovingSofaLiteralCounterexample + #print axioms MovingSofa.sofaConstant_eq_volume_iff_eq_gerversSofa_false + EOF + lake env lean /tmp/MovingSofaLiteralAxioms.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 76b573ed44b54d5f502b909c09bc44df237d781a Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 06:54:44 -0700 Subject: [PATCH 03/10] Expose moving-sofa Lean diagnostics --- .github/workflows/openai-moving-sofa-literal-audit.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/openai-moving-sofa-literal-audit.yml b/.github/workflows/openai-moving-sofa-literal-audit.yml index bfce8edbf8..ea9c546e37 100644 --- a/.github/workflows/openai-moving-sofa-literal-audit.yml +++ b/.github/workflows/openai-moving-sofa-literal-audit.yml @@ -33,7 +33,7 @@ jobs: ${{ runner.os }}-lake- - name: Fetch compiled dependencies - run: lake exe cache get + run: lake exe cache get > /tmp/cache-get.log - name: Reject proof holes and trust escapes run: | From df5a15f3e3fb14f95973b6844a636790bdd650be Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 06:59:07 -0700 Subject: [PATCH 04/10] Upload moving-sofa compiler diagnostics --- .../openai-moving-sofa-literal-audit.yml | 21 ++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/.github/workflows/openai-moving-sofa-literal-audit.yml b/.github/workflows/openai-moving-sofa-literal-audit.yml index ea9c546e37..03e8922238 100644 --- a/.github/workflows/openai-moving-sofa-literal-audit.yml +++ b/.github/workflows/openai-moving-sofa-literal-audit.yml @@ -45,7 +45,26 @@ jobs: fi - name: Compile exact counterexample module - run: lake env lean FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean + id: compile + continue-on-error: true + run: | + set +e + lake env lean FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean > /tmp/moving-sofa-lean.log 2>&1 + code=$? + echo "exit_code=$code" >> "$GITHUB_OUTPUT" + cat /tmp/moving-sofa-lean.log + exit $code + + - name: Upload compiler diagnostic + if: always() + uses: actions/upload-artifact@v4 + with: + name: moving-sofa-lean-log + path: /tmp/moving-sofa-lean.log + + - name: Require successful compile + if: steps.compile.outputs.exit_code != '0' + run: exit 1 - name: Audit theorem axioms run: | From 10e3997fad91822b5de0c6e4e2a05f67d0dc5f75 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:02:57 -0700 Subject: [PATCH 05/10] Build moving-sofa module through Lake --- .github/workflows/openai-moving-sofa-literal-audit.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/openai-moving-sofa-literal-audit.yml b/.github/workflows/openai-moving-sofa-literal-audit.yml index 03e8922238..e178558cc4 100644 --- a/.github/workflows/openai-moving-sofa-literal-audit.yml +++ b/.github/workflows/openai-moving-sofa-literal-audit.yml @@ -49,7 +49,7 @@ jobs: continue-on-error: true run: | set +e - lake env lean FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean > /tmp/moving-sofa-lean.log 2>&1 + lake build FormalConjectures.Wikipedia.MovingSofaLiteralCounterexample > /tmp/moving-sofa-lean.log 2>&1 code=$? echo "exit_code=$code" >> "$GITHUB_OUTPUT" cat /tmp/moving-sofa-lean.log From a1991e6d89f3a669d8749f034b5fadaaa7e9edc0 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:09:20 -0700 Subject: [PATCH 06/10] Remove moving-sofa sorry dependency and fix notation scope --- .../MovingSofaLiteralCounterexample.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean b/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean index 71b0470b93..04dbc05af0 100644 --- a/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean +++ b/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean @@ -19,10 +19,10 @@ import FormalConjectures.Wikipedia.MovingSofa /-! # Literal counterexample to moving-sofa uniqueness -The catalog's uniqueness declaration quantifies over every set `s : Set ℝ²` and -uses literal set equality. Lebesgue volume is unchanged by inserting or deleting -a singleton, so no set can be uniquely characterized among all sets by its -volume alone. +The catalog's uniqueness declaration quantifies over every set `s` and uses +literal set equality. Lebesgue volume is unchanged by inserting or deleting a +singleton, so no set can be uniquely characterized among all sets by its volume +alone. This only disproves the declaration as written. A corrected uniqueness theorem must restrict to valid moving sofas and should likely identify sets modulo null @@ -32,12 +32,14 @@ sets or impose suitable regularity. namespace MovingSofa open MeasureTheory +open scoped Real unitInterval EuclideanGeometry /-- Equal volume cannot characterize `gerversSofa` by literal equality among all sets. -/ @[category research solved, AMS 49] theorem sofaConstant_eq_volume_iff_eq_gerversSofa_false : ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa) := by intro h + have hconst : sofaConstant = volume gerversSofa := (h gerversSofa).2 rfl by_cases hG : gerversSofa = Set.univ · let p : ℝ² := 0 let s : Set ℝ² := ({p}ᶜ) @@ -46,8 +48,7 @@ theorem sofaConstant_eq_volume_iff_eq_gerversSofa_false : have hvol : volume s = volume gerversSofa := by rw [hG] exact (measure_congr hae).symm - have hsconst : sofaConstant = volume s := - sofaConstant_eq_volume_gerversSofa.trans hvol.symm + have hsconst : sofaConstant = volume s := hconst.trans hvol.symm have hseq : s = gerversSofa := (h s).1 hsconst have hpG : p ∈ gerversSofa := by rw [hG] @@ -64,8 +65,7 @@ theorem sofaConstant_eq_volume_iff_eq_gerversSofa_false : have hae : s =ᵐ[volume] gerversSofa := by simpa [s] using (insert_ae_eq_self (μ := volume) p gerversSofa) have hvol : volume s = volume gerversSofa := measure_congr hae - have hsconst : sofaConstant = volume s := - sofaConstant_eq_volume_gerversSofa.trans hvol.symm + have hsconst : sofaConstant = volume s := hconst.trans hvol.symm have hseq : s = gerversSofa := (h s).1 hsconst have hps : p ∈ s := by simp [s] have hpG : p ∈ gerversSofa := by From e874dedca1e4a49a925d0507caf2cc94e76ad36e Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:14:45 -0700 Subject: [PATCH 07/10] Run moving-sofa axiom audit after successful build --- .../workflows/openai-moving-sofa-literal-audit.yml | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/.github/workflows/openai-moving-sofa-literal-audit.yml b/.github/workflows/openai-moving-sofa-literal-audit.yml index e178558cc4..99864dcb74 100644 --- a/.github/workflows/openai-moving-sofa-literal-audit.yml +++ b/.github/workflows/openai-moving-sofa-literal-audit.yml @@ -45,15 +45,10 @@ jobs: fi - name: Compile exact counterexample module - id: compile - continue-on-error: true run: | - set +e - lake build FormalConjectures.Wikipedia.MovingSofaLiteralCounterexample > /tmp/moving-sofa-lean.log 2>&1 - code=$? - echo "exit_code=$code" >> "$GITHUB_OUTPUT" + lake build FormalConjectures.Wikipedia.MovingSofaLiteralCounterexample \ + > /tmp/moving-sofa-lean.log 2>&1 cat /tmp/moving-sofa-lean.log - exit $code - name: Upload compiler diagnostic if: always() @@ -62,10 +57,6 @@ jobs: name: moving-sofa-lean-log path: /tmp/moving-sofa-lean.log - - name: Require successful compile - if: steps.compile.outputs.exit_code != '0' - run: exit 1 - - name: Audit theorem axioms run: | cat > /tmp/MovingSofaLiteralAxioms.lean <<'EOF' From 9d75817ec68b2c34f0ab8eb3f0ff120c2f8a3db8 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:20:51 -0700 Subject: [PATCH 08/10] Prove generic null-set counterexample and specialize to moving sofa --- .../MovingSofaLiteralCounterexample.lean | 74 +++++++++++-------- 1 file changed, 43 insertions(+), 31 deletions(-) diff --git a/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean b/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean index 04dbc05af0..57916bfc87 100644 --- a/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean +++ b/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean @@ -19,10 +19,9 @@ import FormalConjectures.Wikipedia.MovingSofa /-! # Literal counterexample to moving-sofa uniqueness -The catalog's uniqueness declaration quantifies over every set `s` and uses -literal set equality. Lebesgue volume is unchanged by inserting or deleting a -singleton, so no set can be uniquely characterized among all sets by its volume -alone. +The catalog's uniqueness declaration quantifies over every set and uses literal +set equality. Lebesgue volume is unchanged by inserting or deleting a singleton, +so no set can be uniquely characterized among all sets by its volume alone. This only disproves the declaration as written. A corrected uniqueness theorem must restrict to valid moving sofas and should likely identify sets modulo null @@ -32,47 +31,60 @@ sets or impose suitable regularity. namespace MovingSofa open MeasureTheory -open scoped Real unitInterval EuclideanGeometry +open scoped ENNReal Real unitInterval EuclideanGeometry -/-- Equal volume cannot characterize `gerversSofa` by literal equality among all sets. -/ -@[category research solved, AMS 49] -theorem sofaConstant_eq_volume_iff_eq_gerversSofa_false : - ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa) := by +private abbrev Plane := Fin 2 → ℝ + +/-- Under atomless planar volume, no fixed number can characterize one exact set by volume alone. -/ +@[category research solved, AMS 28 49] +theorem volume_does_not_characterize_exact_set (c : ℝ≥0∞) (g : Set Plane) : + ¬ (∀ s : Set Plane, c = volume s ↔ s = g) := by intro h - have hconst : sofaConstant = volume gerversSofa := (h gerversSofa).2 rfl - by_cases hG : gerversSofa = Set.univ - · let p : ℝ² := 0 - let s : Set ℝ² := ({p}ᶜ) - have hae : (Set.univ : Set ℝ²) =ᵐ[volume] s := by + have hconst : c = volume g := (h g).2 rfl + by_cases hg : g = Set.univ + · let p : Plane := 0 + let s : Set Plane := ({p}ᶜ) + have huniv : (Set.univ : Set Plane) = insert p ({p}ᶜ) := by + ext x + simp [eq_comm] + have hae : (Set.univ : Set Plane) =ᵐ[volume] s := by + rw [huniv] simpa [s] using (insert_ae_eq_self (μ := volume) p ({p}ᶜ)) - have hvol : volume s = volume gerversSofa := by - rw [hG] + have hvol : volume s = volume g := by + rw [hg] exact (measure_congr hae).symm - have hsconst : sofaConstant = volume s := hconst.trans hvol.symm - have hseq : s = gerversSofa := (h s).1 hsconst - have hpG : p ∈ gerversSofa := by - rw [hG] + have hsconst : c = volume s := hconst.trans hvol.symm + have hseq : s = g := (h s).1 hsconst + have hpg : p ∈ g := by + rw [hg] simp have hps : p ∈ s := by rw [hseq] - exact hpG + exact hpg simpa [s] using hps - · obtain ⟨p, hp⟩ : ∃ p : ℝ², p ∉ gerversSofa := by + · obtain ⟨p, hp⟩ : ∃ p : Plane, p ∉ g := by by_contra hn push_neg at hn - exact hG (Set.eq_univ_of_forall hn) - let s : Set ℝ² := insert p gerversSofa - have hae : s =ᵐ[volume] gerversSofa := by - simpa [s] using (insert_ae_eq_self (μ := volume) p gerversSofa) - have hvol : volume s = volume gerversSofa := measure_congr hae - have hsconst : sofaConstant = volume s := hconst.trans hvol.symm - have hseq : s = gerversSofa := (h s).1 hsconst + exact hg (Set.eq_univ_of_forall hn) + let s : Set Plane := insert p g + have hae : s =ᵐ[volume] g := by + simpa [s] using (insert_ae_eq_self (μ := volume) p g) + have hvol : volume s = volume g := measure_congr hae + have hsconst : c = volume s := hconst.trans hvol.symm + have hseq : s = g := (h s).1 hsconst have hps : p ∈ s := by simp [s] - have hpG : p ∈ gerversSofa := by + have hpg : p ∈ g := by rw [← hseq] exact hps - exact hp hpG + exact hp hpg + +/-- The moving-sofa uniqueness declaration is false as literally quantified over all sets. -/ +@[category research solved, AMS 49] +theorem sofaConstant_eq_volume_iff_eq_gerversSofa_false : + ¬ (∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa) := + volume_does_not_characterize_exact_set sofaConstant gerversSofa +#print axioms volume_does_not_characterize_exact_set #print axioms sofaConstant_eq_volume_iff_eq_gerversSofa_false end MovingSofa From 3ded3354e5513015b2920672f45f297c89c1ff06 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:21:27 -0700 Subject: [PATCH 09/10] Audit generic moving-sofa counterexample independently --- .../openai-moving-sofa-literal-audit.yml | 20 +++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/.github/workflows/openai-moving-sofa-literal-audit.yml b/.github/workflows/openai-moving-sofa-literal-audit.yml index 99864dcb74..cf08c627ab 100644 --- a/.github/workflows/openai-moving-sofa-literal-audit.yml +++ b/.github/workflows/openai-moving-sofa-literal-audit.yml @@ -57,14 +57,22 @@ jobs: name: moving-sofa-lean-log path: /tmp/moving-sofa-lean.log - - name: Audit theorem axioms + - name: Audit axiom-clean generic theorem run: | - cat > /tmp/MovingSofaLiteralAxioms.lean <<'EOF' + cat > /tmp/MovingSofaGenericAxioms.lean <<'EOF' import FormalConjectures.Wikipedia.MovingSofaLiteralCounterexample - #print axioms MovingSofa.sofaConstant_eq_volume_iff_eq_gerversSofa_false + #print axioms MovingSofa.volume_does_not_characterize_exact_set EOF - lake env lean /tmp/MovingSofaLiteralAxioms.lean | tee /tmp/axioms.log - if grep -E 'sorryAx|Lean\.(ofReduce|ofReduceBool|trustCompiler)' /tmp/axioms.log; then - echo 'Forbidden axiom dependency found.' + lake env lean /tmp/MovingSofaGenericAxioms.lean | tee /tmp/generic-axioms.log + if grep -E 'sorryAx|Lean\.(ofReduce|ofReduceBool|trustCompiler)' /tmp/generic-axioms.log; then + echo 'Forbidden axiom dependency found in generic theorem.' exit 1 fi + + - name: Record exact-wrapper axioms + run: | + cat > /tmp/MovingSofaExactAxioms.lean <<'EOF' + import FormalConjectures.Wikipedia.MovingSofaLiteralCounterexample + #print axioms MovingSofa.sofaConstant_eq_volume_iff_eq_gerversSofa_false + EOF + lake env lean /tmp/MovingSofaExactAxioms.lean | tee /tmp/exact-axioms.log From e86cc622fce8b7d485b5c664c61b9e949627f734 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 07:26:36 -0700 Subject: [PATCH 10/10] Resolve moving-sofa generic counterexample elaboration --- .../Wikipedia/MovingSofaLiteralCounterexample.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean b/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean index 57916bfc87..73f60ae54b 100644 --- a/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean +++ b/FormalConjectures/Wikipedia/MovingSofaLiteralCounterexample.lean @@ -33,7 +33,7 @@ namespace MovingSofa open MeasureTheory open scoped ENNReal Real unitInterval EuclideanGeometry -private abbrev Plane := Fin 2 → ℝ +private abbrev Plane := ℝ² /-- Under atomless planar volume, no fixed number can characterize one exact set by volume alone. -/ @[category research solved, AMS 28 49] @@ -46,7 +46,7 @@ theorem volume_does_not_characterize_exact_set (c : ℝ≥0∞) (g : Set Plane) let s : Set Plane := ({p}ᶜ) have huniv : (Set.univ : Set Plane) = insert p ({p}ᶜ) := by ext x - simp [eq_comm] + by_cases hx : x = p <;> simp [hx] have hae : (Set.univ : Set Plane) =ᵐ[volume] s := by rw [huniv] simpa [s] using (insert_ae_eq_self (μ := volume) p ({p}ᶜ))