feat(OEIS/80170): mark conjecture as solved

[guodk]

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.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[mo271]

Thanks, looks good to me!

Congrats on proving this!

[mo271]

Perhaps @rwst can comment if this solution solves the intended conjecture

[mo271]

Suggested change

	Conjecture: The gcd condition is equivalent to the prime power condition.
	Conjecture: The gcd condition is equivalent to the prime power condition.
	This has been conjectured by Ralf Stephan.

This is prexisting and should hvae been added when this conjecture was added: but let's mention that this conjecture was added to the OEIS by Ralf Stephan, (who is also a frequent contributor to our repo under the github hanble @rwst !)

[rwst]

@guodk Looking good, congratulations! Is there a publication we can refer to?

[guodk]

@guodk Looking good, congratulations! Is there a publication we can refer to?

Thank you! Two papers are currently in preparation: one on the informal and formal theorem-proving agents we used, and one on the mathematical proof of A080170 itself. We plan to post both as arXiv preprints soon, and I'll share the links here once they're available.

[rwst]

@guodk Maybe you want to cite https://arxiv.org/abs/math/0409509 . The conjecture is (17).

[mo271]

@guodk Maybe you want to cite https://arxiv.org/abs/math/0409509 . The conjecture is (17).

let's also add that to the docstring here, I suppose

[guodk]

@rwst @mo271 Thanks for waiting. The arXiv preprint is now available at https://arxiv.org/abs/2606.22997. It gives the natural-language proof and describes the Lean formalization used for this PR.

[mo271]

@rwst @mo271 Thanks for waiting. The arXiv preprint is now available at https://arxiv.org/abs/2606.22997. It gives the natural-language proof and describes the Lean formalization used for this PR.

@guodk Great! Can you add a link to that preprint in the docstring/reference section in the file?
Also let's put @rwst 's arxiv paper in the references

[guodk]

@rwst @mo271 Thanks for waiting. The arXiv preprint is now available at https://arxiv.org/abs/2606.22997. It gives the natural-language proof and describes the Lean formalization used for this PR.

@guodk Great! Can you add a link to that preprint in the docstring/reference section in the file? Also let's put @rwst 's arxiv paper in the references

Completed in commit 33af73c — docstring now cites Ralf Stephan's Proof or Disprove: 100 Conjectures from OEIS (Conjecture 17) and the proof preprint (arXiv:2606.22997). Both the natural-language proof and Lean 4 formalization are credited to the KLMM MechMath Agent Team. Thank you!

[guodk]

@mo271 Friendly ping - the new commit 33af73c needs workflow approval to run CI (it's in action_required). Could you approve & run when you have a moment? Thanks!

-awaiting-author