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

https://github.com/Jayyhk/erdos-lean/tree/main https://github.com/Jayyhk/erdos-lean/tree/main/problems

contains many lean formalizations of Erdős Problems. Some of them are probably already linked with formal_proof; some of them should link with formal_proof using lean4 ... or formal_proof using formal_conjectures if the formal statement is verbatim what is in this repo. Also it probably contains some formalizations of (solved) Erdős problems which aren't yet in our repository. Those should be added as well.

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

Note: some of those formalisations are incomplete in the sense that they assume some hypothesis and only prove an implication. Those are marked in the README. Those should not get a formal_proof attribute, but should instead just link the proof manually in the docstring.

[This issue echoes #3998 ]

Start by comparing README.md with the output of the extract_names script and data/conjectures.json, focusing on each entry's formalProofLink. Check the linked Jayyhk repository and its problems directory for missing or incomplete formalisations, using the README markings to distinguish manual docstring links from formal_proof tags. Done means existing links and statuses are synchronized and eligible missing formalisations are added.

Written by the indexing model from the issue text.