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

> My summary is that Aristotle solved "a" version of this problem (indeed, with an olympiad-style proof), but not "the" version.

> I agree that the [BEGL96] problem is still open (for now!), and your plan to keep this problem open by changing the statement is reasonable. Alternatively, one could add another problem and link them. I have no preference. — BorisAlexeev

There we go, so there is hype to some degree.

Is there some good literature to read about lean? First time I’m hearing about it and it seems pretty cool.

Anything in type theory. Lean is fundamentally a strongly typed dependently typed programming language. Start with Haskell and keep going.