Erdős Problem 973 has a negative answer

### Describe the misformalization

[`Erdos973.erdos_973`](https://github.com/google-deepmind/formal-conjectures/blob/2270d31e8dd611521f979de6d86da364930b7669/FormalConjectures/ErdosProblems/973.lean#L41-L43) is still marked `research open` with `answer(sorry)`, but Erdős Problem 973 has been solved negatively by Luo, Yang, and Zhu in [*Exterior power sums*](https://arxiv.org/abs/2607.22017).

### Trivial proof/disproof

[arXiv:2607.22017](https://arxiv.org/abs/2607.22017)

### Suggested fix

Change `answer(sorry)` to `answer(False)`, mark the theorem `research solved`, and add the paper to the references.

### Additional context

The authors also link to a [Lean 4 development](https://github.com/miracleqihe/Erdos-973_solution_check-by-Lean); it verifies parts of the proof, not the full theorem.

### Choose either option

- [ ] I plan on working on this issue
- [x] This issue is up for grabs: I would like to see this misformalization fixed by somebody else

Open FormalConjectures/ErdosProblems/973.lean at the referenced theorem and compare its status and answer with the issue description. Update the answer and research status, add the cited paper to the references, and confirm the theorem no longer contains the reported placeholder.

Written by the indexing model from the issue text.