Vickrey

A Lean 4 formalization of strategy-proofness for the Vickrey (second-price sealed-bid) auction, built on Mathlib.

What's proved

Theorem (Vickrey.strategyproof). In a Vickrey auction with n ≥ 2 bidders, for any bidder i with private value v, bidding v yields at least as much utility as any alternative bid b, regardless of what other bidders do. Truthful bidding is a weakly dominant strategy.

The formalization also includes:

• Vickrey.truthful_dominates — the abstract 4-case dominance lemma
• Vickrey.maxBidExcluding_update — bid-independence (the threshold a bidder faces is determined entirely by the other bidders)
• Vickrey.truthful_nonneg — individual rationality (truthful utility ≥ 0)

All results are generic over any linearly ordered abelian group (not just ℝ), and compiled with zero sorrys.

Structure

File	Contents
Vickrey/Core.lean	utility, 4-case lemmas, truthful_dominates, truthful_nonneg
Vickrey/Auction.lean	maxBidExcluding, bid-independence, payoff, strategyproof
Vickrey.lean	Root import
TUTORIAL.md	Annotated walkthrough of every definition and proof

Building

Requires elan.

lake update          # resolve dependencies
lake exe cache get   # download pre-built Mathlib (saves hours)
lake build           # compile — should finish in seconds

References

The proof follows Roughgarden's textbook argument and mirrors the architecture of the Caminati et al. Isabelle formalization. The theorem statement is informed by Barthe et al.'s observation that incentive properties are fundamentally relational.

• T. Roughgarden, Twenty Lectures on Algorithmic Game Theory, Lecture 3. Source of the proof strategy: abstract to (value, threshold, bid), observe the threshold is independent of the bidder's own bid, then do a 4-case analysis on win/lose under truthful vs. deviant bidding.

• M. B. Caminati, M. Kerber, C. Lange, C. Rowat, Sound Auction Specification and Implementation (CICM 2015). Isabelle/HOL formalization of the Vickrey auction. The 4-named-lemma structure, and the factoring into "core arithmetic" vs. "auction infrastructure," follow their design. Code at ForMaRE/auction-theory.

• G. Barthe, M. Gaboardi, E. J. Gallego Arias, J. Hsu, A. Roth, P.-Y. Strub, Higher-Order Approximate Relational Refinement Types for Mechanism Design (POPL 2015). Frames strategy-proofness as a relational property — comparing two mechanism executions that differ in one agent's input. This shaped the theorem statement (Function.update makes the two-run comparison explicit).

• MixedMatched/formalizing-game-theory. Lean 4 formalization of basic game theory (Nash equilibrium, pure strategies). Informed type-signature decisions for how to represent bid profiles and deviations in Lean 4.

• Mathlib4. Provides the ordered algebra (Mathlib.Algebra.Order.Group.Defs), finset lattice operations (Mathlib.Data.Finset.Lattice.Fold), and fintype infrastructure used throughout.