Skip to content(if available)orjump to list(if available)

We resolve a $1000 Erdős problem, with a Lean proof vibe coded using ChatGPT

We resolve a $1000 Erdős problem, with a Lean proof vibe coded using ChatGPT

4 comments

·October 21, 2025
Visit

somecontext

I was looking at the submitter's past comments, and the most recent one is interesting: 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

Yep, I'm excited to see how AI can transform the math research workflow!

Ericson2314

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

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