can you please formalize this problem in Coq or Lean?

Ok, I thought about it some more on another plane flight.

One nice property is that the yes-only shares are proportional to liquidity. I.e. if you double all the yes-only shares, you have double the liquidity.

Let k = sqrt(Aiy * Ain) for answer Ai with Aiy yes shares and Ain no shares.

Let N = Sum_i Ain

Then Ai = Aiy + N - Ain

If you scale liquidity k by c, then kc = c * sqrt(AiyAin) = sqrt(c^2AiyAin) = sqrt((cAiy)(cAin))

This means the yes and no shares scale with liquidity. Since Ai is a linear combination of these yes and no shares, it also scales proportionally.

If the magnitude of the yes-only shares determines liquidity, I think then that the probability is determined by their ratio.

A second idea is that the analysis might be simpler by also keeping track of the "purchased shares" which are outside the AMM and you can track separately.

By that I mean that for any set of Ai from i = 1 to i = n, and given liquidity k, you can first construct the "starting pools" where all Ai are equal:

sqrt(AiyAin) = k

1 / n = Ain / (Aiy + Ain)

=> AiyAin = k^2
=> Aiy = k^2 / Ain

=> 1 / n = Ain / (k^2 / Ain + Ain)

=> 1 / n * (k^2 / Ain + Ain) = Ain

=> k^2 / Ain = (n-1)Ain

=> k^2 = (n-1)Ain^2

=> k = sqrt(n-1)Ain

=> Ain = k / sqrt(n-1)

=> Aiy = k sqrt(n-1)
=> Ai = Aiy - Ain + N = Aiy + (n-1)Ain = k sqrt(n-1) + (n-1)k / sqrt(n-1)

= 2k sqrt(n-1)

Then, for any yes-only shares set, you can make one bet on each answer except for the largest Ai to get from the starting pools to the current pools (Proof not included).

The bet operation is to exchange b_a mana for b_a Yes shares of each answer, add them to the pools, and then withdraw shares in one answer such that the probability and liquidity invariants hold.

WLOG let Ai be in decreasing order.

Let (bia, bis) be a bet on Ai of amount bia in exchange for yes shares bis.

Then the total amount bet Sum_i bia is equal to the largest Ai minus the starting pool amount:

Sum_i bia = A1 - 2k sqrt(n-1)

Also, bis = A1 - Ai

I'm not sure how to calculate individual bia. But knowing bis, the "missing" yes shares that are held by the bettors, and the sequence of operations to transform the starting pools into the current pools seems like it could be useful.

@JamesGrugett just simply ask ChatGPT and it will guide you through the question. Hope this wins me the mana lol.

It should be possible to first find a solution of the last 5 (N+2) equations:

Ap = An / (Ay + An)

Bp = Bn / (By + Bn)

Cp = Cn / (Cy + Cn)

1 = Ap + Bp + Cp

AyAn = ByBn = CyCn

…and then scale it to satisfy the first 3 (N) equations:

A = Ay + Bn + Cn

B = By + An + Cn

C = Cy + An + Bn

As starting values for Ap, Bp, Cp, … I use:

Ap = A / (A+B+C)
Bp = B / (A+B+C)
Cp = C / (A+B+C)

…but I realized that's probably a wrong assumption.

Is there a way to compute Ap, Bp, Cp from A, B, C only – or is that part of the question, too?

I appreciate the call-out in your Substack article: https://news.manifold.markets/p/multiple-choice-markets. Thanks @JamesGrugett

Thanks everyone! I appreciate the time and effort you've put into solving this problem so far.

Looks like there's been some good progress and insights, including an almost-solution from @HarrisonNathan, a clean writeup of a partial solution from @BoltonBailey, analysis and an edited-away proof of a counter example from @Pepe, @gregrosent's clear framing of the solution given L and N, and the sketch of a proof that a solution exists from @LinusTang! Nice!

I'll refrain from awarding bounties while we are still making progress. It's likely I will give some partial credit bounties, especially if a full solution eludes us.

Added this to my market on research ideas

Here's a proof that a solution exists, albeit with some details omitted.

I'm also nerd-sniped but don't have much to show for it yet. One insight I had that others might find helpful (and which, just after I wrote this, I noticed that Bolton had already observed) is a way to parameterize the solution space in terms of just two parameters, instead of a number of parameters proportional to the number of options in the market. Specifically, let L denote the liquidity of some option (doesn't matter which) and let N denote the total number of NO shares across all options. Then the equation "A = Ay + Bn + Cn + Dn + ..." implies "A = L/An - An + N", which has a unique solution for An over the positive reals. (You can solve the quadratic equation for An, but an easier way to see this is that the right side is monotone decreasing in An and maps An=0 to infinity and An=infinity to -infinity.) Then plug into the probability sum constraints and the equation "N = An + Bn + Cn + ...." to see if this is a valid solution. So in summary, there exists at most one solution given L and N, although the challenge remains to show that exactly one value of (L,N) does in fact yield a solution.