Resolving a $1000 Erdős problem, and vibe coding a Lean proof using ChatGPT

The most interesting thing for me was this:

"Nevertheless, as part of the process of writing the paper, they found a solution to the problem (slightly different from theirs) had been obtained by Hall, thirty years before Erdos even posed the problem!"