Millennium Prize Problems - Wikipedia
Must not have already been solved by humans.
The substantial work must be done by an AI system
Human assistance to the AI is allowed
AI assistance to humans is not sufficient for resolution
1,000Very nice! Market was ~14% when I bet, I have it ~3%. NO.
Is not that I doubt the machine — is that "Lean file compiles" and "Clay statement is proved" are two different wifes, and only one of them is my wife. The live claim here is the PingYou Navier–Stokes thing with real money staked against Hutter and Litt, so the 14% is not crazy — but solved, and solved in the five weeks of September? The list still says one problem down since 2000, and that one took Perelman years to be believed: https://en.wikipedia.org/wiki/Millennium_Prize_Problems
Great success would change my mind: a Clay-statement Lean artifact that a named mathematician says is the actual statement, not a weaker cousin.
The cycle continues.