This project checks selected results from Sébastien Lahaie and Benjamin Lubin's Iterative Vickrey Auctions via Linear Programming, August 2026 revision. It verifies the payment identity and conditional LP results, and gives a machine-checked counterexample to Lemma 5's step-size claim under its stated assumptions.
The counterexample starts from a feasible price state. Whether Algorithm 1 can reach that state from its initialization remains unproved. An additional invariant might restrict the lemma's scope; this project does not establish a failure of the complete algorithm.
The counterexample · Proof coverage · Run the checks · Validation
Lemma 5 says that a prescribed price update preserves feasibility and lowers the LP objective. Here is a small instance where the update breaks a buyer constraint. The full certificate is refutes_unrestricted_lemma5 in Lemma5.lean, which connects the assumptions, starting state, direction, and failed conclusion in one theorem.
Every bidder has the same valuation, defined for every nonnegative integer quantity:
v(k) = 2 × min(k, 2).
Marginal values are 2, 2, 0, 0, … . Values are integer, nonnegative, and zero for the empty bundle. The paper's consumption rule—allow zero, or a quantity with positive marginal value—gives exactly {0,1,2}. Lean proves these properties for all natural quantities, so the domain is not arbitrarily truncated.
The main economy contains all three bidders. Each marginal economy removes one bidder. Every economy has enough bidder capacity to allocate all three units.
Set the LP variables as follows, for each bidder present in the relevant economy:
| Variable | Main economy | Each marginal economy |
|---|---|---|
| Unit price p | 3 | 0 |
| Bidder offset α | 0 | 3 |
| Buyer utility bound π | 1 | 1 |
| Seller bound μ | 9 | 6 |
The offered bundle price is the lowest applicable affine price, ρ(k) = min(3k, 3). Every bidder has an economy containing it that attains this minimum.
| Quantity k | Value v(k) | Price ρ(k) | Utility v(k) − ρ(k) |
|---|---|---|---|
| 0 | 0 | 0 | 0 |
| 1 | 2 | 3 | −1 |
| 2 | 4 | 3 | 1 |
Every bidder uniquely demands two units. Minimum total demand in the main economy is therefore 6, exceeding supply 3.
The certificate checks every sign condition and all three constraint families in Eq. (6), including the displayed seller constraint's global production set. It also proves that the buyer and seller bounds are attained: the auxiliary variables are already as small as feasibility permits for the fixed prices. All state coordinates are integers, and bundle prices are nonnegative and zero at the empty bundle.
Selecting the main economy, Theorem 4 constructs this direction:
| Direction variable | Value |
|---|---|
| q, the unit-price change | 1/3 in the main economy; 0 elsewhere |
| λ, the buyer-bound change | −2/3 for every active bidder/economy pair |
| ν, the offset change | 0 in the main economy; 2/3 elsewhere |
| r(k), the bundle-price change | min(k, 2)/3 |
Lean checks the actual demand and minimum-price index restrictions in Eq. (8). The direction is feasible and has objective −1, satisfying the negative-direction requirement.
Lemma 5 prescribes Δ = K = 3. For the zero bundle, the update gives:
new π = 1 + 3 × (−2/3) = −1
new ρ(0) = 0 + 3 × 0 = 0
The buyer constraint (6a) requires v(0) − new ρ(0) ≤ new π. It becomes 0 ≤ −1.
applyStep constructs the updated state, and updated_buyer_constraint_fails extracts this contradiction from it. no_seller_variable_can_repair_update proves that any choice of the updated seller variable μ leaves the buyer violation intact.
Updating only the slopes and offsets, then recomputing the remaining variables, gives the bundle price min(4k, 5). Utilities become (0, −2, −1), so the smallest nonnegative buyer bound is now π = 0.
This restores feasibility, but raises the dual objective 36 → 42. The Lean calculation uses defined old and updated states. The independent checker obtains the seller bounds by enumerating production allocations.
The issue in Appendix A's induction is also identifiable: decreasing marginal values do not justify the required inequality for every affine price branch. For the main branch and quantities 0 and 1 in this example, that inequality would require 2 ≥ 4. A different branch makes quantity two attractive.
Keep the same bidders and supply, but use ρ(k) = min(3k, 4). Utilities are (0, −1, 0), so demand is exactly {0,2}.
Every economy passes §4.2's min/max balance test: minimum total demand is 0; maximum is 6 in the main economy and 4 in each marginal economy. Yet every allocation drawn from these demand sets has an even total quantity, so none totals 3.
demand_has_gap and balance_without_clearing verify this counterexample to the unrestricted demand-convexity and balance arguments. As with the Lemma 5 example, reachability from the algorithm's initialization is not established.
The project also proves positive results from the paper. The qualifications below are part of the formal statements. “Mass” means the sum of fractional allocation variables.
| Paper result | What is checked | Source |
|---|---|---|
| §2: supported allocations are efficient | Buyer utility optimality plus seller revenue maximality imply welfare maximality. | support_efficient |
| Theorem 1: UCE prices determine VCG payments | The payment equals the marginal revenue difference. The revenue calculation may use any marginal revenue maximizer. | vcg_from_uce, vcg_from_universal_prices |
| Lemma 2: replace x by χ | Objective conservation, transformed feasibility, and CE feasibility of χ, including fractional solutions. | objective_preserved, diagonalize, chi_feasible |
| Lemma 2: integral optimum transfer | Transfer from supplied integral CE optima when each buyer's mass is bounded by its economy's seller mass. Seller mass one suffices. | integral_optimum_preserved_of_mass_compatible, integral_optimum_preserved_normalized |
| Lemma 2: seller normalization | Assign unused seller mass to an allocation with zero resource embedding, preserving feasibility and integrality. | integral_optimum_preserved |
| Theorem 3, certificate form | Feasible allocations and Eq. (6)'s bounds, with zero total duality gap, imply equilibrium support in every economy. | uce_of_lp_certificate |
| Theorem 3, nonnegative-price convention | Explicit nonnegative prices and main/marginal indexing give UCEPrices. |
paper_uce_of_zero_total_gap |
Two assumptions matter. First, an economic empty allocation need not have a zero resource embedding for nonlinear indicator encodings. The normalization theorem covers zero-preserving embeddings, including multi-unit and product-mix resource quantities; other embeddings need compatible witnesses or a separate argument. The transformation uses v2's seller variables and vector resource balance, with values shared across economies.
Second, Theorem 3's zero-gap certificate must be supplied and checked. General LP strong duality, deriving zero gap solely from optimality, and extracting economic allocations from arbitrary integral LP coordinates are outside this verification. The code also separates the paper's nonnegative-price convention from the displayed LP's free ρ variables.
Other work outside scope includes general Theorem 4, Algorithm 1 reachability and convergence, activity-rule incentives, the empirical tables, and the product-mix implementation. The particular Theorem 4 direction used above is checked.
Requires elan and uv. Lean and Mathlib revisions are pinned in lean-toolchain, lakefile.toml, and lake-manifest.json.
From the project directory, fetch dependencies on a fresh checkout:
lake updateThen run all proofs, the axiom audit, and the regression tests:
bash scripts/check.shTo see the independent exact-fraction reconstruction alone:
uv run python -B scripts/independent_check.pyThe target is arXiv:2507.03252v2, revised 11 August 2026. Source metadata records the downloaded HTML's URL and checksum. Local reference copies are excluded from Git.
The recorded validation on 10 September 2026 passed:
- 328 project declarations, including 169 theorems, audited with only
propext,Classical.choice, andQuot.sound. Counts include generated helpers and private definitions. - 7 independent-checker tests, covering the reconstructed constraints, deliberately corrupted states, the update, and the distinction between global and marginal seller domains.
- 6 audit tests, confirming rejection of unused/private axioms, proof holes, and unsafe definitions, while accepting an ordinary private proof.
The audit examines all project declarations, including private and unused definitions. The intentionally bad fixtures exist only in temporary files. There are no admitted proofs or custom axioms in the Lean project, and warnings fail the build.
Worked examples apply the payment theorem to bidders with values 2 and 1, proving the winner pays 1, and check seller normalization from mass zero.
A separate AI subagent challenged the source mapping and wrote the independent checker, which uses exact fractions and reads no Lean constants. Review strengthened the example to ensure marginal economies can fill supply, made envelope attainment and auxiliary tightness explicit, aligned Eq. (6c)'s domain, and narrowed the LP coverage claims. The review converged with no remaining substantive objections. It was not an external human review or author confirmation.
Start with Lemma5.lean, which includes a notation glossary and explanatory comments. Read these declarations in order:
refutes_unrestricted_lemma5— the complete certificate, at the bottom of the file.ModelHypotheses— the global valuation and exact consumption-set assumptions.DualFeasibleandRestrictedFeasible— the equation-by-equation translation.prescribedDirection,applyStep, andupdated_buyer_constraint_fails— the update and contradiction.
The remaining question for the author is precise: is an additional reachable-state invariant intended to restrict Lemma 5?
Copyright © 2026 June Kim. The original code and documentation in this repository
are licensed under the GNU General Public License, version 3 or later
(GPL-3.0-or-later). You may redistribute and modify them under those terms.
They are provided without warranty; see LICENSE for the full terms.
Lean, Mathlib, and other dependencies retain their own licenses. The cited paper belongs to its authors and is not relicensed by this project.