571–580 of 1001 posts
Pretty cool. The impact of AI is getting undeniable, there aren’t many positions left to move the goalposts to at this stage, next they’ll have to be outside the stadium entirely. The sooner people can be broken out of their denial about all this the better, and we can start actually taking it seriously.
In a way the most remarkable thing about this is that it isn't even at the top of the HN homepage. Even if this is a step up from what we've seen before, we're no longer astonished by the idea that AI can make significant advances in mathematics and computer science.
This is not at the top as it is actively flagged by people that can't psychologically cope with the advances of AI. Hacker News is no longer a web site of an elite.
I am duly impressed by the powerl of the nameless internal AI, but not a single human contributor's name listed anywhere? Did someone at least make this model a coffee?
surely some human regularly typed "think deeper, make no mistakes".
The GitHub repo with the Lean formalizations just came out a couple of hours ago: https://github.com/openai/ten-proofs It also links to a paper written by an LLM where the model "reconstructs how the proof came together" based on the unpublished reasoning traces: https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf I wish they'd publish the prompts though!
Pretty cool. The impact of AI is getting undeniable, there aren’t many positions left to move the goalposts to at this stage, next they’ll have to be outside the stadium entirely. The sooner people can be broken out of their denial about all this the better, and we can start actually taking it seriously.
The models are frequently getting worse at items that they aren’t being benchmarked for — and that’s happening more and more over time! Other people in other fields aren’t idiots, they are accurately perceiving the fact that these models are being hyper optimized for our industry, and are becoming less capable in other domains over time. Models of the same scale are massively worse at writing a broad variety of style…
That’s not a credible position, but there isn’t anything that I or anyone else can say to someone who simply doesn’t want to believe something.
Earlier quoted context omitted.
It sounds like he hasn't verified the results of a problem that he has personally worked on, so how many of these problems have actually been verified?
From what I understand all of them have Lean proofs/certificates thus are basically 100% proven without a doubt.
Earlier quoted context omitted.
Proof? In my experience modern models are better at all tasks than models from two years ago, especially complex multi-step tasks.
you are working on coding. they are working on things like "creative writing" remember that gpt 4o was popular among those who had ai as a romantic partnet?
I suspect GPT 5.6 would be even better at it, if given the same sycophantic system prompt and lack of guardrails.
Henry Yuen's (whose work problem 6 builds on) comments on this are worth reading IMO: https://bsky.app/profile/henryyuen.bsky.social/post/3ms2jpch...
Not being an expert in any of the fields OpenAI has "advanced" I don't want to prematurely downplay the significance of this contribution. However, I am worried that the language they are using in this blog post is exaggerating for the sake of marketing. It is true there hasn't been a reliable computational approach to solving these problems before. But do these proofs contribute new ideas to the mathematical corpus,…
Pretty cool. The impact of AI is getting undeniable, there aren’t many positions left to move the goalposts to at this stage, next they’ll have to be outside the stadium entirely. The sooner people can be broken out of their denial about all this the better, and we can start actually taking it seriously.
Which straw man are you arguing against?