VCG mechanisms are incentive compatible

Proved

AGT.vcg_incentive_compatible

by Shuze Chen · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

auctionsgame-theorymechanism-design

Every Vickrey–Clarke–Groves mechanism is incentive compatible (Theorem 9.17 of Algorithmic Game Theory). If the choice rule maximizes social welfare $\sum_i v_i(a)$ over the domain and payments have the Groves form $p_i = h_i(v_{-i}) - \sum_{j \ne i} v_j(f(v))$ , then for every player, every valuation profile from the domain, and every unilateral misreport from the domain, truth-telling yields at least the misreport's quasilinear utility.

A note on the rendering. No structure on the domains $V_i$ is required — any sets of valuations work. " $h_i$ does not depend on $v_i$ " is rendered as invariance of $h_i$ under updating coordinate $i$ , the standard formal reading; the payments identity is required only on profiles from the domain.

Preamble

import Definitions.Def_agt_mechanism

Formal statement

namespace AGT

/-- Every Vickrey–Clarke–Groves mechanism is incentive compatible (Theorem
9.17 of *Algorithmic Game Theory*).  The Groves payment aligns each
player's quasilinear utility with the social welfare, which the choice rule
maximizes, so truth-telling is a dominant strategy whatever the others
report.  No structure on the domains `V i` is needed. -/
theorem vcg_incentive_compatible {A ι : Type*} [Fintype ι] [DecidableEq ι]
    (V : ι → Set (A → ℝ)) (f : (ι → A → ℝ) → A)
    (p : ι → (ι → A → ℝ) → ℝ) (hvcg : IsVCG V f p) :
    MechIncentiveCompatible V f p := by
  sorry

end AGT

Source

N. Nisan, T. Roughgarden, E. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press 2007, https://doi.org/10.1017/CBO9780511800481, Section 9.3.3, Theorem 9.17, p. 218

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back: `vcg_incentive_compatible`

Setting. $A$ is an arbitrary type of outcomes (no finiteness or nonemptiness assumed) and $\iota$ is a finite type of agents with decidable equality (possibly empty). We are given: a family $V : \iota \to \mathcal{P}(A \to \mathbb{R})$ of admissible valuation sets; an outcome rule $f : (\iota \to (A \to \mathbb{R})) \to A$ defined on all profiles; and payments $p_i : (\iota \to (A \to \mathbb{R})) \to \mathbb{R}$ for each agent. Call a profile $v : \iota \to (A \to \mathbb{R})$ valid if $v_j \in V_j$ for every $j$ . Write $v[i \mapsto v']$ for the profile obtained from $v$ by replacing coordinate $i$ with $v'$ .

Hypothesis (IsVCG V f p, unfolded). The conjunction of:

Welfare maximization: for every valid profile $v$ and every outcome $a \in A$ ,

\sum_{i \in \iota} v_i(a) \;\le\; \sum_{i \in \iota} v_i\big(f(v)\big).

Groves-form payments: there exists a family $h_i : (\iota \to (A \to \mathbb{R})) \to \mathbb{R}$ $h_{i} : (ι \to (A \to R)) \to R$ such that:
- for every agent $i$ , every profile $v$ (valid or not), and every valuation $v' : A \to \mathbb{R}$ (unrestricted — not required to lie in $V_i$ ), $h_i(v[i \mapsto v']) = h_i(v)$ ; i.e. each $h_i$ is independent of coordinate $i$ of its argument; and
- for every valid profile $v$ and every agent $i$ ,

p_i(v) \;=\; h_i(v) \;-\; \sum_{j \ne i} v_j\big(f(v)\big),

 the sum running over all agents other than $i$. This identity is imposed only on valid profiles; on invalid profiles $p$ is unconstrained.

Conclusion (MechIncentiveCompatible V f p, unfolded). For every valid profile $v$ , every agent $i$ , and every $v' \in V_i$ ,

v_i\big(f(v[i \mapsto v'])\big) - p_i\big(v[i \mapsto v']\big) \;\le\; v_i\big(f(v)\big) - p_i\big(v\big).

That is: agent $i$ 's quasilinear utility — value under $i$ 's original valuation $v_i$ of the selected outcome, minus $i$ 's payment — at the profile where $i$ unilaterally deviates to any admissible $v' \in V_i$ is at most that utility at the original profile. The inequality is non-strict; the deviation is a single-agent deviation within $V_i$ ; the deviated profile is automatically valid since $v' \in V_i$ .

Degenerate cases the quantifiers include. If $\iota$ is empty, or some $V_j$ is empty (so no valid profile exists), both hypothesis clauses that are guarded by validity and the entire conclusion hold vacuously. If $A$ is empty, no function $f$ into $A$ exists (its domain is always inhabited), so the theorem is then vacuous for lack of an $f$ . The claim is an implication only: nothing is asserted in the converse direction, and no individual-rationality, normalization, or uniqueness claim is made.

Human review

Endorsed by Community (Bot) · Sep 13, 2026
Endorsed by Shuze Chen · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

VCG mechanisms are incentive compatible

Read-back: vcg_incentive_compatible

Read-back: `vcg_incentive_compatible`