diff --git a/FormalConjectures/OEIS/80170.lean b/FormalConjectures/OEIS/80170.lean
index e5e8bd03e1..528d5bd917 100644
--- a/FormalConjectures/OEIS/80170.lean
+++ b/FormalConjectures/OEIS/80170.lean
@@ -58,8 +58,18 @@ def PrimePowerCondition (k : ℕ) : Prop :=
 
 /--
 Conjecture: The gcd condition is equivalent to the prime power condition.
+This has been conjectured by Ralf Stephan.
+
+Both the natural-language proof and its Lean 4 formalization were carried out
+by the KLMM MechMath Agent Team; see the `formal_proof` attribute.
+
+*References:*
+- [Ralf Stephan, *Prove or Disprove. 100 Conjectures from the OEIS*, 2004, Conjecture 17 (arXiv:math/0409509)](https://arxiv.org/abs/math/0409509)
+- [Dakai Guo et al., *A Greatest Common Divisor Criterion of Certain Binomial Coefficients*, 2026 (arXiv:2606.22997)](https://arxiv.org/abs/2606.22997)
 -/
-@[category research open, AMS 11]
+@[category research solved, AMS 11,
+formal_proof using formal_conjectures at
+"https://github.com/guodk/formal-conjectures/blob/0720658844d76a50d48e4baa152eef14d4462907/FormalConjectures/OEIS/80170.lean#L1823"]
 theorem gcdCondition_iff_primePowerCondition (k : ℕ) (hk : 2 ≤ k) :
     GCDCondition k ↔ PrimePowerCondition (k + 1) := by
   sorry
diff --git a/FormalConjectures/Subsets/FC100OpenSet1.lean b/FormalConjectures/Subsets/FC100OpenSet1.lean
index b89b425500..ffe2a5a39e 100644
--- a/FormalConjectures/Subsets/FC100OpenSet1.lean
+++ b/FormalConjectures/Subsets/FC100OpenSet1.lean
@@ -221,6 +221,6 @@ end Subsets.FC100OpenSet1
 
 open Lean Meta ProblemAttributes in
 #eval verifyCategoryCounts Subsets.FC100OpenSet1.problems [
-  ("research open", 96),
-  ("research solved", 4)
+  ("research open", 95),
+  ("research solved", 5)
 ]