Should be a top 10 math problem of its math subfield, so nothing crazy but several mathematicians care about it and have tried solving it.
I have started a project to see how doable this is at scale, may drop it if it doesn’t go anywhere. Tips welcome.
By ‘solve’ I don't have a too airtight definition, but it would definitely count if a Lean statement was proven without exploiting bugs in the lean kernel for example, as would an involved expert mathematician signing off on it. Edge cases like AIs all agreeing the solution is clearly correct, and nobody managing to find errors, would lead to the market staying closed pre-resolution to give the math community time to find errors, but I may ultimately count it without strong guarantees if it seems very likely to be correct.
A problem still counts if it's a solve that shows the problem wasn't interesting after all, or similar cope
For the purpose of this market there are roughly 300-500 math "subfields", yielding around 4000 open problems that, if solved, would resolve this market positively.
Last month's market resolved NO:
1,000People are also trading
I have several candidate solutions, which I will verify better before resolving this market YES. but 2 of them are fully lean verified
With one of these, your agent will able to run to code to check if its formalized proof solved the problem: https://google-deepmind.github.io/formal-conjectures/
@Bayesian Outside of maybe P vs NP and Riemann hypothesis I don't think there's agreement on even the top problem in any subfield, let alone the top 10.
How would you define this? Asking people in the field for each of their top 10? Good luck untangling the Arrow-type paradoxes!
I think your market is interesting but maybe the criterion should be something like "at least k published papers in journals with impact factor > f attacked the problem or solved a special case".