Hacker News Reader

Comment by gpm | Hacker News Reader

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...

View on HN

This starts to feel like chess engines. It’s obvious their play is superior but it’s impossible for humans to understand the moves.

It's going to be an interesting time if this generalizes to other fields.

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?

I mean, they're verified in the sense that the lean proof checks out... and presumably OpenAI read them.

Or they made another LLM 'read' them?

> You are an expert in the field of mathematics, with decades of experience. You are a reviewer of proofs, etc etc.etc.

From what I understand all of them have Lean proofs/certificates thus are basically 100% proven without a doubt.

Incorrect. The statement in Lean can itself be wrong. Moreover, they could be exploiting a kernel bug in Lean, of which we had one published literally a week ago.

We recently saw that lean itself isnt proven correct. Its not likely but i wouldnt call it verified if its only verified in lean

https://x.com/gro_tsen/status/2082483878480977959

Between a lean proof, and a peer reviewed paper, the former is a lot less likely to be mistaken...

Nothing is perfect.

Besides for what others have mentioned, the lean proof could be proving something else. Given AI’s propensity to hallucinate, seems like someone should check the lean proof actually expresses what it’s claimed to.

Reply on news.ycombinator.com