So I’ve been thinking a little more about the real-world-incentives problem, and I still suspect that there are situations in which rules won’t solve this. Suppose there’s a prediction market question with a real-world outcome tied to the resulting market probability (i.e. a relevant actor says “I will do XYZ if the prediction market says ABC”). Let’s say the prediction market participants’ objective functions are of the form play_money_reward + real_world_outcome_reward. If there are just a couple people for whom real_world_outcome_reward is at least as significant as play_money_reward and if you can reliably identify those people (i.e. if you can reliably identify the people with a meaningful conflict of interest), then you can create rules preventing those people from betting on the prediction market.
However, I think that there are some questions where the number of people with real-world incentives is large and/or it’s difficult to identify those people with rules. For example, suppose a sports team is trying to determine whether to hire a star player and they create a prediction market for whether the star athlete will achieve X performance if hired. There could be millions of fans of that athlete all over the world who would be willing to waste a little prediction market money to see that player get hired. It’s difficult to predict who those people are without massive privacy violations—in particular, they have no publicly verifiable connection to the entities named in the prediction market.
For anyone wanting to harness AI models to create formally verified proofs for theoretical alignment, it looks like last call for formalizing question statements.
Game theory is almost completely absent from mathlib4. I found some scattered attempts at formalization in Lean online but nothing comprehensive. This feels like a massive oversight to me—if o12345 were released tomorrow with perfect reasoning ability then I’d have no framework with which to check its proofs of any of my current research questions.