updated to "formally solved" from solved lean 1102

FormalConjectures/ErdosProblems/1102.lean

@@ -45,7 +45,7 @@ If `A = {a₁ < a₂ < …}` has property P,
 then `A` has natural density `0`.
 Equivalently, `(a_j / j) → ∞` as `j → ∞`.
 -/
-@[category research solved, AMS 11]
+@[category research formally solved, AMS 11]
 theorem erdos_1102.density_zero_of_P
     (A : ℕ → ℕ)
     (h_inc : StrictMono A)
@@ -58,7 +58,7 @@ Conversely, for any function `f : ℕ → ℕ` that goes to infinity,
 there exists a strictly increasing sequence `A = {a₁ < a₂ < …}`
 with property P such that `(a_j / j) ≤ f(j)` for all `j`.
 -/
-@[category research solved, AMS 11]
+@[category research formally solved, AMS 11]
 theorem erdos_1102.exists_sequence_with_P
     (f : ℕ → ℕ) (h_inf : Tendsto f atTop atTop)
     (h_pos : ∀ n, f n ≠ 0) :
@@ -70,7 +70,7 @@ theorem erdos_1102.exists_sequence_with_P
 /--
 Every sequence with property Q has upper density at most `6 / π^2`.
 -/
-@[category research solved, AMS 11]
+@[category research formally solved, AMS 11]
 theorem erdos_1102.upper_density_Q
     (A : ℕ → ℕ) (h_inc : StrictMono A)
     (hQ : HasPropertyQ (range A)) :
@@ -83,7 +83,7 @@ $\mathsf{SF} := \mathbb{N} \setminus \bigcup_{p} p^{2}\mathbb{N}$, i.e. the set
 squarefree numbers. The set `A` has property `Q` and natural density `6 / π^2`.
 Equivalently, `(j / a_j) → 6/π^2` as `j → ∞`.
 -/
-@[category research solved, AMS 11]
+@[category research formally solved, AMS 11]
 theorem erdos_1102.lower_density_Q_exists :
     ∃ A : ℕ → ℕ, StrictMono A ∧
     (∀ j, Squarefree (A j)) ∧

FormalConjectures/ErdosProblems/434.lean

@@ -47,7 +47,7 @@ maximises the number of integers not representable as the sum of finitely
 many elements from $A$ (with repetitions allowed)?
 Is it $\{n, n - 1, \dots, n - k + 1\}$?
 -/
-@[category research open, AMS 11]
+@[category research formally solved, AMS 11]
 theorem erdos_434.parts.i (n k : ℕ) (hn : 1 ≤ n) (hk : 1 ≤ k) (h : k ≤ n) :
     IsGreatest
       { Nat.NcardUnrepresentable S | (S : Finset ℕ) (_ : S ⊆ Finset.Icc 1 n)
@@ -60,7 +60,7 @@ Let $k \le n$. Out of all $A\subseteq\{1, \dots, n\}$ (with $\text{gcd}(A) = 1$)
 does $A = \{n, n - 1, \dots, n - k + 1\}$ maximise the number of integers
 not representable as the sum of finitely many elements from $A$ (with repetitions allowed)?
 -/
-@[category research open, AMS 11]
+@[category research formally solved, AMS 11]
 theorem erdos_434.parts.ii : answer(sorry) ↔ ∀ᵉ (n ≥ 1) (k ≥ 1), k ≤ n →
     IsGreatest
       { Nat.NcardUnrepresentable S | (S : Finset ℕ) (_ : S ⊆ Finset.Icc 1 n)