google-deepmind · YaelDillies · Jan 25, 2026 · Jan 25, 2026 · Jan 25, 2026 · Jan 26, 2026
diff --git a/FormalConjectures/Arxiv/1601.03081/UniqueCrystalComponents.lean b/FormalConjectures/Arxiv/1601.03081/UniqueCrystalComponents.lean
@@ -36,7 +36,6 @@ def IsCrystalWithComponents (n a b : ℕ) : Prop :=
 @[category test, AMS 11]
 theorem isCrystalWithComponents_35_5_7 : IsCrystalWithComponents 35 5 7 := by
   norm_num [IsCrystalWithComponents]
-  decide
 
 -- TODO(firsching): show divisibility properties from section 3.
 

diff --git a/FormalConjectures/ErdosProblems/1.lean b/FormalConjectures/ErdosProblems/1.lean
@@ -84,7 +84,8 @@ A finite set of real numbers is said to be sum-distinct if all the subset sums d
 at least $1$.
 -/
 abbrev IsSumDistinctRealSet (A : Finset ℝ) (N : ℕ) : Prop :=
-    A.toSet ⊆ Set.Ioc 0 N ∧ A.powerset.toSet.Pairwise fun S₁ S₂ => 1 ≤ dist (S₁.sum id) (S₂.sum id)
+  ↑A ⊆ Set.Ioc (0 : ℝ) N ∧ (A.powerset : Set (Finset ℝ)).Pairwise fun S₁ S₂ =>
+    1 ≤ dist (S₁.sum id) (S₂.sum id)
 
 /--
 A generalisation of the problem to sets $A \subseteq (0, N]$ of real numbers, such that the subset
@@ -116,7 +117,7 @@ theorem erdos_1.variants.least_N_3 :
       refine Finset.ext_iff.mpr (fun n => ?_)
       simp [show P = {{}, {1}, {2}, {4}, {1, 2}, {1, 4}, {2, 4}, {1, 2, 4}} by decide]
       omega
-    rw [Set.injective_iff_injOn_univ, ← Finset.coe_univ]
+    rw [← Set.injOn_univ, ← Finset.coe_univ]
     have : (Finset.univ.image (fun p : P ↦ ∑ x ∈ p.1, x)).card = (Finset.univ (α := P)).card := by
       rw [this]; aesop
     exact Finset.injOn_of_card_image_eq this

diff --git a/FormalConjectures/ErdosProblems/1052.lean b/FormalConjectures/ErdosProblems/1052.lean
@@ -62,6 +62,8 @@ theorem isUnitaryPerfect_90 : IsUnitaryPerfect 90 := by
 
 @[category test, AMS 11]
 theorem isUnitaryPerfect_87360 : IsUnitaryPerfect 87360 := by
+  -- TODO: Find a quicker proof. This one is too slow.
+  stop
   norm_num [IsUnitaryPerfect, properUnitaryDivisors]
   decide +kernel
 

diff --git a/FormalConjectures/ErdosProblems/1060.lean b/FormalConjectures/ErdosProblems/1060.lean
@@ -22,7 +22,7 @@ import FormalConjectures.Util.ProblemImports
 -/
 
 open Asymptotics Finset Filter Real
-open scoped ArithmeticFunction
+open scoped ArithmeticFunction.sigma
 
 namespace Erdos1060
 

diff --git a/FormalConjectures/ErdosProblems/1061.lean b/FormalConjectures/ErdosProblems/1061.lean
@@ -25,7 +25,7 @@ import FormalConjectures.Util.ProblemImports
 -/
 
 open Filter Asymptotics
-open scoped ArithmeticFunction
+open scoped ArithmeticFunction.sigma
 
 namespace Erdos1061
 

diff --git a/FormalConjectures/ErdosProblems/107.lean b/FormalConjectures/ErdosProblems/107.lean
@@ -31,7 +31,7 @@ namespace Erdos107
 
 /-- The set of $N$ such that any $N$ points in the plane, no three on a line,
 contain a convex $n$-gon. -/
