google-deepmind / google-deepmind/formal-conjectures
Formal proofs for Erdos problems 45, 46 and 298
Open
erdos-problems
erdos-status-sync
- Dominant language
- Lean
- Stars
- 1.3k
- Forks
- 485
- Avg merge
- 1d 20h
- Merged PRs (30d)
- 328
Description
According to [comment within this PR](https://github.com/teorth/erdosproblems/pull/276), it seems there is now a Lean 4 formal proof for [Erdos problem 298](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/298.lean). Since currently referenced formal proof is in Lean 3, does it make sense to also add a link to Lean 4 formal proof?
Additionally, if Erdos problems 45 and 46 are added to this repository in the future, should [the same Lean 4 formal proof as for 298](https://github.com/plby/unit-fractions/blob/a18841f8f2803f9680c4a00dc458fbe8d3eb6bda/src4/ErdosProblems.lean) be referenced?
Contributor guide
Assessment
This issue has not been assessed yet.