Lean verified a proof of a solution to a problem, but was it the same problem as Erdős problem #124?

https://www.erdosproblems.com/forum/thread/124#post-1899