-def cardSet (n : ℕ) := { N | ∀ (pts : Finset ℝ²), pts.card = N → NonTrilinear pts.toSet →
+def cardSet (n : ℕ) := { N | ∀ (pts : Finset ℝ²), pts.card = N → NonTrilinear (pts : Set ℝ²) →
   HasConvexNGon n pts }
 
 /-- The function $f(n)$ specified in `erdos_107`. -/

diff --git a/FormalConjectures/ErdosProblems/1071.lean b/FormalConjectures/ErdosProblems/1071.lean
@@ -37,15 +37,11 @@ Solved affirmatively by [Da85], who gave an explicit construction. -/
 @[category research solved, AMS 52]
 theorem erdos_1071a :
     answer(True) ↔ ∃ S : Finset (ℝ² × ℝ²),
-      (∀ seg ∈ S, dist seg.1 seg.2 = 1 ∧
-        seg.1 0 ∈ Icc 0 1 ∧ seg.1 1 ∈ Icc 0 1 ∧
-        seg.2 0 ∈ Icc 0 1 ∧ seg.2 1 ∈ Icc 0 1) ∧
-      S.toSet.Pairwise SegmentsDisjoint ∧
       Maximal (fun T : Finset (ℝ² × ℝ²) =>
         (∀ seg ∈ T, dist seg.1 seg.2 = 1 ∧
           seg.1 0 ∈ Icc 0 1 ∧ seg.1 1 ∈ Icc 0 1 ∧
           seg.2 0 ∈ Icc 0 1 ∧ seg.2 1 ∈ Icc 0 1) ∧
-        T.toSet.Pairwise SegmentsDisjoint) S := by
+          (T : Set (ℝ² × ℝ²)).Pairwise SegmentsDisjoint) S := by
   sorry
 
 /-- Is there a region $R$ with a maximal set of disjoint unit line segments that is countably infinite? -/

diff --git a/FormalConjectures/ErdosProblems/1084.lean b/FormalConjectures/ErdosProblems/1084.lean
@@ -39,7 +39,7 @@ variable {n : ℕ}
 /-- The maximal number of pairs of points which are distance 1 apart that a set of `n` 1-separated
 points in `ℝ^d` make. -/
 noncomputable def f (d n : ℕ) : ℕ :=
-  ⨆ (s : Finset (ℝ^ d)) (_ : s.card = n) (_ : IsSeparated 1 s.toSet), unitDistNum s
+  ⨆ (s : Finset (ℝ^ d)) (_ : s.card = n) (_ : IsSeparated 1 (s : Set (ℝ^ d))), unitDistNum s
 
 /-- It is easy to check that $f_1(n) = n - 1$. -/
 @[category research solved, AMS 52]

diff --git a/FormalConjectures/ErdosProblems/141.lean b/FormalConjectures/ErdosProblems/141.lean
@@ -43,7 +43,7 @@ theorem first_three_odd_primes : ({3, 5, 7} : Set ℕ).IsPrimeProgressionOfLengt
   use 1
   constructor
   · aesop
