Mark Erdős Problem 260 as solved

[Hanziwww]

A complete Lean 4 proof of the exact right-hand side of
FormalConjectures/ErdosProblems/260.lean is available in an external
repository:

• Permanent proof: https://github.com/Hanziwww/erdos260/blob/1f2baf4547f2c2805cdd160611b0b983f43941aa/Erdos260/DeepMind.lean#L92-L132
• Proof repository: https://github.com/Hanziwww/erdos260
• Successful verification run: https://github.com/Hanziwww/erdos260/actions/runs/29516048968
• Associated paper: https://arxiv.org/abs/2606.24972

The external theorem proves the exact RHS currently used in Formal
Conjectures, including a : ℕ → ℤ, the original n = 0 division, integer
exponentiation in 2 ^ a n, StrictMono, Tendsto, HasSum, and the
conclusion Irrational s.

The pinned proof repository builds without sorry, project-specific axioms,
or opaque proof stand-ins. Its successful CI run includes the ordinary Lean
build and axiom audit at trust level zero, serial Leanchecker replay, and an
independent Nanoda kernel check.

I propose the following small update:

1. Change @[category research open] to @[category research solved].
2. Replace answer(sorry) with answer(True).
3. Add a formal_proof using lean4 attribute pointing to the permanent proof
   above.

The full proof will remain in the external repository, following the
contribution guideline for proofs longer than approximately 25--50 lines.

Related: #457 and #1629.