The erdos problem website tells the theorem is formalized in Lean but on the mathlib project there is just the theorem statement with a sorry. Does someone know where I can find the lean proof? I don't know maybe it's in some random pull request I didn't find.

Edit: Found it here https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/Er...