`plby` formalisations: sync status/update `formal_proof` tags + add new formalisations

https://github.com/plby/lean-proofs/blob/main/data/sources.yaml

contains many lean formalistaions of Erdős Problems. Some of them we already link with `formal_proof`, some of them we should link with `formal_proof using lean4 ...` or `formal_proof using formal_conjectures` if the formal statement is verbatim what we have in our repo. Also it contains some formalisation of (solved) Erdős problems which haven't yet in our repository. Those should be added as well.

A first step would be to run a script comparing `sources.yaml` against what is produced with our `extract_names` script, i.e. https://google-deepmind.github.io/formal-conjectures/data/conjectures.json comparing with the "formalProofLink" there and seeing what we are missing.

Note: some of those formalisations are incomplete in the sense that they assume some hyporthesis and only prove an implication. Those are marked in the file and also with `partial: yes` in the yaml. Those should not get a `formal_proof` attribute, but we should instead just link the proof manually in the docstring.

Start with data/sources.yaml and run the extract_names script, then compare its entries with data/conjectures.json and the formalProofLink values. Identify missing or outdated links and the additional solved Erdős problems to add; exclude entries marked partial: yes from formal_proof tags and link those proofs manually in the docstring.

Written by the indexing model from the issue text.