Open Research Index

agv-mechanism-lean

Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz

Palomar Registrypalomar/PALOMAR-2026-10-02-000006Oct 2, 2026cs.GTscore 0

Lean 4 formalization of the AGV (d'Aspremont-Gérard-Varet-Arrow) expected-externality mechanism: with independent types, ex post efficiency, Bayesian incentive compatibility, and budget balance are jointly attainable. Agents are indexed by Fin n with 2 ≤ n; each agent has a finite nonempty type space with an independent PMF prior; alternatives form a finite nonempty type; values are private. The efficient rule xmax maximizes utilitarian welfare, and agvTransfer pays each agent its expected externality minus an equal share of the other agents' receipts. Interim individual rationality is not…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-10-02-000006
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-02-000006/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-02-000006/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'