2 ms·
We resolve a $1000 Erdős problem, with a Lean proof vibe coded using ChatGPT
- somecontext 1y agoI was looking at the submitter's past comments, and the most recent one is interesting: https://news.ycombinator.com/item?id=45092516 https://news.ycombinator.com/item?id=45092516 > 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 1y agoYep, I'm excited to see how AI can transform the math research workflow!
- Ericson2314 11mo agoThis 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 11mo agoReminds 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