feat(OEIS/80170): mark conjecture as solved (#4253)

Closes #4252

This PR marks `OeisA80170.gcdCondition_iff_primePowerCondition` (a
member of
FC100OpenSet1) as `research solved`, with a `formal_proof` attribute
linking to
a complete Lean 4 proof:


https://github.com/guodk/formal-conjectures/blob/0720658844d76a50d48e4baa152eef14d4462907/FormalConjectures/OEIS/80170.lean#L1823

**About the proof**
- ~1800 lines, no `sorry`; the proved statement is verbatim the one in
this repo.
- Builds inside this repository (Lean v4.27.0, `lake build` green,
linters clean).
- Axiom audit: depends only on `propext`, `Classical.choice`,
`Quot.sound`.
- Mathematical route: Newton forward-difference interpolation, the Lucas
and
Kummer theorems, a digit-box stabilizer theorem, a zero-run lemma, and a
  primary criterion for the binomial GCD `D(k)`.

**Changes**
- `FormalConjectures/OEIS/80170.lean`: `research open` → `research
solved`,
added `formal_proof` attribute (proof body stays `sorry` per the 25–50
line
  policy in CONTRIBUTING.md).
- `FormalConjectures/Subsets/FC100OpenSet1.lean`: category counts 96/4 →
95/5.

**Provenance / AI disclosure:** the proof was found by the informal and
formal
theorem-proving agents developed by the Key Laboratory of Mathematics
Mechanization (KLMM), Chinese Academy of Sciences — the informal agent
produced
the mathematical proof and the formal agent carried out the Lean 4
formalization. The result is fully verified by the Lean compiler.

---------

Co-authored-by: Moritz Firsching <firsching@google.com>

Author: guodk

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

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)
 ]