Thank you! Much to think about, but later...

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

checkingproofs.

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?

Thank you!

I went ahead and created the 2024 version of one of the questions. If you’re looking for high-liquidity questions to include, which seems like a good way to avoid false alarms / pranks, this one seems like a good inclusion.

There are a bunch of lower-liquidity questions; including a mix of those with some majority-rule type logic might or might not be worth it.