-  · norm_num [exists_lt_succ, or_assoc, eq_comm, Set.insert_def,
+  · norm_num [exists_lt_succ_right, or_assoc, eq_comm, Set.insert_def,
     show (2).nth Nat.Prime = 5 from nth_count prime_five,
     show (3).nth Nat.Prime = 7 from Nat.nth_count (by decide : (7).Prime)]
 
@@ -65,7 +65,7 @@ theorem exists_three_consecutive_primes_in_ap : ∃ (s : Set ℕ), s.IsAPAndPrim
     unfold Set.IsAPOfLengthWith
     constructor
     · aesop
-    · norm_num [exists_lt_succ, or_assoc, eq_comm, Set.insert_def]
+    · norm_num [exists_lt_succ_right, or_assoc, eq_comm, Set.insert_def]
   · exact first_three_odd_primes
 
 /--

diff --git a/FormalConjectures/ErdosProblems/153.lean b/FormalConjectures/ErdosProblems/153.lean
@@ -34,7 +34,7 @@ namespace Erdos153
 /-- Define `f n` to be the minimum of
 `∑ (i : Set.Ico 1 ((A + A).card), (s i - s (i - 1)) ^ 2 / n` as `A` ranges over all Sidon sets
 of size `n`, where `s` is an order embedding from `Fin n` into `A`. -/
-noncomputable def f (n : ℕ) : ℝ := ⨅ A : {A : Finset ℕ | A.card = n ∧ IsSidon A},
+noncomputable def f (n : ℕ) : ℝ := ⨅ A : {A : Finset ℕ | A.card = n ∧ IsSidon (A : Set ℕ)},
   let s := (A.1 + A).orderIsoOfFin rfl
   ∑ i : Set.Ico 1 ((A.1 + A).card), (s ⟨i, i.2.2⟩ - s ⟨i - 1, by grind⟩) ^ 2 / (n : ℝ)
 

diff --git a/FormalConjectures/ErdosProblems/158.lean b/FormalConjectures/ErdosProblems/158.lean
@@ -40,6 +40,7 @@ lemma b2_one {A : Set ℕ} : B2 1 A ↔ IsSidon A where
       grind
     wlog h₂ : a₂ ≤ b₂
     · have := this hA _ ha₁ _ hb₂ _ hb₁ _ ha₂
+      clear ha₁ ha₂ hb₁ hb₂
       grind
     have := Set.encard_le_one_iff.1 (hA (a₁ + b₁)) ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ (by simp [*]) (by simp [*])
     grind

diff --git a/FormalConjectures/ErdosProblems/170.lean b/FormalConjectures/ErdosProblems/170.lean
@@ -45,9 +45,8 @@ abbrev TrivialRuler (N : ℕ) : Finset ℕ := Finset.range (N+1)
 /-- Sanity Check: the trivial ruler is actually a perfect ruler if $K \geq N$ -/
 @[category API, AMS 05]
 lemma trivial_ruler_is_perfect (N : ℕ) : TrivialRuler N ∈ PerfectRulersLengthN N := by
-    simp only [PerfectRulersLengthN, Finset.mem_filter, Finset.mem_powerset, Finset.range_subset,
-      add_le_add_iff_right]
-    exact ⟨by rfl, fun k hk => ⟨0, by simp, k, hk, rfl⟩⟩
+    simp only [PerfectRulersLengthN, Finset.mem_filter, Finset.mem_powerset, Finset.range_subset]
+    exact ⟨by simp, fun k hk => ⟨0, by simp, k, hk, rfl⟩⟩
 
 /-- We define a function `F N` as the minimum cardinality of an `N`-perfect ruler of length `N`. -/
 def F (N : ℕ) : ℕ :=

diff --git a/FormalConjectures/ErdosProblems/194.lean b/FormalConjectures/ErdosProblems/194.lean
@@ -36,7 +36,7 @@ The answer is no, even for $k=3$, as shown by Ardal, Brown, and Jungić [ABJ11].
 @[category research solved, AMS 5]
 theorem erdos_194 :
   answer(False) ↔ ∀ k ≥ 3, ∀ r : ℝ → ℝ → Prop, IsStrictTotalOrder ℝ r →
-    ∃ s : List ℝ, s.IsAPOfLength k ∧ (s.Sorted r ∨ s.Sorted (flip r)) := by
+    ∃ s : List ℝ, s.IsAPOfLength k ∧ (s.Pairwise r ∨ s.Pairwise (flip r)) := by
   sorry
 
 end Erdos194
diff --git a/FormalConjectures/ErdosProblems/219.lean b/FormalConjectures/ErdosProblems/219.lean
@@ -32,14 +32,19 @@ def primeArithmeticProgressions : Set (Set ℕ) :=
 
 @[category test, AMS 5 11]
 theorem primeArithmeticProgression_3_5_7 : {3, 5, 7} ∈ primeArithmeticProgressions := by
-  simp [primeArithmeticProgressions, Set.IsAPOfLength, Set.IsAPOfLengthWith]
+  simp only [primeArithmeticProgressions, gt_iff_lt, Set.IsAPOfLength, Set.IsAPOfLengthWith,
+    smul_eq_mul, exists_prop, exists_and_left, existsAndEq, true_and, Set.mem_setOf_eq,
+    Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp, forall_eq,
+    ENat.card_eq_coe_fintype_card, Fintype.card_ofFinset, Set.toFinset_insert,
+    Set.toFinset_singleton, Finset.mem_insert, Nat.reduceEqDiff, Finset.mem_singleton, or_self,
+    not_false_eq_true, Finset.card_insert_of_notMem, Finset.card_singleton, Nat.reduceAdd,
+    Nat.cast_ofNat, Nat.ofNat_pos, Nat.cast_lt_ofNat]
   refine ⟨by norm_num, ⟨3, 2, Set.ext fun x => ?_⟩⟩
-  refine ⟨fun h => ?_, fun ⟨w, ⟨hl, hr⟩⟩ => by interval_cases w <;> simp_all⟩
-  cases h with
-  | inl hl => simp [hl]
-  | inr hr => cases hr with
-    | inl hrl => simpa [hrl] using ⟨1, by simp⟩
-    | inr hrr => simpa [hrr] using ⟨2, by aesop⟩
+  refine ⟨?_, fun ⟨w, ⟨hl, hr⟩⟩ => by interval_cases w <;> simp_all⟩
+  rintro (rfl | rfl | rfl)
+  · simp
+  · simpa using ⟨1, by simp⟩
+  · simpa using ⟨2, by simp⟩
 
 @[category test, AMS 5 11]
 theorem not_primeArithmeticProgression_1_2 : ¬{1, 2} ∈ primeArithmeticProgressions := by

diff --git a/FormalConjectures/ErdosProblems/248.lean b/FormalConjectures/ErdosProblems/248.lean
@@ -24,7 +24,7 @@ import FormalConjectures.Util.ProblemImports
 - [TaTe25] T. Tao and J. Teräväinen, Quantitative correlations and some problems on prime factors of consecutive integers. arXiv:2512.01739 (2025).
 -/
 
-open scoped ArithmeticFunction
+open scoped ArithmeticFunction.omega
 
 namespace Erdos248
 

diff --git a/FormalConjectures/ErdosProblems/250.lean b/FormalConjectures/ErdosProblems/250.lean
@@ -22,7 +22,7 @@ import FormalConjectures.Util.ProblemImports
 *Reference:* [erdosproblems.com/250](https://www.erdosproblems.com/250)
 -/
 
-open scoped ArithmeticFunction
+open scoped ArithmeticFunction.sigma
 
 namespace Erdos250
 

diff --git a/FormalConjectures/ErdosProblems/252.lean b/FormalConjectures/ErdosProblems/252.lean
@@ -35,8 +35,7 @@ import FormalConjectures.Wikipedia.Schinzel
     arXiv:2209.11124 (2022).
 -/
 
-open scoped Nat
-open ArithmeticFunction
+open scoped Nat ArithmeticFunction.sigma
 
 namespace Erdos252
 

diff --git a/FormalConjectures/ErdosProblems/259.lean b/FormalConjectures/ErdosProblems/259.lean
@@ -22,7 +22,7 @@ import FormalConjectures.Util.ProblemImports
 *Reference:* [erdosproblems.com/259](https://www.erdosproblems.com/259)
 -/
 
-open scoped ArithmeticFunction
+open scoped ArithmeticFunction.Moebius
 
 namespace Erdos259
 

diff --git a/FormalConjectures/ErdosProblems/26.lean b/FormalConjectures/ErdosProblems/26.lean
@@ -45,7 +45,8 @@ theorem not_isThick_of_geom_one_lt (r : ℕ) (hr : r > 1) : ¬IsThick fun n :
 
 @[category test, AMS 11]
 theorem isThick_const {ι : Type*} [Infinite ι] (r : ℕ) (h : r > 0) : IsThick fun _ : ι ↦ r := by
-  field_simp [IsThick, h, summable_const_iff]
+  simp only [IsThick, one_div, summable_const_iff, inv_eq_zero, Nat.cast_eq_zero]
+  exact Nat.ne_zero_of_lt h
 
 /-- The set of multiples of a sequence $(a_i)$ is $\{na_i | n \in \mathbb{N}, i\}$. -/
 def MultiplesOf {ι : Type*} (A : ι → ℕ) : Set ℕ := Set.range fun (n, i) ↦ n * A i
@@ -69,7 +70,8 @@ theorem isBehrend_of_contains_one {ι : Type*} (A : ι → ℕ) (h : 1 ∈ Set.r
     IsBehrend A := by
   rw [IsBehrend, Set.HasDensity]
   exact tendsto_atTop_of_eventually_const (i₀ := 1) fun n hn ↦ by
-    field_simp [multiplesOf_eq_univ A h, Set.partialDensity]
+    simp [multiplesOf_eq_univ A h, Set.partialDensity]
+    lia
 
 @[category test, AMS 11]
 theorem isWeaklyBehrend_of_ge_one {ι : Type*} (A : ι → ℕ) {ε : ℝ} (hε : 1 ≤ ε) :

diff --git a/FormalConjectures/ErdosProblems/298.lean b/FormalConjectures/ErdosProblems/298.lean
@@ -35,15 +35,15 @@ Note: The solution to this problem has been formalized in Lean 3 by T. Bloom and
 https://github.com/b-mehta/unit-fractions -/
 @[category research solved, AMS 11]
 theorem erdos_298 : answer(True) ↔ (∀ (A : Set ℕ), 0 ∉ A → A.HasPosDensity →
-    ∃ (S : Finset ℕ), S.toSet ⊆ A ∧ ∑ n ∈ S, (1 / n : ℚ) = 1) := by
+    ∃ (S : Finset ℕ), ↑S ⊆ A ∧ ∑ n ∈ S, (1 / n : ℚ) = 1) := by
   sorry
 
 /--
 In [Bl21] it is proved under the weaker assumption that `A` only has positive upper density.
 -/
 @[category research solved, AMS 11]
 theorem erdos_298.variants.upper_density : answer(True) ↔ (∀ (A : Set ℕ), 0 ∉ A → 0 < A.upperDensity →
-    ∃ (S : Finset ℕ), S.toSet ⊆ A ∧ ∑ n ∈ S, (1 / n : ℚ) = 1) := by
+    ∃ (S : Finset ℕ), ↑S ⊆ A ∧ ∑ n ∈ S, (1 / n : ℚ) = 1) := by
   sorry
 
 end Erdos298
diff --git a/FormalConjectures/ErdosProblems/299.lean b/FormalConjectures/ErdosProblems/299.lean
@@ -49,7 +49,7 @@ density) then there is a finite $S \subset A$ such that $\sum_{n \in S} \frac{1}
 -/
 @[category research solved, AMS 11 40]
 theorem erdos_299.variants.density : ∀ (A : Set ℕ), 0 ∉ A → 0 < A.upperDensity →
-    ∃ S : Finset ℕ, S.toSet ⊆ A ∧ ∑ n ∈ S, (1 : ℝ) / n = 1 := by
+    ∃ S : Finset ℕ, ↑S ⊆ A ∧ ∑ n ∈ S, (1 : ℝ) / n = 1 := by
   sorry
 
 end Erdos299
diff --git a/FormalConjectures/ErdosProblems/306.lean b/FormalConjectures/ErdosProblems/306.lean
@@ -23,7 +23,8 @@ import FormalConjectures.Util.ProblemImports
 *Reference:* [erdosproblems.com/306](https://www.erdosproblems.com/306)
 -/
 
-open scoped ArithmeticFunction
+open ArithmeticFunction
+open scoped omega Omega
 
 namespace Erdos306
 

diff --git a/FormalConjectures/ErdosProblems/317.lean b/FormalConjectures/ErdosProblems/317.lean
@@ -71,7 +71,6 @@ theorem erdos_317.variants.counterexample : ¬ (∀  δ : (Fin 4) → ℚ, δ ''
   push_neg
   use ![0, 1, -1, -1]
   norm_num [Finset.sum]
-  refine ⟨by grind, le_of_eq ?_⟩
-  exact (abs_of_nonneg (by norm_num)).trans (one_div _)
+  exact ⟨by grind, by simp; rfl⟩
 
 end Erdos317
diff --git a/FormalConjectures/ErdosProblems/318.lean b/FormalConjectures/ErdosProblems/318.lean
@@ -40,7 +40,7 @@ def P₁ (A : Set ℕ) : Prop := ∀ (f : ℕ → ℝ),
   f ∘ (Subtype.val : (A \ {0} : Set ℕ) → ℕ) ≠ (fun _ => 1) →
   f ∘ (Subtype.val : (A \ {0} : Set ℕ) → ℕ) ≠ (fun _ => - 1) →
   Set.range f ⊆ {1, -1} →
-  ∃ S : Finset ℕ, S.Nonempty ∧ S.toSet ⊆ A \ {0} ∧ ∑ n ∈ S, f n / n = 0
+  ∃ S : Finset ℕ, S.Nonempty ∧ ↑S ⊆ A \ {0} ∧ ∑ n ∈ S, f n / n = 0
 
 /-- `ℕ` has property `P₁`. This is proved in [ErSt75]. -/
 @[category research solved, AMS 11]

diff --git a/FormalConjectures/ErdosProblems/329.lean b/FormalConjectures/ErdosProblems/329.lean
@@ -83,7 +83,7 @@ then the maximum density would be 1.
 -/
 @[category research open, AMS 5 11]
 theorem erdos_329.of_sub_perfectDifferenceSet :
-    (∀ (A : Finset ℕ), IsSidon A → ∃ (D : Set ℕ) (n : ℕ),
+    (∀ (A : Finset ℕ), IsSidon (A : Set ℕ) → ∃ (D : Set ℕ) (n : ℕ),
       ↑A ⊆ D ∧ IsPerfectDifferenceSet D n) →
     sSup {sidonUpperDensity A | (A : Set ℕ) (_ : IsSidon A)} = 1 := by
   sorry
@@ -95,7 +95,7 @@ can be embedded in a perfect difference set.
 @[category research open, AMS 5 11]
 theorem erdos_329.converse_implication :
     (sSup {sidonUpperDensity A | (A : Set ℕ) (_ : IsSidon A)} = 1) →
-    (∀ (A : Finset ℕ), IsSidon A → ∃ (D : Set ℕ) (n : ℕ),
+    (∀ (A : Finset ℕ), IsSidon (A : Set ℕ) → ∃ (D : Set ℕ) (n : ℕ),
       ↑A ⊆ D ∧ IsPerfectDifferenceSet D n) := by
   sorry
 

diff --git a/FormalConjectures/ErdosProblems/340.lean b/FormalConjectures/ErdosProblems/340.lean
@@ -30,26 +30,28 @@ namespace Erdos340
 /-- Given a finite Sidon set `A` and a lower bound `m`, `go` finds the smallest number `m' ≥ m`
 such that `A ∪ {m'}` is Sidon. If `A` is empty then this returns the value `m`. Note that
 the lower bound is required to avoid `0` being a contender in some cases. -/
-private def greedySidon.go (A : Finset ℕ) (hA : IsSidon A) (m : ℕ) :
-    {m' : ℕ // m' ≥ m ∧ m' ∉ A ∧ IsSidon (A ∪ {m'})} :=
+private def greedySidon.go (A : Finset ℕ) (hA : IsSidon (A : Set ℕ)) (m : ℕ) :
+    {m' : ℕ // m' ≥ m ∧ m' ∉ A ∧ IsSidon (↑(A ∪ {m'}) : Set ℕ)} :=
   if h : A.Nonempty then
