This is very neat work, thank you. One of those delightful things that seems obvious in retrospect, but that I’ve never seen expressed like this before. A few questions, or maybe implementation details that aren’t obvious:
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? Do they each need liquidity from an automated market maker? Presumably not if you’re starting from axioms and building a full proof, and that applies to implications and conjunctions and so on as well, because the market doesn’t need to keep tracking things that are proven. However:
First Alice, who can prove A, produces many many shares of ¬A for free. This is doable if you have a proof for A by starting from a bunch of free ⊥ shares and using equivalent exchange. She sells these for $0.2 each to Bob, pure profit.
In order for this to work, the market must be willing to maintain a price for these shares in the face of a proof that they’re equivalent to ⊥. Presumably the proof is not yet public, and if Alice has secret knowledge she can sell with a profit-maximizing strategy.
She could simply not provide the proof to the exchange, generating A and ¬A pairs and selling only the latter, equivalent to just investing in A, but that requires capital. It’s far more interesting if she can do it without tying up the capital.
So how does the market work for shares of proven things, and how does the proof eventually become public? 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?
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?
Second question: how does this work in different axiom systems? Do we need separate markets, or can they be tied together well? How does the market deal with “provable from ZFC but not Peano”? “Theorem X implies corollary Y” is a thing we can prove, and if there’s a price on shares of “Theorem X” then that makes perfect sense, but does it make sense to put a “price” on the “truth” of the ZFC axioms?
Presumably if we have a functional market that distinguishes Peano proofs from ZFC proofs, we’d like to distinguish more axiom sets. What happens if someone sets up an inconsistent axiom set, and that inconsistency is found? Presumably all dependent markets become a mess and there’s a race to the exits that extracts all the liquidity from the AMMs; that seems basically fine. But can that be contained to only those markets, without causing weird problems in Peano-only markets?
Probably some of this would be clearer if I knew a bit more about modern proof formalisms.
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.
Second question: how does this work in different axiom systems? Do we need separate markets, or can they be tied together well? How does the market deal with “provable from ZFC but not Peano”? “Theorem X implies corollary Y” is a thing we can prove, and if there’s a price on shares of “Theorem X” then that makes perfect sense, but does it make sense to put a “price” on the “truth” of the ZFC axioms?
Actually, I don’t think that creates any problem? Just create shares of “ZFC axioms” and “not ZFC axioms” via logical share splitting. If you are unable to sell “not ZFC axioms”, that only means that price of one main share is $1 (though, it’s likely possible to prove something fun if we take these axioms as false).
This is very neat work, thank you. One of those delightful things that seems obvious in retrospect, but that I’ve never seen expressed like this before. A few questions, or maybe implementation details that aren’t obvious:
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? Do they each need liquidity from an automated market maker? Presumably not if you’re starting from axioms and building a full proof, and that applies to implications and conjunctions and so on as well, because the market doesn’t need to keep tracking things that are proven. However:
In order for this to work, the market must be willing to maintain a price for these shares in the face of a proof that they’re equivalent to ⊥. Presumably the proof is not yet public, and if Alice has secret knowledge she can sell with a profit-maximizing strategy.
She could simply not provide the proof to the exchange, generating A and ¬A pairs and selling only the latter, equivalent to just investing in A, but that requires capital. It’s far more interesting if she can do it without tying up the capital.
So how does the market work for shares of proven things, and how does the proof eventually become public? 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?
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?
Second question: how does this work in different axiom systems? Do we need separate markets, or can they be tied together well? How does the market deal with “provable from ZFC but not Peano”? “Theorem X implies corollary Y” is a thing we can prove, and if there’s a price on shares of “Theorem X” then that makes perfect sense, but does it make sense to put a “price” on the “truth” of the ZFC axioms?
Presumably if we have a functional market that distinguishes Peano proofs from ZFC proofs, we’d like to distinguish more axiom sets. What happens if someone sets up an inconsistent axiom set, and that inconsistency is found? Presumably all dependent markets become a mess and there’s a race to the exits that extracts all the liquidity from the AMMs; that seems basically fine. But can that be contained to only those markets, without causing weird problems in Peano-only markets?
Probably some of this would be clearer if I knew a bit more about modern proof formalisms.
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.
Actually, I don’t think that creates any problem? Just create shares of “ZFC axioms” and “not ZFC axioms” via logical share splitting. If you are unable to sell “not ZFC axioms”, that only means that price of one main share is $1 (though, it’s likely possible to prove something fun if we take these axioms as false).