HEXAGONbeta

A Lean Formalization of Myerson-Satterthwaite Impossibility for Continuous Bilateral Trade

Primarily AI-generated textHuman understanding: some partscs.LO — Logic in Computer Sciencemath.LO — Logic

Contributed by Arthur ↗, David Barros Hulak ↗, Ruy J. G. B. de Queiroz ↗

SubmitterArthur

Version 1 / Oct 01, 2026 / CC BY 4.0

Abstract

We present a source-grounded account of a Lean 4 formalization of the Myerson-Satterthwaite impossibility theorem for continuous bilateral trade. Buyer values and seller costs are independent, with atomless probability measures supported on compact real intervals whose interiors overlap. The model explicitly requires restricted Lebesgue measure to be absolutely continuous with respect to each type measure, together with full support; it does not require the type measures themselves to have densities. Under allocation and transfer measurability and integrability conditions, the registered theorem excludes the simultaneous satisfaction of almost-sure ex post efficiency, Bayesian incentive compatibility at every admissible type and report, interim individual rationality, and weak ex ante budget balance. The proof derives envelope identities from incentive inequalities, identifies the efficient allocation almost everywhere, and uses a layer-cake representation to show that the required information rents strictly exceed efficient surplus. We explain the analytic steps, their Lean declarations, and the verification evidence for the exact Palomar-registered source revision. This is an exposition of a classical result and an existing formal artifact, without a claim of mathematical novelty or formalization priority.

Provenance statement

The manuscript names Arthur Freitas Ramos (submitting contributor; ORCID 0009-0003-3568-0325), David Barros Hulak (0009-0002-8056-1774), and Ruy J. G. B. de Queiroz (0000-0003-1482-0977). The submitting contributor reports understanding some parts, but not all, of the work. OpenAI GPT-6.1 assisted with manuscript drafting, inspection of the registered source, organization of the proof exposition, and editorial, bibliography, and consistency checks. The pinned repository formalization.yaml reports gpt-6-luna (Codex CLI) assistance for historical proof engineering. The archival Palomar report records Lean default-kernel, nanoda, and con-ron acceptance. No fresh Lean or Comparator run was performed for the manuscript. Exact registered artifact: https://palomar-registry.org/entry?id=PALOMAR-2026-09-26-000002&version=1 . This is a source-grounded exposition of a classical result and existing formal artifact, without a claim of mathematical novelty or formalization priority.
FormalizationsPalomar

Tools used

OpenAI
ChatGPTVersion GPT 6.1 (manuscript)
OpenAI
CodexVersion gpt-6-luna (historical proof engineering)
Lean
LeanVersion 4.35.0-rc2 (registered artifact)

References

  1. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 Theorem Prover and Programming Language. Automated Deduction–CADE 28, vol. 12699, pp. 625–635. 2021. \urlhttps://doi.org/10.1007/978-3-030-79876-5_37DOI
  2. Myerson, Roger B.; Satterthwaite, Mark A. Efficient Mechanisms for Bilateral Trading. Journal of Economic Theory, vol. 29, no. 2, pp. 265–281. 1983. \urlhttps://doi.org/10.1016/0022-0531(83)90048-0DOI
  3. Palomar Registry. Myerson-Satterthwaite Impossibility Theorem (Continuous Bilateral-Trade Version). 2026. Registered September 26, 2026. \urlhttps://palomar-registry.org/entry?id=PALOMAR-2026-09-26-000002&version=1
  4. Ramos, Arthur Freitas. Myerson-Satterthwaite Theorem (Lean 4 Formalization). 2026. Commit \nolinkurlf4dae9744e26a499679e4b8a7aeb9d82dd3f11ee. \urlhttps://github.com/Arthur742Ramos/myerson-satterthwaite-lean/tree/f4dae9744e26a499679e4b8a7aeb9d82dd3f11ee
  5. The mathlib Community. The Lean Mathematical Library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 367–381. 2020. \urlhttps://doi.org/10.1145/3372885.3373824DOI

Version history

  1. v1Initial depositCurrentOct 01, 2026