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