Thanks! I’ll try to answer some of your questions.
For complicated proofs, the fully formally verified statement all the way back to axioms might be very long. In practice, do we end up with markets for all of those?
In practice, I think not. I expect interesting conjectures to end up thickly traded such that the concept of a market price makes sense. For most other propositions, I expect nobody to hold any shares in them at all most of the time. To take the example of Alice and ¬A, if we suppose that Alice is the only one with a proof of A, then everyone else has to tie up capital to invest in A, but Alice can just create shares of ¬A for free, and then sell them for profit. If A is an interesting conjecture, then Alice can sell on the open market and Bob can buy from the open market. If A is a niche thing, only useful as a step in the proof of B, then Bob might trade directly with Alice and the price will be determined by how hard Bob would find it to come up with a proof of A himself, or to find someone other than Alice to trade with. So Alice does have to keep her proof secret for as long as she wants to profit from it.
Second question: how does this work in different axiom systems? Do we need separate markets, or can they be tied together well?
Different axiom systems can encode each other. So long as we start from an axiom system that can fully describe Turing machines, statements about other axiom systems should be possible to encode as statements about certain specific Turing machines. The root system has to be consistent. If it’s inconsistent, then people can just money pump the market mechanism. But systems built on top need not be consistent. If people try to prove things about some pet system that they’ve encoded, and that system happens to be inconsistent, that means that they’re surprised by the outcomes of some markets they’re trading on, but it doesn’t blow up the entire rest of the market.
If there are a large number of true-but-not-publicly-proven statements, does that impose a large computational cost on the market making mechanism?
I expect that the computers running this system might have to be fairly beefy, but they’re only checking proofs. Coming up with proofs is a much harder task, and it’s the traders who are responsible for that. Sorry if this is a bad answer, I’m not 100% sure what you’re getting at here.
Is there any way to incentivize publishing proofs, or do we simply get a weird world where everyone is pretty sure some things are true but the only “proof” is the market price?
For thickly traded propositions, I can make money by investing in a proposition first, then publishing a proof. That sends the price to $1 and I can make money off the difference. Usually, it would be more lucrative to keep my proof secret, though. So I think we do actually get this weird world you’re talking about. The market mechanism can see all the proofs everyone is using, of course, but people wouldn’t want to trade with a market mechanism that would blab their proofs everywhere. We can imagine that the market mechanism does reveal the proofs, but only after 10 or 20 years so that the discoverer has had plenty of chance to make money.
I think that knowing which things are true even if you don’t know why does still contribute something to mathematical progress, in a weird way. There’s a trick in theoretical comp-sci where a program that tells you whether a given SAT problem is solvable can be run repeatedly (only a linear number of times) to give an actual concrete solution to that SAT problem. You try setting the first variable to 0, leaving all the others free. If the problem is still solvable, you set it to 0. Otherwise, you set it to 1. Repeating this process gives a full solution to the SAT problem. Something similar might be possible for proofs.
If there are a large number of true-but-not-publicly-proven statements, does that impose a large computational cost on the market making mechanism?
I expect that the computers running this system might have to be fairly beefy, but they’re only checking proofs.
They’re not, though. They’re making markets on all the interrelated statements. How do they know when they’re done exhausting the standing limit orders and AMM liquidity pools? My working assumption is that this is equivalent to a full Bayesian network and explodes exponentially for all the same reasons. In practice it’s not maximally intractable, but you don’t avoid the exponential explosion either—it’s just slower than the theoretical worst case.
If every new order placed has to be checked against the limit orders on every existing market, you have a problem.
For thickly traded propositions, I can make money by investing in a proposition first, then publishing a proof. That sends the price to $1 and I can make money off the difference. Usually, it would be more lucrative to keep my proof secret, though.
The problem I’m imaging comes when the market is trading at .999, but life would really be simplified for the market maker if it was at actually, provably 1. So it could stop tracking that price as something interesting, and stop worrying about the combinatorial explosion.
So you’d really like to find a world where once everyone has bothered to run the SAT-solver trick and figure out what route someone is minting free shares through, that just becomes common knowledge and everyone’s computational costs stop growing exponentially in that particular direction. And furthermore, the first person to figure out the exact route is actually rewarded for publishing it, rather than being able to extract money at slowly declining rates of return.
In other words: at what point does a random observer start turning “probably true, the market said so” into “definitely true, I can download the Coq proof”? And after that point, is the market maker still pretending to be ignorant?
They’re not, though. They’re making markets on all the interrelated statements. How do they know when they’re done exhausting the standing limit orders and AMM liquidity pools?
There’s no reason I can’t just say: “I’m going to implement the rules listed above, and if anyone else wants to be a market-maker, they can go ahead and do that”. The rules do prevent me from losing money (other than cases where I decide to subsidize a market). I think in some sense, this kind of market does run more on letting traders make their own deals, and less on each and every asset having a well-defined price at a given point in time. (Though market makers can maintain networks tracking which statements are equivalent, which helps with combining the limit orders on the different versions of the statement.)
In other words: at what point does a random observer start turning “probably true, the market said so” into “definitely true, I can download the Coq proof”?
Good question, I’m still not sure how to handle this.
Thanks! I’ll try to answer some of your questions.
In practice, I think not. I expect interesting conjectures to end up thickly traded such that the concept of a market price makes sense. For most other propositions, I expect nobody to hold any shares in them at all most of the time. To take the example of Alice and ¬A, if we suppose that Alice is the only one with a proof of A, then everyone else has to tie up capital to invest in A, but Alice can just create shares of ¬A for free, and then sell them for profit. If A is an interesting conjecture, then Alice can sell on the open market and Bob can buy from the open market. If A is a niche thing, only useful as a step in the proof of B, then Bob might trade directly with Alice and the price will be determined by how hard Bob would find it to come up with a proof of A himself, or to find someone other than Alice to trade with. So Alice does have to keep her proof secret for as long as she wants to profit from it.
Different axiom systems can encode each other. So long as we start from an axiom system that can fully describe Turing machines, statements about other axiom systems should be possible to encode as statements about certain specific Turing machines. The root system has to be consistent. If it’s inconsistent, then people can just money pump the market mechanism. But systems built on top need not be consistent. If people try to prove things about some pet system that they’ve encoded, and that system happens to be inconsistent, that means that they’re surprised by the outcomes of some markets they’re trading on, but it doesn’t blow up the entire rest of the market.
I expect that the computers running this system might have to be fairly beefy, but they’re only checking proofs. Coming up with proofs is a much harder task, and it’s the traders who are responsible for that. Sorry if this is a bad answer, I’m not 100% sure what you’re getting at here.
For thickly traded propositions, I can make money by investing in a proposition first, then publishing a proof. That sends the price to $1 and I can make money off the difference. Usually, it would be more lucrative to keep my proof secret, though. So I think we do actually get this weird world you’re talking about. The market mechanism can see all the proofs everyone is using, of course, but people wouldn’t want to trade with a market mechanism that would blab their proofs everywhere. We can imagine that the market mechanism does reveal the proofs, but only after 10 or 20 years so that the discoverer has had plenty of chance to make money.
I think that knowing which things are true even if you don’t know why does still contribute something to mathematical progress, in a weird way. There’s a trick in theoretical comp-sci where a program that tells you whether a given SAT problem is solvable can be run repeatedly (only a linear number of times) to give an actual concrete solution to that SAT problem. You try setting the first variable to 0, leaving all the others free. If the problem is still solvable, you set it to 0. Otherwise, you set it to 1. Repeating this process gives a full solution to the SAT problem. Something similar might be possible for proofs.
Thank you! Much to think about, but later...
They’re not, though. They’re making markets on all the interrelated statements. How do they know when they’re done exhausting the standing limit orders and AMM liquidity pools? My working assumption is that this is equivalent to a full Bayesian network and explodes exponentially for all the same reasons. In practice it’s not maximally intractable, but you don’t avoid the exponential explosion either—it’s just slower than the theoretical worst case.
If every new order placed has to be checked against the limit orders on every existing market, you have a problem.
The problem I’m imaging comes when the market is trading at .999, but life would really be simplified for the market maker if it was at actually, provably 1. So it could stop tracking that price as something interesting, and stop worrying about the combinatorial explosion.
So you’d really like to find a world where once everyone has bothered to run the SAT-solver trick and figure out what route someone is minting free shares through, that just becomes common knowledge and everyone’s computational costs stop growing exponentially in that particular direction. And furthermore, the first person to figure out the exact route is actually rewarded for publishing it, rather than being able to extract money at slowly declining rates of return.
In other words: at what point does a random observer start turning “probably true, the market said so” into “definitely true, I can download the Coq proof”? And after that point, is the market maker still pretending to be ignorant?
There’s no reason I can’t just say: “I’m going to implement the rules listed above, and if anyone else wants to be a market-maker, they can go ahead and do that”. The rules do prevent me from losing money (other than cases where I decide to subsidize a market). I think in some sense, this kind of market does run more on letting traders make their own deals, and less on each and every asset having a well-defined price at a given point in time. (Though market makers can maintain networks tracking which statements are equivalent, which helps with combining the limit orders on the different versions of the statement.)
Good question, I’m still not sure how to handle this.