feat(ErdosProblems): 194

[danielchin]

I didn't actually see an issue created for Erdos 194, but nonetheless, there's no existing lean file so trying to formalize it regardless.

[mo271]

Thanks, LGTM!

[mo271]

I didn't actually see an issue created for Erdos 194, but nonetheless, there's no existing lean file so trying to formalize it regardless.

I only created issues for open Erdős Problems, but it is also welcome to tackle formatlizing the statement of solved ones!

[danielchin]

@mo271 I believe this should be good to go if you want to merge.

[mo271]

thanks!