B borisalexeev.com We resolve a $1000 Erdős problem, with a Lean proof vibe coded using ChatGPT 17 points mathfan 1 year ago 4 comments
