I can’t tell from their main text whether the human authors of this math paper that solved the $1,000 Erdos problem 707 used ChatGPT-5 Pro or Thinking or what. Supposing they didn’t use Pro, I wonder how their experience would’ve been if they did; they said that vibe-coding the 6,000+ line Lean proof with ChatGPT took about a week and was “extremely annoying”
(technically one of the authors said Marshall Hall Jr. already solved it in 1947 via counterexample)
I dislike hype-flavored summaries by the likes of Sebastien Bubeck et al, so I appreciated these screenshots of the paper and accompanying commentary by @life2030com on how the authors felt about using ChatGPT to assist them in all this:
I found that “curious inversion” remark at the end interesting too.
I can’t tell from their main text whether the human authors of this math paper that solved the $1,000 Erdos problem 707 used ChatGPT-5 Pro or Thinking or what. Supposing they didn’t use Pro, I wonder how their experience would’ve been if they did; they said that vibe-coding the 6,000+ line Lean proof with ChatGPT took about a week and was “extremely annoying”
(technically one of the authors said Marshall Hall Jr. already solved it in 1947 via counterexample)
I dislike hype-flavored summaries by the likes of Sebastien Bubeck et al, so I appreciated these screenshots of the paper and accompanying commentary by @life2030com on how the authors felt about using ChatGPT to assist them in all this:
I found that “curious inversion” remark at the end interesting too.
That “final step” line is fun because one doesn’t need any math background to understand it: