M mathstodon.xyz Resolving a $1000 Erdős problem, and vibe coding a Lean proof using ChatGPT 5 points mathfan 1 year ago 1 comments
