We resolve a $1000 Erdős problem, with a Lean proof vibe coded using ChatGPT

I was looking at the submitter's past comments, and the most recent one is interesting: https://news.ycombinator.com/item?id=45092516

> Wow, I was already impressed with the new comment feature on erdosproblems.com and how it's already been used to solve some of the problems. Excited to see if AI can make a meaningful contribution here.

Since then, there has been some discussion of GPTPro finding a bunch of references, thus enabling many of the problem statuses to be changed from "open" to "solved". But it seems that LLMs couldn't find the right reference for this problem.

But there was a different meaningful contribution from AI here instead.

This was a nice read. It was especially nice for the authors to say many times things like "we had _x_ trouble with Lean but it didn't feel like Lean's fault". That feels new to me!