← back to the atlas

Fair and Truthful Giveaway Lotteries (aaai22-20405)

Answer: Polynomial-time solvable in \(\tau,L\), with \(u(P)=u^*(\mu,\kappa)\).

The anchor (named result in the paper)

Theorem 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateAlgorithm IPMAX is hybrid adjunctive group strategyproof (and in particular group strategy proof), pro- duces a solution that is leximin optimal, and approximates the utilization to at least a 1/2 factor. By Propositions 3 and 2, IPMAX is also anonymous, envy-free, and Pareto optimal (ex-ante and ex-post). By Propositions 4 and 5, hybrid adjunctive group strategyproof is the strongest possible stretegy proofness if leximin opti- mality is desired, and by Propositions 7 and 6, a 1/2 uti- lization is the best possible for either leximin optimality or hybrid adjunctive group strategyproofness.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given finite \(K\subseteq\mathbb{Z}_{>0}\), rational family masses \(\mu\in\Delta(K)\), and rational capacity \(\kappa>0\), compute an exactly represented finite-support lottery \(P\) over \(Z(\mu,\kappa)=\{z:0\le z_k\le\mu_k,\ \sum_{k\in K}kz_k\le\kappa\}\), implemented by exchangeably selecting whole families from each nonatomic type class. The induced mechanism must lexicographically maximize type admission rates \(q_k=\mathbb{E}_P[z_k]/\mu_k\), be Pareto-optimal and envy-free, resist every measurable positive-mass hybrid adjunctive split/merge report, and achieve \(u(P)\ge\frac{1}{2}u^*(\mu,\kappa)\).

Packaged proof task (what the prover saw — nothing else)

A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational; \(\tau\) is the support size, not the number of possible types. Here \(\varnothing\ne K\subset\mathbb Z_{>0}\), \(m=\max K\), \(\mu_k>0\), \(\sum_k\mu_k=1\), and \(\kappa>0\) is rational. Let \(L\) be the total binary input length; measure running times in \(m,\tau,L\), with polynomial time meaning polynomial in \(\tau,L\), since \(m\) is binary encoded.
Type \(k\) consists of a nonatomic family space of measure \(\mu_k\); each family has \(k\) indivisible members and succeeds only when all its members are admitted. Capacity is measured in individual mass, so individual families have zero capacity cost and there is no restriction \(k\le\kappa\).
An outcome selects measurable sets of whole families, with selected type masses \(z\in Z(\mu,\kappa)=\{z:0\le z_k\le\mu_k,\ \sum_k kz_k\le\kappa\}\). A mechanism outputs a finite lottery \(P\) with rational weights and rational outcome vectors, together with a finitely described randomized implementation giving almost every type-\(k\) family admission probability \(q_k=\mathbb E_P[z_k]/\mu_k\). Type anonymity is the intended meaning of exchangeable selection here; correlations are part of the implementation.
Leximin optimality means lexicographically maximizing the vector \((q_k)_{k\in K}\) sorted in nondecreasing order. Require ex-ante Pareto optimality for family admission probabilities and ex-post maximality against adding a positive mass of unselected families.
Envy-freeness means, for almost every pair of families \(A,B\), that \(\Pr[A\subseteq S]\ge\Pr[B\subseteq S\text{ and }(S\setminus B)\cup A\text{ is feasible}]\), where \(S\) is the selected set of individuals.
A hybrid adjunctive report chooses a measurable positive-family-mass coalition \(C\), adds a finite mass of uninterested individuals, and measurably repartitions these and all coalition members into nonempty finite reported families; no individual is duplicated, outsiders remain unchanged, and every new family contains an original coalition member. Reports may both split and merge families and must have finite size support.
After a report, let \(\nu'_j\) be the absolute reported family masses and \(T'=\sum_j\nu'_j\); evaluate the mechanism at \(\mu'_j=\nu'_j/T'\) and \(\kappa'=\kappa/T'\). The mechanism is defined mathematically also for real masses, although computation is required only on rational inputs. A true family's deviating utility is the probability that all its original members are admitted, regardless of their reported groups; hybrid adjunctive group strategyproofness forbids a report that strictly improves this utility for almost every family in \(C\).
Define \(u(P)=\mathbb E_P[\sum_k kz_k]/\kappa\) and \(u^*(\mu,\kappa)=\max_{z\in Z(\mu,\kappa)}\sum_k kz_k/\kappa\).

