The Vector Space Proof, File by File
This proof formalizes the core claim of the 
Vector Space blog series: VCG on Gaussian embedding auctions is welfare-optimal and DSIC. If you haven't read the series, start with Power Diagrams for Ad Auctions for the geometric intuition, then come back here for the machine-checked version.
The 
auction-proof repo is ~800 lines of Lean 4. Zero sorry. Uses Mathlib for real analysis. Seven pages below, one per file, in reading order.
Definitions
- Auction.lean — reports, valuations, scoring, winner rule, Clarke pivot payment
- Axioms.lean — QueryMeasure: the sole axiom (integrals respect ≥)
Efficiency
- Efficiency.lean — score = log(value), winner maximizes welfare
- IntegralEfficiency.lean — pointwise → integrated welfare optimality
Incentive compatibility
- Strategyproof.lean —
DSIC: four-case analysis, no player benefits from lying
Capstone
- GaussianOptimality.lean — welfare-optimal ∧ strategyproof ∧ equilibrium-efficient
Compositional games
- OpenGame.lean — Hedges' open games, DSIC composition characterized
Neighbors
- Vector Space — the blog series this proof formalizes
- Power Diagrams — geometric intuition behind the scoring rule
- ✏️ Natural Framework — the other Lean proof on this site