Simply directly declaring a $100 million reward for a solution would probably not work.
If it didn’t directly yield a solution, I think it would produce a huge leap forward. That’s a huge sum of money. Syndicates would form, and some would be competent.
As for your and John’s schemes, I didn’t try to understand them, but they seem to be heavy on logical formalism. But you shouldn’t overestimate the importance of deductive formalism in fundamental mathematical research. Creativity and ingenuity are the truly essential ingredient.
Did you reach the section on computer assistance yet? The idea is that mathematicians could use their creative insight as normal, write up a paper as normal (minus a lot of effort spent on polishing), and then ask GPT-4 or a successor to convert that into the corresponding low-level formalism. I get the sense that we’re only just passing (or are about to pass) the technology threshold where it could possibly make sense to do things this way. The market idea does have several advantages:
Formal reasoning means that proofs produced in this way do not contain errors.
Non-mathematicians can participate (for smaller leaps of reasoning than the ones requiring lots of creativity and deep mathematical intuition).
Reinforcement learning algorithms can participate.
GOFAI algorithms can participate.
Better combination of insights from all these participants.
Automatically creates prediction markets on conjectures.
Very speculatively: Might have some application as a variant of logical induction?
The main drawbacks are:
Doesn’t necessarily produce interpretable proofs.
Profit-motivated participants have to keep their proofs secret, maybe for a long time if they expect most of the supply for the shares they can redeem to appear a long ways into the future.
As you say, overhead from formalism.
Of course, even if you think all this math stuff isn’t interesting, the application to ordinary prediction markets allows double-investing in conditional markets, which I think is pretty nice.
If it didn’t directly yield a solution, I think it would produce a huge leap forward. That’s a huge sum of money. Syndicates would form, and some would be competent.
As for your and John’s schemes, I didn’t try to understand them, but they seem to be heavy on logical formalism. But you shouldn’t overestimate the importance of deductive formalism in fundamental mathematical research. Creativity and ingenuity are the truly essential ingredient.
Did you reach the section on computer assistance yet? The idea is that mathematicians could use their creative insight as normal, write up a paper as normal (minus a lot of effort spent on polishing), and then ask GPT-4 or a successor to convert that into the corresponding low-level formalism. I get the sense that we’re only just passing (or are about to pass) the technology threshold where it could possibly make sense to do things this way. The market idea does have several advantages:
Formal reasoning means that proofs produced in this way do not contain errors.
Non-mathematicians can participate (for smaller leaps of reasoning than the ones requiring lots of creativity and deep mathematical intuition).
Reinforcement learning algorithms can participate.
GOFAI algorithms can participate.
Better combination of insights from all these participants.
Automatically creates prediction markets on conjectures.
Very speculatively: Might have some application as a variant of logical induction?
The main drawbacks are:
Doesn’t necessarily produce interpretable proofs.
Profit-motivated participants have to keep their proofs secret, maybe for a long time if they expect most of the supply for the shares they can redeem to appear a long ways into the future.
As you say, overhead from formalism.
Of course, even if you think all this math stuff isn’t interesting, the application to ordinary prediction markets allows double-investing in conditional markets, which I think is pretty nice.