3 ms·

Henry Yuen's (whose work problem 6 builds on) comments on this are worth reading IMO: https://bsky.app/profile/henryyuen.bsky.social/post/3ms2jpchfjc2t https://

by gpm 2mo ago

Henry Yuen's (whose work problem 6 builds on) comments on this are worth reading IMO: https://bsky.app/profile/henryyuen.bsky.social/post/3ms2jpchfjc2t https://bsky.app/profile/henryyuen.bsky.social/post/3ms2jpch...

an0malous 2mo ago
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?
- gpm 2mo ago
  I mean, they're verified in the sense that the lean proof checks out... and presumably OpenAI read them.
  - deleted 2mo ago
    [deleted]
  - doctorwho42 2mo ago
    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.
- margorczynski 2mo ago
  From what I understand all of them have Lean proofs/certificates thus are basically 100% proven without a doubt.
  - voxl 2mo ago
    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.
  - samrus 2mo 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 https://x.com/gro_tsen/status/2082483878480977959
    - gpm 2mo ago
      Between a lean proof, and a peer reviewed paper, the former is a lot less likely to be mistaken... Nothing is perfect.
  - an0malous 2mo ago
    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.
jhrmnn 2mo ago
This starts to feel like chess engines. It’s obvious their play is superior but it’s impossible for humans to understand the moves.
- andai 2mo ago
  It's going to be an interesting time if this generalizes to other fields.

by gpm 2mo ago

an0malous 2mo ago

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?

gpm 2mo ago
I mean, they're verified in the sense that the lean proof checks out... and presumably OpenAI read them.
- deleted 2mo ago
  [deleted]
- doctorwho42 2mo ago
  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.
margorczynski 2mo ago
From what I understand all of them have Lean proofs/certificates thus are basically 100% proven without a doubt.
- voxl 2mo ago
  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.
- samrus 2mo 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 https://x.com/gro_tsen/status/2082483878480977959
  - gpm 2mo ago
    Between a lean proof, and a peer reviewed paper, the former is a lot less likely to be mistaken... Nothing is perfect.
- an0malous 2mo ago
  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.

jhrmnn 2mo ago

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

andai 2mo ago
It's going to be an interesting time if this generalizes to other fields.