Is computing such a mechanism, simultaneously satisfying leximin optimality, both Pareto requirements, envy-freeness, hybrid adjunctive group strategyproofness, and \(u(P)\ge\tfrac12u^*(\mu,\kappa)\), polynomial-time solvable in \(\tau,L\), or NP-hard?

For explicitly listed discrete families, IPMAX has all these guarantees and runs in time polynomial in the number of families and numeric capacity. [Arbiv–Aumann](https://ojs.aaai.org/index.php/AAAI/article/view/20405)
A later discrete result gives an FPTAS for leximin and explicitly notes the unary-capacity qualification of the exact algorithm; no result settling the precise nonatomic mechanism problem above was located. [Hartman et al.](https://arxiv.org/html/2409.10395v3#S11.SS2)

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Result

The problem is polynomial-time solvable in \(\tau,L\). The mechanism below satisfies all the requested properties and, more strongly, achieves \(u(P)=u^*(\mu,\kappa)\).

The proof uses the intended interpretation of anonymity: equal admission probabilities within each type, with correlations permitted.

1. The uniquely optimal probability vector

Define total individual mass and a common admission probability by

\[ W=\sum_{k\in K}k\mu_k, \qquad p=\min\left\{1,\frac{\kappa}{W}\right\}. \]

For any feasible lottery, linearity of expectation gives

\[ \sum_{k\in K}k\mu_kq_k =\mathbb E_P\left[\sum_{k\in K}kz_k\right] \le\kappa. \]

Consequently, if \(t=\min_{k\in K}q_k\), then \(tW\le\kappa\). Since admission probabilities also satisfy \(t\le1\), every feasible lottery has \(t\le p\).

The vector \(q_k=p\) is feasible: the outcome

\[ z_k=p\mu_k \]

satisfies all coordinate bounds and uses individual mass \(pW=\min\{W,\kappa\}\).

Moreover, this is the unique probability vector attaining minimum probability \(p\). If \(\kappa<W\) and all \(q_k\ge p\), then

\[ 0\le\sum_{k\in K}k\mu_k(q_k-p) \le\kappa-pW=0. \]

Every coefficient \(k\mu_k\) is positive, so every \(q_k=p\). If \(\kappa\ge W\), attaining minimum probability \(p=1\) likewise forces every coordinate to equal \(1\).

Thus \(q_k=p\) is uniquely leximin optimal.

2. A finitely described implementation

Output the one-outcome lottery

\[ P=\delta_z, \qquad z=(p\mu_k)_{k\in K}. \]

Although its outcome vector is deterministic, the implementation randomizes which families realize those selected masses.

For the canonical realization of a support-only input, represent type-\(k\) families by \(x\in[0,1)\), with family measure \(\mu_k\,dx\). Draw one uniform random variable \(U\in[0,1)\). Select the whole family at coordinate \(x\) precisely when

\[ \operatorname{frac}(x+U)<p, \]

where \(\operatorname{frac}\) denotes fractional part.

For each fixed \(U\), the selected coordinates form a circular interval of Lebesgue measure \(p\). Hence selected type mass is exactly \(p\mu_k\), and capacity is respected in every realization.

For each fixed family coordinate \(x\), uniformity of \(U\) gives

\[ \Pr[\operatorname{frac}(x+U)<p]=p. \]

Thus every family has the required probability, even though family selections are correlated.

This construction also works on arbitrary nonatomic family spaces. The nonatomic divisibility lemma states that a measurable set of finite measure contains a measurable subset of any prescribed intermediate measure. Its hypotheses hold for each type space. Recursively bisecting that space produces a measurable uniform coordinate: the successive binary partition labels have every length-\(n\) prefix with normalized measure \(2^{-n}\), so their binary expansion has uniform distribution on \([0,1)\). Pulling the circular-interval rule back through this coordinate preserves both calculations above. Injectivity is unnecessary.

The implementation therefore has a finite symbolic description: one uniform draw and the displayed selection rule on the canonical type circles.

3. Pareto properties and utilization

Ex-ante Pareto optimality

If \(\kappa<W\), a feasible vector weakly improving every \(q_k=p\) and strictly improving one would have

\[ \sum_{k\in K}k\mu_kq_k>pW=\kappa, \]

contradicting feasibility. If \(\kappa\ge W\), every family already succeeds with probability \(1\).

The same argument covers family-specific competitors, even without anonymity. Let \(\eta_k\) be type-\(k\) family measure, and let \(r_k(A)\) be a competitor’s admission probability for family \(A\). By Tonelli’s theorem, its expected individual usage is

\[ \sum_{k\in K}k\int r_k(A)\,d\eta_k(A). \]

Weakly increasing probabilities almost everywhere, with strict increases on a set of positive family mass, makes this integral strictly exceed \(\kappa\) when capacity is scarce. Thus the mechanism is Pareto optimal under the usual almost-everywhere interpretation as well.

Ex-post maximality

When \(\kappa<W\), every realization uses exactly \(\kappa\). Adding a positive mass of unselected whole families increases individual usage strictly, because every family size is positive. Such an addition is infeasible.

When \(\kappa\ge W\), the implementation selects all families. There are no unselected families to add.

Optimal utilization

Any outcome uses at most both \(W\) and \(\kappa\), and our outcome attains their minimum. Therefore

\[ u(P)=\frac{\min\{W,\kappa\}}{\kappa} =u^*(\mu,\kappa). \]

In particular, the required factor-\(\tfrac12\) guarantee holds.

4. Envy-freeness

For any families \(A,B\), the event on the right-hand side of the required envy inequality is contained in the event that \(B\) is admitted. Hence

\[ \Pr\!\left[B\subseteq S\text{ and }(S\setminus B)\cup A \text{ is feasible}\right] \le\Pr[B\subseteq S] =p =\Pr[A\subseteq S]. \]

This proves envy-freeness without requiring any further property of the swap event.

5. Hybrid adjunctive group strategyproofness

Extend the same formulas and circular-interval implementation to real masses.

Consider any permitted report. Let \(D\ge0\) denote the individual mass of added uninterested individuals. Because the report repartitions all original individuals without duplication and leaves outsiders unchanged, conservation of individual mass gives

\[ \sum_j j\nu'_j=W+D. \]

The reported support is finite and consists of positive finite sizes. Consequently, \(T'=\sum_j\nu'_j\) is finite and positive.

Applying the mechanism to the normalized reported instance gives every reported family admission probability

\[ p' =\min\left\{1, \frac{\kappa/T'}{\sum_j j(\nu'_j/T')}\right\} =\min\left\{1,\frac{\kappa}{W+D}\right\} \le p. \]

The normalization therefore cancels exactly. Splitting and merging cannot raise the common reported probability; adding individuals can only decrease it.

Now fix any true coalition family \(A\), and choose one of its original members \(a\). Let \(G(a)\) be the reported family containing that member. Since the mechanism admits reported families whole, every realization satisfies

\[ \{\text{all original members of }A\text{ are admitted}\} \subseteq \{G(a)\text{ is admitted}\}. \]

Taking probabilities yields

\[ \Pr[\text{all original members of }A\text{ are admitted}] \le p'\le p. \]

This argument permits arbitrary correlations and arbitrary splitting or merging: it uses only one original member as a necessary condition for true-family success.

The circular-interval implementation assigns probability \(p'\) to every reported coordinate, so the bound does not depend on transferring an almost-everywhere assertion through the reporting map. Every true family covered by the report is bounded in this way; in particular, almost every coalition family is.

Before reporting, each true family succeeds with probability \(p\). Therefore no permitted report strictly improves the utilities of almost every family in a positive-mass coalition. This proves hybrid adjunctive group strategyproofness.

6. Binary complexity and the discrete comparison

On rational inputs, compute \(W\), then \(p\), then the \(\tau\) coordinates \(p\mu_k\). Output these coordinates with lottery weight \(1\) and the implementation rule.

All calculations use exact rational arithmetic. A common denominator for the input masses can be taken to be the product of their denominators, whose binary length is at most the sum of their input lengths. Summation, multiplication by the binary-encoded sizes, and division by \(W\) therefore produce numbers with binary lengths polynomial in \(L\). There are only polynomially many arithmetic operations, and the output has polynomial length.

Thus construction takes time polynomial in \(\tau,L\). There is no iteration up to numeric \(m\) or numeric capacity.

The discrete knapsack obstacle does not transfer to this model: nonatomic families allow the exact selected masses \(p\mu_k\) while keeping each family whole. The finite-family formulation and its unary-capacity qualification are described explicitly in [Hartman et al., Section 11.2](https://arxiv.org/html/2409.10395v3#S11.SS2). The proof here establishes the requested nonatomic result directly.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

Verification report

Verdict: proved with minor gaps. The argument establishes polynomial-time construction of the requested mechanism in \(\tau,L\), with optimal utilization. No central step is false, and no additional mathematical idea is needed. Two routine details in the measure-theoretic discussion require clarification.

1. Leximin optimality

The definitions of \(W\) and \(p\) are valid: the support is finite and nonempty, every \(k\mu_k\) is positive, and therefore \(W>0\).

The expected-capacity inequality follows from feasibility of every lottery outcome. Consequently, the bound on the smallest admission probability is correct.

The proposed vector \(z_k=p\mu_k\) satisfies the coordinate bounds and the capacity constraint. It establishes attainability of the upper bound on the minimum probability.

The uniqueness argument is also correct:

Thus maximizing the first sorted coordinate already determines the entire vector uniquely. The leximin conclusion follows.

2. Randomized implementation

On the canonical type circles, the implementation is correct. For every fixed realization of \(U\), the selection rule identifies a measurable set of normalized measure \(p\) in each type. Its outcome vector is exactly \(z\), rather than merely having expectation \(z\).

For each fixed family coordinate, translation modulo one preserves the uniform distribution of \(U\), so its admission probability is exactly \(p\). Using the same random variable across types introduces permitted correlations without changing either calculation.

The distinction between a one-outcome lottery over mass vectors and a randomized implementation over actual selected families is explicitly allowed by USER_TASK. There is no inconsistency here.

The stated nonatomic divisibility lemma has the required hypotheses: each type space is nonatomic and has finite positive measure. The recursive binary partitions yield a measurable coordinate with the asserted uniform distribution, subject to the following endpoint detail.

Minor issue 1 — binary-coordinate endpoint. A binary expansion whose labels are all ones equals one. The write-up calls the coordinate \([0,1)\)-valued without specifying what happens on that exceptional set. This is a null-set convention, and the fractional-part rule remains meaningful at one, so none of the substantive conclusions fails.

Minimum clarification: specify the coordinate convention on the exceptional endpoint set, and state that the coordinate and selection rule are defined for every family. This also makes the pointwise claim used in Section 5 fully explicit.

The polynomial-time claim concerns producing the finite implementation description for the support-only input. It does not require enumerating selected families, generating an exact real random variable in finitely many bit operations, or computationally constructing partitions of an unencoded abstract measure space. Under the task’s stated output model, the finite symbolic description is sufficient.

3. Pareto requirements and utilization

Ex-ante Pareto optimality

For competitors described by type probabilities, the argument is correct. Under scarce capacity, any coordinatewise improvement with a strict improvement in at least one coordinate raises expected individual usage above capacity. Under abundant capacity, all probabilities already equal one.

The extension to family-specific competitors is substantively correct under the stated almost-everywhere interpretation. A nonnegative probability improvement that is strictly positive on a set of positive family measure has strictly positive integral. The finite sum over types therefore exceeds the capacity bound.

Minor issue 2 — Tonelli application. The write-up invokes Tonelli without stating its precise relevant form or explicitly identifying the jointly measurable selection indicator to which it applies. Measurability of each realized selected set, considered separately, is not itself the full hypothesis for interchanging the two integrals.

Minimum clarification: state that admissible randomized competitors have a jointly measurable family-admission indicator, and state the nonnegative-integrand version of Tonelli being invoked. Identify the probability measure and family measure used in that application. This is a routine formalization of the measurable randomized-mechanism interpretation, rather than a new lemma.

Ex-post maximality

The proof is correct. When capacity is scarce, every realization uses exactly \(\kappa\). Adding a positive family mass increases individual usage because all family sizes are positive. When capacity is abundant, every family is selected.

This establishes precisely the requested maximality against additions of positive mass. It does not rely on treating an individual nonatomic family as having positive capacity cost.

Utilization

The upper bound by both \(W\) and \(\kappa\) is correct, and the proposed outcome attains their minimum. Therefore the claimed equality with \(u^*\) follows.

The utilization denominator is valid because \(\kappa>0\). The required approximation guarantee follows immediately, including when \(\kappa>W\).

4. Envy-freeness

The event inclusion is correct regardless of whether the swap itself is feasible. The right-hand event is contained in the admission event for \(B\).

Both families have admission probability \(p\), so the required inequality follows. Neither independence nor any stronger permutation-invariance assumption is needed. The task expressly defines the intended anonymity through equal type probabilities and permits correlations.

5. Hybrid adjunctive group strategyproofness

The conservation identity follows from the permitted report: original individuals are repartitioned without duplication, outsiders remain unchanged, and added individuals contribute nonnegative individual mass \(D\).

Finite reported size support and finite individual mass ensure that \(T'\) is finite. It is positive because the original society has positive individual mass and reported families are nonempty.

The normalization calculation is correct. The factors of \(T'\) cancel, leaving a common reported-family probability determined by \(W+D\). Since \(D\ge0\), this probability cannot exceed the truthful probability.

The crucial event inclusion is valid: success of a true family requires admission of the reported family containing any one of its original members. Each true family is nonempty, so such a member exists.

This argument requires neither independence among reported groups nor a measurable choice of one member simultaneously across all true families. It is a pointwise argument for each fixed true family.

The prover also correctly avoids an otherwise important null-set problem: the circular rule gives the same probability to every reported coordinate, rather than only almost every coordinate. Thus an arbitrary reporting map cannot invalidate the bound by routing original members into exceptional reported families. Minor issue 1 should be clarified to make this pointwise statement fully explicit.

The resulting bound excludes even an individual true-family improvement, and therefore excludes the coalition improvement forbidden by USER_TASK. Splitting, merging, real reported masses, and addition of uninterested individuals are all covered.

6. Binary complexity and cited comparison

The rational-arithmetic argument is correct. The product-denominator bound controls intermediate bit lengths; multiplication by binary-encoded sizes introduces only polynomially many bits. Computing \(W\), \(p\), and the output coordinates requires polynomially many arithmetic operations on polynomial-length integers.

The output contains only \(\tau\) rational coordinates, weight one, and a finite implementation rule. No loop depends on numeric \(m\) or numeric capacity.

The cited discrete comparison is accurate: Section 11.2 describes finite groups and explicitly notes the unary-capacity qualification of the exact algorithm. That citation supplies background rather than a necessary theorem for the nonatomic proof. [Hartman et al., Section 11.2](https://arxiv.org/html/2409.10395v3#S11.SS2)

Required feedback

Clarify the binary-coordinate endpoint convention and the measurability hypotheses for the Tonelli application. No change to the mechanism, complexity analysis, or strategyproofness argument is required.

⟨structured verdict parsed — rendered above⟩

Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.