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 ]
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 ]