-    ⟨Nat.find (hA.exists_insert_ge h m), Nat.find_spec (hA.exists_insert_ge h m)⟩
+    haveI : ∃ m', m' ≥ m ∧ m' ∉ A ∧ IsSidon (↑(A ∪ {m'}) : Set ℕ) := by
+      simpa [and_assoc] using hA.exists_insert_ge h m
+    ⟨Nat.find this, Nat.find_spec this⟩
   else ⟨m, by simp_all [IsSidon]⟩
 
 @[category test, AMS 5]
 theorem greedySidon_go_singleton_two : (greedySidon.go {1} (by simp [IsSidon]) 2).val = 2 := by
-  decide
+  decide +native
 
 @[category test, AMS 5]
 theorem greedySidon_go_pair_three : (greedySidon.go {1, 2} (by simp [IsSidon]) 3).val = 4 := by
-  decide
+  decide +native
 
 /-- Main search loop for generating the greedy Sidon sequence. The return value for step `n` is the
 finite set of numbers generated so far, a proof that it is Sidon, and the greatest element of
 the finite set at that point. This is initialised at `{1}`, then `greedySidon.go` is
 called iteratively using the lower bound `max + 1` to find the next smallest Sidon preserving
 number. -/
-private def greedySidon.aux (n : ℕ) : ({A : Finset ℕ // IsSidon A} × ℕ) :=
+private def greedySidon.aux (n : ℕ) : ({A : Finset ℕ // IsSidon (A : Set ℕ)} × ℕ) :=
   match n with
   | 0 => (⟨{1}, by simp [IsSidon]⟩, 1)
   | k + 1 =>
@@ -68,22 +70,22 @@ theorem greedySidon_zero : greedySidon 0 = 1 := rfl
 
 @[category test, AMS 5]
 theorem greedySidon_one : greedySidon 1 = 2 := by
-  decide
+  decide +native
 
 @[category test, AMS 5]
 theorem greedySidon_two : greedySidon 2 = 4 := by
-  decide
+  decide +native
 
 @[category test, AMS 5]
 theorem greedySidon_three : greedySidon 3 = 8 := by
-  decide
+  decide +native
 @[category test, AMS 5]
 theorem greedySidon_four : greedySidon 4 = 13 := by
-  decide
+  decide +native
 
 @[category test, AMS 5]
 theorem greedySidon_five : greedySidon 5 = 21 := by
-  decide
+  decide +native
 
 @[category test, AMS 5]
 theorem greedySidon_ten : greedySidon 10 = 97 := by

diff --git a/FormalConjectures/ErdosProblems/350.lean b/FormalConjectures/ErdosProblems/350.lean
@@ -37,13 +37,13 @@ theorem decidableDistinctSubsetSums_1_2 : DecidableDistinctSubsetSums {1, 2} :=
   rw [DecidableDistinctSubsetSums] ; decide
 
 @[category test, AMS 5 11]
-theorem distinctSubsetSums_1_2 : DistinctSubsetSums ({1, 2} : Finset ℕ).toSet := by
-  rw [DistinctSubsetSums]
+theorem distinctSubsetSums_1_2 : DistinctSubsetSums ({1, 2} : Set ℕ) := by
+  simp only [DistinctSubsetSums, Set.Pairwise, Set.mem_setOf_eq, ne_eq, id_eq]
   intro x hx y hy hxy
-  simp_rw [Finset.coe_subset, ←Finset.mem_powerset, Finset.setOf_mem, Finset.mem_coe] at *
+  -- FIXME: Why is `norm_cast` useless here?
+  simp_rw [← Finset.coe_singleton, ← Finset.coe_insert, Finset.coe_subset, ←Finset.mem_powerset] at *
   fin_cases hx <;> fin_cases hy <;> simp_all
 
-
 /-- Small sanity check: the two predicates are saying the same thing. -/
 @[category API, AMS 5 11]
 theorem DistinctSubsetSums_iff_DecidableDistinctSubsetSums

diff --git a/FormalConjectures/ErdosProblems/351.lean b/FormalConjectures/ErdosProblems/351.lean
@@ -39,7 +39,7 @@ large integer is a sum of elements of the set `A \ B`. -/
 def IsStronglyComplete {α : Type*} [Semiring α] (A : Set α) : Prop :=
   ∀ B : Finset α,
     ∀ᶠ (m : ℕ) in Filter.atTop,
-      ↑m ∈ { ∑ n ∈ X, n | (X : Finset α) (_ : X.toSet ⊆ A \ B.toSet) }
+      ↑m ∈ { ∑ n ∈ X, n | (X : Finset α) (_ : ↑X ⊆ A \ B) }
 
 /-- The predicate that the rational polynomial `P` has a complete image. -/
 def HasCompleteImage (P : ℚ[X]) : Prop := IsStronglyComplete (imageSet P)