Theorem 3.2 (Roberts, 1979) — a weighted VGC mechanism is truthful

Proved

AlgMechDesign.Randomized.weighted_vgc_truthful

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

algorithmic-game-theorymechanism-designp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1vcg

Let $v^i(t^i, o)$ be the valuations of $n$ agents over a set of outputs $O$ , and let $\beta^1,\dots,\beta^n > 0$ be weights. Let $m = (o(t), p(t))$ be a direct revelation mechanism in the weighted VGC family: $o(t)$ maximizes $\sum_i \beta^i v^i(t^i, o)$ over all outputs $o$ , and

p^i(t) = \frac{1}{\beta^i}\sum_{j \ne i} \beta^j v^j\big(t^j, o(t)\big) + h^i(t^{-i})

for functions $h^i$ that do not depend on $t^i$ . Then $m$ is truthful: for every agent $i$ , all declarations $t^{-i}$ of the others, every true type $t^i$ and every misreport $d^i$ ,

v^i\big(t^i, o(t^{-i}, d^i)\big) + p^i(t^{-i}, d^i) \le v^i\big(t^i, o(t^{-i}, t^i)\big) + p^i(t^{-i}, t^i).

In the paper, the biased min work mechanism restricted to one task is a weighted VGC mechanism with weights $\{1,\beta\}$ or $\{\beta, 1\}$ , and this theorem gives its truthfulness.

Formalization Note The output set, the types and the valuations are arbitrary; the weights are assumed positive as in Definition 8.

Preamble

import Mathlib
import Definitions.Def_AlgMechDesign_Randomized_WeightedVGC

Formal statement

namespace AlgMechDesign.Randomized

/-- Theorem 3.2 (Roberts, 1979): for positive weights `β`, every mechanism of the weighted VGC
family is truthful. -/
theorem weighted_vgc_truthful {n : ℕ} {O : Type*} {T : Fin n → Type*}
    (v : ∀ i, T i → O → ℝ) (β : Fin n → ℝ) (hβ : ∀ i, 0 < β i)
    (o : (∀ i, T i) → O) (p : (∀ i, T i) → Fin n → ℝ) (hvgc : IsWeightedVGC v β o p) :
    IsTruthfulGeneral v o p := by sorry

end AlgMechDesign.Randomized

Source

Nisan, Ronen, Algorithmic Mechanism Design, Games Econ. Behav. 35, 2001, p. 174, Theorem 3.2 (with Definitions 8 and 9, pp. 173–174)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph