Hacker News new | ask | show | jobs
Resolving a $1000 Erdős problem, and vibe coding a Lean proof using ChatGPT (mathstodon.xyz)
5 points by mathfan 244 days ago
1 comments

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!"