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

▲

jhrmnn a minute ago | parent | next [-]

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

▲

an0malous 2 hours ago | parent | prev [-]

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?

▲

margorczynski an hour ago | parent | next [-]

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

	▲	samrus 3 minutes ago \| parent \| next [-]
		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
	▲	voxl 14 minutes ago \| parent \| prev [-]
		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.

▲

gpm an hour ago | parent | prev [-]

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

	▲	an hour ago \| parent [-]
		[deleted]