4 ms·
Resolving a $1000 Erdős problem, and vibe coding a Lean proof using ChatGPT
- derbOac 1y agoThe 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!"