> Wow, I was already impressed with the new comment feature on erdosproblems.com and how it's already been used to solve some of the problems. Excited to see if AI can make a meaningful contribution here.
Since then, there has been some discussion of GPTPro finding a bunch of references, thus enabling many of the problem statuses to be changed from "open" to "solved". But it seems that LLMs couldn't find the right reference for this problem.
But there was a different meaningful contribution from AI here instead.
mathfan•3mo ago
Yep, I'm excited to see how AI can transform the math research workflow!
Ericson2314•3mo ago
This was a nice read. It was especially nice for the authors to say many times things like "we had _x_ trouble with Lean but it didn't feel like Lean's fault". That feels new to me!
readthenotes1•3mo ago
Reminds me of an early attempt at a language created to prove program correctness.
One attempt reported there were more errors in the proving language than in the program itself
somecontext•3mo ago
> Wow, I was already impressed with the new comment feature on erdosproblems.com and how it's already been used to solve some of the problems. Excited to see if AI can make a meaningful contribution here.
Since then, there has been some discussion of GPTPro finding a bunch of references, thus enabling many of the problem statuses to be changed from "open" to "solved". But it seems that LLMs couldn't find the right reference for this problem.
But there was a different meaningful contribution from AI here instead.
mathfan•3mo ago